Skip to content

Commit 0eca60e

Browse files
committed
ci(verify-proofs): mkdir extracted/ before make (gitignored output dir)
extraction.v's [Extraction "extracted/filesystem.ml" ...] writes into the gitignored directory, which doesn't exist on a fresh CI clone. Add a one- line mkdir before the make step. Local fresh clone reproduces the issue without this fix.
1 parent 281128e commit 0eca60e

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

.github/workflows/validation.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,8 @@ jobs:
6262
- name: Build Coq proofs (oracle)
6363
working-directory: proofs/coq
6464
run: |
65+
# extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
66+
mkdir -p extracted
6567
coq_makefile -f _CoqProject -o Makefile
6668
make -j1
6769

0 commit comments

Comments
 (0)