Add check-docstrings to CI

[marsella]

I'm starting to make changes to interfaces that cascade down to multiple files and I'm less confident that I'm checking all the the properties in all the dependencies still work. I'd like to add a CI run that addresses this concern without being outrageously slow.

My ideal version would

1. Identify all the Cryptol files that changed
2. Recursively identify all files that depend on each changed file
3. Load and run :check-docstrings on each file in the set (1 + 2). In parallel, ideally.

I'm not sure what the best way to do 2 is. We have pretty well specified module path names so it might be as straightforward as grepping the whole repo for each file name. There are also some built-in tools that identify dependencies (:module-deps) for a given file, but we'd have to do that "in reverse" (that is, we want the files that depend on X, not the dependencies of X). There might be another way to use haskell / cryptol internals to get the dependency tree.

Related: #56.

• Choose an approach for this bit of CI
• Write all the scripts + yml files

[mccleeary-galois]

We also need to ensure that we are targeting the solvers that we ship with https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20240212 for now. More discussion across ecosystem as a whole needs to happen for solver versions in general.

[Isweet]

The concerns expressed by @marsella come up pretty often, and I wonder if it warrants revisiting and prioritizing work on a Cryptol build system and package manager. See, e.g., GaloisInc/cryptol#1334.

[Isweet]

The concerns expressed by @marsella come up pretty often, and I wonder if it warrants revisiting and prioritizing work on a Cryptol build system and package manager. See, e.g., GaloisInc/cryptol#1334.

It looks like @yav and @glguy are actively working on this, so maybe you can use it here when they merge the initial prototype. See: GaloisInc/cryptol#1526.