currently marked as allow_error, which is awkward, we should either remove the mark or remove it alltogether
GG: doesn't seem very useful
JG: I remember it catching a bug that wasn't catched by anything else
EJG: In particular FCL was sensitive to changes in the proof engine / future goals stuff.
GG: can we afford to care about bugs that only appear in a legacy thing?
EJG: I'd be good to understand how FCL affects coverage
TZ: state of the CI? GG: we use 2 of the 4 bench machines for CI (because INRIA custom runners are unreliable), with 6 runners per machine (so 12 in total)
JG: would need a finer control on CI than just light/full CI, sometimes need to run a pair of job and end up running full CI
EJG: we could have three levels of CI with some heavy CI only run once a week
TZ: thing easy to implement: add a tier, other option: be fine with merging with not full CI
GG: not very optimistic on last option, we might end up loosing more time with it
JG: running after the fact seems bad: not clear whose responsibility it is to fix, might end up remaining broken for long time
GG: my idea was rather to just run it on the merge commit
GG: not clear testing after merge will end up saving a lot of time
could we run some light CI only when we have some insight that there could be a breakage?
but then if breakages happen often, we can no longer know if breakage doesn't come from a previous PR
and breakages probably happen too often for us
EJG: we could spend more money into more servers
GG: let's discuss that in a future Call
GG: mid term I would like for projects in CI to have a reason to be tested that doesn't apply to the whole world (unless we end up testing the whole world I guess)
YB: it's not black and white, it's a matter of cost/benefit ratio
better support for submodules on CI #18736
JG: lot of pain with submodules making fiat crypto overlays impossible in the past;
PR makes it seamless
PR: agree it's easier, disagree it's seamless
JG: would like to understand what's not seamless
as the PR is designed, the only differences between overlaying submodules vs other projects will be:
Determine the upstream repo and branch from the end of the project line rather than the middle; or determine them from the comment in the generated overlay file
Tell upstream to take care of merging not just the overlay but also of bumping submodules (but this should already be known by upstream)
EJG: I think for this particular PR, we should understand what problems are conceptual and what problems are with the concrete implementation
PR: would like to better understand why fiat_crypto development process looks so complicated
TZ: we seem to have two different dev process:
MIT way based on git submodules
others that use package managers like OPAM
JG: the development workflow with submodules looks like:
each project has development on the master branch
usually the master branches are compatible
dependabot automatically fast-forwards submodules when the CI shows that they are compatible
when the branches are incompatible, the CI stalls, and someone has to reconcile the branches
JG: [this explanation is elaborated in these notes, a much more condensed version was given verbally] the constraints that make this approach appealing at MIT PLV:
projects depend on each other but have different leads, sometimes only one part of a project depends on another one
don't want to block small coqutil PRs on a couple hours of fiat-crypto CI
don't want to block fiat-crypto PRs on the synthesis pipeline on resynchronizing separation logic infrastructure
projects have different priorities
coqutil is a small library, wants low CI overhead, ease of trying out new approaches
fiat-crypto depends on coqutil but is primarily targeting its non-Coq users; wants to maintain ease of installation for non-Coq users
so we want to be able to rapidly develop different projects asynchronously, and reconcile them a bit more lazily, while still having only a single branch of active development
PR: doesn't feel like a definitive solution but since the PR is already an improvement over the current situation, let's merge it