Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add generation of Coq translator libraries to CI #1615

Merged
merged 11 commits into from
Mar 17, 2022
Merged

Add generation of Coq translator libraries to CI #1615

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
e9a6d78
added a step to the heapster-tests CI workflows to re-generate the Co…
Mar 16, 2022
eb36b72
removed generated Coq files from the repo; added logic to regenerate …
Mar 17, 2022
993c305
removed the no-longer needed saw generate_scaffolding.saw step from t…
Mar 17, 2022
2848803
added a step to explicitly generate the Coq files
Mar 17, 2022
df157eb
added a path to the saw generate_scaffolding.saw step in the CI
Mar 17, 2022
6a89b15
removing the generate_scaffolding step again...
Mar 17, 2022
7b0af72
changed ci.yml to be the same as on master...
Mar 17, 2022
1b209a8
re-added the CI step to explicitly generate the Coq scaffolding
Mar 17, 2022
3ac932b
updated Makefile comment per Kevin's suggestion
Mar 17, 2022
bdf35f2
added a mkdir command to the coq Makefile, and removed the generate_s…
Mar 17, 2022
45af7a6
fix blst test in CI... hopefully?
Mar 17, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,9 +267,10 @@ jobs:

- run: opam install -y coq=8.13.2 coq-bits=1.1.0

# FIXME: the following builds the Coq libraries for the SAW core
# to Coq translator; if we do other Coq tests, this should become
# its own build artifact, to avoid downloading it twice
# FIXME: the following steps generate Coq libraries for the SAW core to
# Coq translator and builds them; if we do other Coq tests, these steps
# should become their own build artifact, to avoid re-compiling the Coq
# libraries
- working-directory: saw-core-coq/coq
shell: bash
run: opam exec -- make -j
Expand Down
1 change: 1 addition & 0 deletions s2nTests/docker/blst.dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \
cd /workdir && \
git checkout 05d29b0e9d826053185e5bdba287045aab0b4669 && \
git config --file=.gitmodules submodule.blst.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.cryptol-specs.url https://github.com/GaloisInc/cryptol-specs && \
git submodule sync && \
git submodule update --init

Expand Down
26 changes: 19 additions & 7 deletions saw-core-coq/coq/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,25 @@
all: build
all: Makefile.coq

Makefile.coq: _CoqProject
coq_makefile -f $< -o $@

build: Makefile.coq
make -f Makefile.coq
include Makefile.coq
eddywestbrook marked this conversation as resolved.
Show resolved Hide resolved

clean: Makefile.coq
make -f Makefile.coq clean
# Set the SAW variable to the appropriate command. Always look in the path
# first, otherwise fall back on cabal run saw, unless running in CI because if
# saw is not in the path in CI then something else is terribly wrong and that
# should be an error
SAW=$(shell which saw)
ifeq ($(SAW),)
ifeq ($(CI),)
SAW=cabal run saw
else
$(error Could not find SAW executable; PATH = $(PATH))
endif
endif

%.vo: Makefile.coq
make -f Makefile.coq $@
generated/CryptolToCoq/SAWCorePrelude.v: ../../saw-core/prelude/Prelude.sawcore
(mkdir -p generated/CryptolToCoq; cd ../saw; $(SAW) generate_scaffolding.saw)

generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v: ../../cryptol-saw-core/saw/Cryptol.sawcore
(mkdir -p generated/CryptolToCoq; cd ../saw; $(SAW) generate_scaffolding.saw)
1 change: 1 addition & 0 deletions saw-core-coq/coq/generated/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
*.v
Loading