I think we have done quite lot of progress on these items from a year ago:
Regarding Travis / GitHub Actions, I think it really makes sense to move the Nix support to GitHub Actions as well based on the experiments of @Cyril Cohen. Then, we may encourage GitHub Actions as the most recommended CI option.
I agree, the Actions CI seems most supported/convenient going forward, hopefully it can be reduced to a single line whether to build with OPAM or Nix in the Actions .yml file
What constitutes compositional extraction?
@Bas Spitters it just means that Dune knows about dependencies across Coq files and OCaml files, and will do the minimal work required to run coqc
and the OCaml compiler to produce a new (verified) program once a file is changed
Last updated: Mar 28 2024 at 18:02 UTC