Merge pull request #1615 from GaloisInc/saw-core-coq/ci

Add generation of Coq translator libraries to CI

Author: mergify[bot]

.github/workflows/ci.yml

@@ -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

s2nTests/docker/blst.dockerfile

@@ -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
 

saw-core-coq/coq/Makefile

@@ -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
 
-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)

saw-core-coq/coq/generated/.gitignore

@@ -0,0 +1 @@
+*.v