Coq Call 2024 03 19

• March 19th (back to Tuesday! (IINM)), 4pm UTC+1 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Unblocking #17393 (Allow require to load libraries from memory) [Emilio, 5 mins?]
• (postponed) Dangers of making env mutable see comment in #17674 [Emilio, 10 mins]
• Merging https://github.com/coq/coq/pull/18424 (remove vio) ? [Emilio, 10 mins?]
• (postponed) More cleanups (CoqIDE, async, side effects) [Emilio, 20 mins]
• fiat crypto legacy and CI (https://github.com/coq/coq/pull/18778) [Gaëtan, 10min]
• better support for submodules on CI #18736 [Jason, 1 min context + discussion (4--9 min?)]

notes

• attending: Jason Gross, Gaetan Gilbert, Emilio J. Gallego, Anton Danikin, Théo Zimmermann, Yves Bertot, Pierre Roux
• TZ: should we postpone some subjects
• EJG: well, they are already waiting for a month
• points 2 and 4 got postponed
• Unblocking #17393 (Allow require to load libraries from memory)
  • EJG: blocked on a review but unfortunately the said reviewer is not present to discuss it
  • GG: reviewed the PR, no strong opinion, would tend to accept along the principle that the author of the code gets to take the decisions
  • let's wait for Enrico to precise his request, GG (assignee) to write the conclusion of the discussion in the PR
• Merging https://github.com/coq/coq/pull/18424 (remove vio) ?
  • significant number of bugs "closed"
  • superseeded by vos now
  • maybe we could ask on zulip user channel if there is any vio user remaining
  • JG: isn't metacoq CI using it, GG: they are using vos
  • probably no need for deprecation phase
• fiat crypto legacy and CI (https://github.com/coq/coq/pull/18778)
  • 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:
      1. 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
      2. 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