Skip to content

Commit 5773aa5

Browse files
mtzguidomtzguido
authored
Merge pull request #4217 from mtzguido/check
update check-friends: remove karamel and pulse jobs, set KRML_EXE, mo…
2 parents 0c689c3 + dd07fe7 commit 5773aa5

1 file changed

Lines changed: 20 additions & 177 deletions

File tree

‎.github/workflows/check-friends.yml‎

Lines changed: 20 additions & 177 deletions
Original file line numberDiff line numberDiff line change
@@ -9,76 +9,6 @@ defaults:
99
shell: bash
1010

1111
jobs:
12-
build-krml:
13-
runs-on: ubuntu-latest
14-
container: mtzguido/dev-base:v2
15-
steps:
16-
- name: Cleanup
17-
run: sudo find . -delete
18-
- run: echo "HOME=/home/user" >> $GITHUB_ENV
19-
- uses: mtzguido/set-opam-env@master
20-
21-
- uses: actions/download-artifact@v8
22-
with:
23-
name: fstar.tar.gz
24-
- run: tar -xzf fstar.tar.gz
25-
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
26-
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
27-
28-
- name: Checkout karamel
29-
uses: actions/checkout@master
30-
with:
31-
path: karamel/
32-
repository: FStarLang/karamel
33-
34-
- name: Build krml (minimal)
35-
run: make -C karamel -skj$(nproc) minimal
36-
37-
# krml is a symlink to _build/default/src/Karamel.exe, but we want to exclude _build.
38-
# So, overwrite the link with the actual file.
39-
- name: Fix for symlink
40-
run: |
41-
cp --remove-destination $(realpath karamel/krml) karamel/krml
42-
43-
- uses: mtzguido/gci-upload@master
44-
with:
45-
name: karamel
46-
extra: --exclude=karamel/_build
47-
hometag: KRML
48-
49-
test-krml:
50-
runs-on: ubuntu-latest
51-
container: mtzguido/dev-base:v2
52-
if: false # No karamel test since it needs a full build (and Low*)
53-
needs:
54-
- build-krml
55-
steps:
56-
- name: Cleanup
57-
run: sudo find . -delete
58-
- run: echo "HOME=/home/user" >> $GITHUB_ENV
59-
- uses: mtzguido/set-opam-env@master
60-
61-
- uses: actions/download-artifact@v8
62-
with:
63-
name: fstar.tar.gz
64-
- run: tar -xzf fstar.tar.gz
65-
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
66-
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
67-
68-
69-
# krml test needs node
70-
- uses: actions/setup-node@v6
71-
with:
72-
node-version: 16
73-
74-
- uses: mtzguido/gci-download@master
75-
with:
76-
name: karamel
77-
78-
# node is needed for the wasm tests, skip them for now
79-
- name: Test
80-
run: make -C karamel -skj$(nproc) test
81-
8212
build-steel:
8313
runs-on: ubuntu-latest
8414
container: mtzguido/dev-base:v2
@@ -93,6 +23,7 @@ jobs:
9323
name: fstar.tar.gz
9424
- run: tar -xzf fstar.tar.gz
9525
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
26+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
9627
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
9728

9829
- name: Checkout steel
@@ -113,7 +44,6 @@ jobs:
11344
runs-on: ubuntu-latest
11445
container: mtzguido/dev-base:v2
11546
needs:
116-
- build-krml
11747
- build-steel
11848
steps:
11949
- name: Cleanup
@@ -126,12 +56,9 @@ jobs:
12656
name: fstar.tar.gz
12757
- run: tar -xzf fstar.tar.gz
12858
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
59+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
12960
- run: echo "OTHERFLAGS=--proof_recovery --z3version 4.15.3" >> $GITHUB_ENV
13061

