Build crux-mir-comp by default

[sauclovian-g]

Currently crux-mir-comp (and thus crucible-mir-comp) doesn't get built by build.sh, but only by the CI. This seems like a mistake; if nothing else it's annoying to have to do non-default builds to avoid CI failures when cleaning up or refactoring.

There's an extant issue (#1887) about running its test suite in the CI, which requires having mir-json installed. It doesn't appear necessary to have mir-json installed to just build it though.

[RyanGlScott]

Good catch.

I think it would be worth adopting a position on what exactly the build.sh script is intended to build:

• Should it build all of the executable components in the saw-script repo? If so, we should also build the exe:extcore-info and exe:verif-viewer components, which build.sh also does not cover at the moment.
• Should it build all of the test suite components? At the moment, it doesn't do this. Note that we do build the test suite components as part of the CI (see here), but this is nevertheless a separate code path from build.sh.

[sauclovian-g]

My thought is that since it's the documented way to build the tree, it should build the whole tree. So I'll add the other executables.

Re test components that could go either way. My instinct is that if you make a change with ramifications, and work through and fix everything so it all still builds again, and then the test code turns out not to compile, that this will at least be irritating and occasionally problematic (e.g. if you forget you need to get the tests built too and go on to the next breaking change) ... so I would vote for building all the test assets too. But if other people have other ideas I'm not super committed to that.

[sauclovian-g]

(also, how do you do that?)

[RyanGlScott]

(also, how do you do that?)

If you want to build (but not run) a test suite component, you can run cabal build test:<test-suite-name>. For instance, cabal build test:integration_tests will build SAW's integration test suite.

[RyanGlScott]

Writing down the results of a recent conversation with @sauclovian-g (and others) about the scope of the build.sh script:

1. It makes sense for build.sh to build all of the executable components in the saw-script repo. After all, if you wanted to build an individual component, you should just use the corresponding cabal build command (e.g., cabal build exe:saw).
2. One might wonder why we're bothering with a build.sh script in the first place if we can do everything that build.sh does with cabal commands. The reason is mainly for the sake of convenience: you could type out cabal build exe:saw exe:saw-remote-api exe:crux-mir-comp ... every time you wanted to build all of the executable components, but that would be tedious to run repeatedly. The build.sh script aims to automate some of this tedium, much like the cry script in the cryptol repo does.

3. It's conceivable that you might want to go beyond what build.sh currently does. For instance, you might want to build all of the executable components plus the test suite components (SAW's integration tests, the saw-core test suite, the saw-remote-api test suite, the Heapster test suite, etc.). You may want to do this plus run all of the tests. And so on. That being said, we couldn't come to a consensus on whether build.sh should do all of these by default.

   The way that the cry script handles this is by having different command-line options for different tasks. For instance, running cry build builds Cryptol, running cry test runs the Cryptol test suite, and so on. We agreed that it would be desirable to make SAW's build.sh script more like cry in this sense by adding different options for different workflows. (The exact design of these options remains to be worked out.)

2061 achieves the goal stated in (1), persuant to the vision laid out in (2). More work is required to achieve the goal stated in (3), however. I don't think we need to do this as part of #2061, however, so I'm fine with landing #2061 as-is. We should open a separate issue to implement the remaining work needed for (3), which can be under the purview of the MTV remediation effort.