CI should run cryptol-saw-core test suite

[brianhuffman]

In the current saw-script master, cabal test cryptol-saw-core on a local build fails:

cryptol-saw-core> test (suite: cryptol-saw-core-tc-test)

Loaded Cryptol.sawcore!


Translated Cryptol.cry!
cryptol-saw-core-tc-test: You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< ---------------------------------------------------
  Revision:  ed0d14aa85818be4eb258832115ed77348ea8846
  Branch:    master (uncommited files present)
  Location:  Unknown Cryptol primitive name
  Message:   PrimIdent (ModName "Float") "fpIsNaN"
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-9A2eRkdb6nHBNt2LU0ZEhm:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:628:29 in cryptol-saw-core-0.1-9A2eRkdb6nHBNt2LU0ZEhm:Verifier.SAW.Cryptol
%< ---------------------------------------------------


cryptol-saw-core> Test suite cryptol-saw-core-tc-test failed
Completed 2 action(s).
Test suite failure for package cryptol-saw-core-0.1
    cryptol-saw-core-tc-test:  exited with: ExitFailure 1
Logs printed to console

This test needs to be run in CI.

[brianhuffman]

Bisection shows that 1d2de81 is the first bad commit.

[RyanGlScott]

I agree that this should be tested somewhere, but isn't cryptol-saw-core located in the saw-core repo instead of saw-script?

[brianhuffman]

Yes, it is, and it should be run there too. (However, for that test to be well-defined there, we'll need to make cryptol into a submodule of saw-core, which is a whole different can of worms.)

But in any case, even if we had the relationship between saw-core and cryptol versions formalized as a git submodule, there's still no guarantee that the saw-script submodules pair up a version of cryptol-saw-core and a version of cryptol that are actually compatible with each other. (Merely being able to compile is really not enough; the cryptol-saw-core test suite ensures that the translator supports the full set of cryptol primitives with implementations of the appropriate types, and also checks the full set of implicit class instance rules from cryptol.) We'd still need to run the test for each saw-script PR.

This situation would be made rather simpler if we merged the saw-core repo into the saw-script repo, which I think we should do as soon as it's convenient.