131-
- uses: mtzguido/gci-download@master
132-
with:
133-
name: karamel
134-
13562
- uses: mtzguido/gci-download@master
13663
with:
13764
name: steel
@@ -143,7 +70,6 @@ jobs:
14370
runs-on: ubuntu-latest
14471
container: mtzguido/dev-base:v2
14572
needs:
146-
- build-krml
14773
- build-steel
14874
steps:
14975
- name: Cleanup
@@ -156,85 +82,19 @@ jobs:
15682
name: fstar.tar.gz
15783
- run: tar -xzf fstar.tar.gz
15884
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
85+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
15986
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
16087

161-
- uses: mtzguido/gci-download@master
162-
with:
163-
name: karamel
164-
16588
- uses: mtzguido/gci-download@master
16689
with:
16790
name: steel
16891

16992
- name: Test
17093
run: make -C steel -skj$(nproc) test
17194

172-
build-pulse:
173-
runs-on: ubuntu-latest
174-
container: mtzguido/dev-base:v2
175-
steps:
176-
- name: Cleanup
177-
run: sudo find . -delete
178-
- run: echo "HOME=/home/user" >> $GITHUB_ENV
179-
- uses: mtzguido/set-opam-env@master
180-
181-
- name: Checkout pulse
182-
uses: actions/checkout@master
183-
with:
184-
path: pulse/
185-
repository: FStarLang/pulse
186-
187-
- uses: actions/download-artifact@v8
188-
with:
189-
name: fstar.tar.gz
190-
- run: tar -xzf fstar.tar.gz
191-
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
192-
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
193-
194-
- name: Build (after setting up cargo env)
195-
run: . $HOME/.cargo/env && make -C pulse -skj$(nproc)
196-
197-
- uses: mtzguido/gci-upload@master
198-
with:
199-
name: pulse
200-
hometag: PULSE
201-
202-
test-pulse:
203-
runs-on: ubuntu-latest
204-
container: mtzguido/dev-base:v2
205-
needs:
206-
- build-krml
207-
- build-pulse
208-
steps:
209-
- name: Cleanup
210-
run: sudo find . -delete
211-
- run: echo "HOME=/home/user" >> $GITHUB_ENV
212-
- uses: mtzguido/set-opam-env@master
213-
214-
- uses: actions/download-artifact@v8
215-
with:
216-
name: fstar.tar.gz
217-
- run: tar -xzf fstar.tar.gz
218-
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
219-
220-
- uses: mtzguido/gci-download@master
221-
with:
222-
name: karamel
223-
224-
- uses: mtzguido/gci-download@master
225-
with:
226-
name: pulse
227-
228-
- name: Test
229-
run: . $HOME/.cargo/env && make -C pulse -skj$(nproc) test
230-
23195
build-everparse:
23296
runs-on: ubuntu-latest
23397
container: mtzguido/dev-base:v2
234-
if: false # Currently needs Low*
235-
needs:
236-
- build-krml
237-
- build-pulse
23898
steps:
23999
- name: Cleanup
240100
run: sudo find . -delete
@@ -251,33 +111,21 @@ jobs:
251111
name: fstar.tar.gz
252112
- run: tar -xzf fstar.tar.gz
253113
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
114+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
254115
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
255116

256-
- uses: mtzguido/gci-download@master
257-
with:
258-
name: karamel
259-
260-
- uses: mtzguido/gci-download@master
261-
with:
262-
name: pulse
263-
264-
# everparse expects PULSE_HOME to be the root of the installation,
265-
# not the root of the repo
266-
- run: echo "PULSE_HOME=$PULSE_HOME/out" >> $GITHUB_ENV
267-
268117
# everparse expects more environment variables to opt out of
269118
# in-tree dependencies
270119
- run: echo "EVERPARSE_USE_OPAMROOT=1" >> $GITHUB_ENV
271120
- run: echo "EVERPARSE_USE_FSTAR_EXE=1" >> $GITHUB_ENV
272-
- run: echo "EVERPARSE_USE_KRML_HOME=1" >> $GITHUB_ENV
273-
- run: echo "EVERPARSE_USE_PULSE_HOME=1" >> $GITHUB_ENV
121+
- run: echo "EVERPARSE_USE_KRML_EXE=1" >> $GITHUB_ENV
274122

