Add generation of Coq translator libraries to CI

[eddywestbrook]

This PR adds a step to the heapster-tests CI workflows (which are the only workflows that use the Coq translator) to re-generate the Coq support libraries using the Coq translator. Currently, the Coq translator is not run during CI, and only the checked-in versions of the Coq support libraries are used by Coq tests.

[brianhuffman]

If the generated files are also going to be checked into the repo, then it would be nice for CI to compare the newly-generated files with the checked-in ones to ensure that they're the same. If they don't match, we should get a CI failure (and print the file diff in the CI log). How much work would it be to add this?

[eddywestbrook]

I'm not sure of the best way to compare the old and new versions of the generated Coq files, though you're right, it would make sense to compare them if they are going to be checked in. I guess an alternative is to not check in the auto-generated Coq files, because they are straightforward to generate. That's what we have done with other auto-generated artifacts. Thoughts?

[brianhuffman]

If any not-usually-installed-by-default external tools are required to generate files, then that would be a good reason to have copies of auto-generated files checked in. Or if you think there's a benefit from being able to view the files through the github web interface without having to clone the repo, that can also be a good reason to check in generated files. (E.g. this is why it's nice to check in generated pdf documentation.)

These .v files are just generated by running saw, if I understand correctly? It might make sense to remove the checked-in copies, because they shouldn't be too hard to generate locally. But I think it really depends on how convenient it is for you to leave them checked in. Our primary goal should be to save time and make things easier for us developers.

[eddywestbrook]

Well, it is nice to have them checked in, because a pull will just update them without the developer having to remember to regenerate them any time they pull. But I don't think there is a good way to check that the correct versions are checked in, and that seems sort of silly if we could just regenerate them in CI. The ideal situation would be to have the build system (cabal or maybe something else that calls cabal?) automatically regenerate them when needed. I.e., if Prelude.sawcore or Cryptol.sawcore changes, to rerun the saw generate_scaffolding.saw as part of the build process. No idea how to do this though...

[brianhuffman]

If there's no easy way to regenerate them automatically as needed by the Coq build system, then that's probably a good reason to keep them checked in. But in that case I think it's really important for the saw-script CI to ensure that the generated files are always the right ones and fail if they don't match.

[eddywestbrook]

Well, ok, we could probably build a Makefile that regenerates them automatically as needed. In fact, maybe that wouldn't be too hard.

[kquick]

The potential values of having CI generate the files are:

1. They are expensive or complicated to generate (which is not the case here)
2. You want to check that any changes in them can be generated successfully.
3. You want to verify that the generated output is correct.

I don't know if (2) is a concern and if (3) is even possible.

The developer support environment is not likely to be helped by the CI (unless the CI were to also check these back into the repo, which is not recommended for several reasons). The best way to support the developer environment is to cause these to be rebuilt as part of the normal build process.

If your normal build process is just cabal then you can have a custom Setup.hs that generates them for you.

If these are generated via some other method, perhaps there's a way to have the ingestion process simply look at the modified dates of the inputs and outputs and generate a warning if there's a modification time inversion or the outputs are missing (along with instructions on how t o rebuild).

[eddywestbrook]

Yeah, again, I'm just going to add to the Makefile already in the saw-core-coq/coq directory to tell it how to regenerate the generated Coq files if Prelude.sawcore or Cryptol.sawcore change. Then any Coq projects that use these files can call out to that Makefile in their Makefiles. That should be pretty automatic.

[eddywestbrook]

Ok, I have removed the generated Coq files from the repo, and added logic to the saw-core-coq/coq Makefile to regenerate them.

[kquick]

Could use rewording in the comment, but otherwise looks good!

[RyanGlScott]

The blst CI job failure is due to #1620. As a short-term workaround, can you try making this change?

diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile
index f04082c6..26bc8d63 100644
--- a/s2nTests/docker/blst.dockerfile
+++ b/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