search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.13k stars 122 forks source link

Reorganize CI taks #1471

Open yav opened 1 year ago

yav commented 1 year ago

As far as I understand, the current CI has the following steps:

  1. configure which sets up the general build environment
  2. build this builds a full Cryptol distribution, including documentation
  3. test this uses the package built in step 2, to run the tests

A drawback of this setup is that if there is a problem with building the documentation, we never get to run the tests. I think it'd be nicer to split up an reorganize the tasks, so that we get the following workflow:

  1. configure (same as before)
  2. build this should only build the Cryptol binary, without building documentation or generating release packages
  3. test run the tests, this should test the binary generated in step 2
  4. test-docs make sure that the examples used in the documentation have the expected results. This uses the results of (2) to validate the output, but could be run in parallel with (3)
  5. build-docs generate documentation: this runs the tools to generate the actual documentation (e.g., PDF). I am not 100% sure, but it is possible that this does not depend on any of the previous steps, so it could probably happen whenever. It would probably be OK to make this to depend on the outcome of (4) and only build the docs if the doc tests pass.
  6. build-release this depends on (2), (3), (4), and (5), and packages up the binaries, documentation, and other examples, to make a single distributable package. We need (2) and (5) to actually package it up, and (3) and (4) ensure that we don't make bad distributions.

EDIT: A note on parameters/matrix. GHC: We have a range of GHC versions we'd like to support OS: We have a bunch of OSes we'd like to support

Here is how the various steps depend on these:

  1. We want to build for all combinations of GHC and OS
  2. We want to test on all combinations of GHC and OS. The tests for a specific pair, only depend on the corresponding build pair
  3. This step probably only needs to be run with a single GHC version (the one to be used for release, see later) and a single OS
  4. This probably only needs to be run on a single OS, as the results are documents. I don't think it needs GHC at all.
  5. This needs to be built once per OS, but it can probably use the build from a single GHC version. This would be OK as long as the package only contains executables and not libraries.

EDIT: There are some more steps related to testing the rpc parts---if thesting the docs fails, this should not prevent running the normal tests.

RyanGlScott commented 1 year ago

This all sounds sensible to me. This also looks reasonably parallelizable, as (2), (3), (4), and possibly (5) can all run independently.