Generalize/strengthen build.sh

[sauclovian-g]

As discussed in #2060 there are more things we might want to have build.sh build, and also possibly other things we might want to have it do.

1. It should be able to build all the test assets as well as the "real" code, although perhaps not by default.
2. It should perhaps take an optional argument that tells it what to build.
3. At some level part of its purpose is to document the things that can be built (so casual users don't have to dig through cabal files to figure that out).
4. It should maybe also be able to run tests, or maybe there should be a separate script for that, or maybe it should get renamed so as to make the names of the actions it supports less ambiguous (e.g. "build.sh test" could reasonably build test assets, or run tests, but it can't do both)
5. The cry script in cryptol is analogous and it would probably be good to align these so moving from one context to the other isn't arbitrarily confusing or annoying.
6. There are some things the CI does by hand that could be usefully shifted into build.sh so all the CI has to do is run build.sh (this makes it easier for users to run the same things the CI does...)

This needs some discussion, or at least some design.

[sauclovian-g]

After prodding various things I've come to the conclusion that, unless I'm missing something, we should have a script that runs all the tests. There appear to be five cabal test suites, plus at least one other thing (the mr_solver tests) that is not run via cabal. Wading through the CI config to try to find all the tests is unfortunate (and also not very reliable).

I have no particular opinion on whether this should happen via build.sh test (akin to make test as often seen in make-based projects), via a separate test.sh, or something else (e.g. rename build.sh to make.sh or something like that).

However, since we also want to be able to build the test code, unless we decide that should just happen by default (I would be ok with that, there doesn't seem to be very much compared to the size of the whole tree) it should be clear and easy to remember what invocation builds the test code and what invocation runs the tests, without having to look it up or read the script or whatever.

[RyanGlScott]

After prodding various things I've come to the conclusion that, unless I'm missing something, we should have a script that runs all the tests.

Agreed.

I have no particular opinion on whether this should happen via build.sh test (akin to make test as often seen in make-based projects), via a separate test.sh, or something else (e.g. rename build.sh to make.sh or something like that).

My personal feeling is that having build.sh (for building code sans tests) and build.sh test (for running the tests) would be enough. This would mirror what Cryptol's cry and cry test currently do.

cry doesn't have a mode for building the test suite code without running it, but perhaps it should. We can start by prototyping something on the SAW side with build.sh. How about build.sh --enable-tests? That mirrors the cabal flag of the same name.

the mr_solver tests

This test suite is perhaps the odd one out, given that it's primarily Coq-based (via saw-core-coq) rather than primarily Haskell-based. It would be nice to offer a convenient way to run it, however, but we may need to think carefully about how we ensure that the necessarily prerequisites are installed. (This might intersect with ongoing work on dev scripts.)

[sauclovian-g]

Since I should have responded to the above long ago: given that the test code is small and builds pretty quickly, my inclination would be to just always build it and not create complications.

Meanwhile, another thought: while there are various reasons build.sh currently does git submodule update --init, I don't think it really belongs there; partly because downloading stuff should be a separate operation from building, but also because it's kind of ...rude for it to reset things on you if you're trying to build against a different version of a submodule for testing.

[RyanGlScott]

given that the test code is small and builds pretty quickly, my inclination would be to just always build it and not create complications.

I'm fine with that.

while there are various reasons build.sh currently does git submodule update --init, I don't think it really belongs there; partly because downloading stuff should be a separate operation from building, but also because it's kind of ...rude for it to reset things on you if you're trying to build against a different version of a submodule for testing.

I am inclined to agree with this. I've always found build.sh's habit of updating submodules to be annoying, and I often have to employ ugly workarounds to avoid this behavior from biting me.