275123
- name: Checkout everparse
276124
uses: actions/checkout@master
277125
with:
278-
path: everparse/
279-
ref: _nik_smt_univs_2025
280126
repository: project-everest/everparse
127+
path: everparse/
128+
ref: fstar2
281129

282130
- name: Build
283131
run: make -C everparse -skj$(nproc) all
@@ -290,7 +138,6 @@ jobs:
290138
test-everparse:
291139
runs-on: ubuntu-latest
292140
container: mtzguido/dev-base:v2
293-
if: false # Currently needs Low*
294141
needs:
295142
- build-everparse
296143
steps:
@@ -309,19 +156,9 @@ jobs:
309156
name: fstar.tar.gz
310157
- run: tar -xzf fstar.tar.gz
311158
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
159+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
312160
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
313161

314-
- uses: mtzguido/gci-download@master
315-
with:
316-
name: karamel
317-
318-
- uses: mtzguido/gci-download@master
319-
with:
320-
name: pulse
321-
# everparse expects PULSE_HOME to be the root of the installation,
322-
# not the root of the repo
323-
- run: echo "PULSE_HOME=$PULSE_HOME/out" >> $GITHUB_ENV
324-
325162
- uses: mtzguido/gci-download@master
326163
with:
327164
name: everparse
@@ -330,8 +167,15 @@ jobs:
330167
# in-tree dependencies
331168
- run: echo "EVERPARSE_USE_OPAMROOT=1" >> $GITHUB_ENV
332169
- run: echo "EVERPARSE_USE_FSTAR_EXE=1" >> $GITHUB_ENV
333-
- run: echo "EVERPARSE_USE_KRML_HOME=1" >> $GITHUB_ENV
334-
- run: echo "EVERPARSE_USE_PULSE_HOME=1" >> $GITHUB_ENV
170+
- run: echo "EVERPARSE_USE_KRML_EXE=1" >> $GITHUB_ENV
171+
172+
# Everparse test needs the DICE/DPE files from the F* repo.
173+
# Clone the repo here and point Everparse to it.
174+
- uses: actions/checkout@master
175+
with:
176+
path: /tmp/FStar
177+
submodules: true
178+
- run: echo "DICE_HOME=/tmp/FStar/pulse/share/pulse/examples/dice" >> $GITHUB_ENV
335179

336180
- name: Test
337181
# NOTE: We do not check against the expected C/Rust
@@ -343,7 +187,6 @@ jobs:
343187
runs-on: ubuntu-latest
344188
container: mtzguido/dev-base:v2
345189
needs:
346-
- build-krml
347190
- build-steel
348191
steps:
349192
- name: Cleanup
@@ -356,6 +199,7 @@ jobs:
356199
name: fstar.tar.gz
357200
- run: tar -xzf fstar.tar.gz
358201
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
202+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
359203
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
360204

361205
- name: Checkout steel
@@ -364,9 +208,6 @@ jobs:
364208
path: starmalloc/
365209
repository: Inria-Prosecco/starmalloc
366210

367-
- uses: mtzguido/gci-download@master
368-
with:
369-
name: karamel
370211
- uses: mtzguido/gci-download@master
371212
with:
372213
name: steel
@@ -390,6 +231,7 @@ jobs:
390231
name: fstar.tar.gz
391232
- run: tar -xzf fstar.tar.gz
392233
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
234+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
393235
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
394236

395237
- uses: actions/checkout@master
@@ -416,6 +258,7 @@ jobs:
416258
name: fstar.tar.gz
417259
- run: tar -xzf fstar.tar.gz
418260
- run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
261+
- run: echo "KRML_EXE=$(pwd)/fstar/bin/krml" >> $GITHUB_ENV
419262
- run: echo "OTHERFLAGS=--proof_recovery" >> $GITHUB_ENV
420263

421264
- uses: actions/checkout@master

0 commit comments

Comments
 (0)