Rocq Call 2025 11 04 - rocq-prover/rocq GitHub Wiki

Topics

  • Rocq and async interruptions (E. J. Gallego Arias, cc #17266 , cc #19177, 30 min)
  • Rocq Platform progress update (Sylvain Borgogno, 5 minutes)
  • Update on Rocq with algebraic universes/variances/sort poly (Matthieu Sozeau, 15min)

Roles

  • Chairman: Nicolas Tabareau
  • Secretary:
  • Attending:

Notes

  • Attending: Sylvain Borgogno, Emilio Gallego Arias, Gaëtan Gilbert, Hugo Herbelin, Patrick Nicodemus, Pierre-Marie Pédrot, Pierre Roux, Matthieu Sozeau, Nicolas Tabareau, Gabriel Scherer

  • Rocq Platform progress update (Sylvain Borgogno, 5 minutes)

    • only 3 issues left open (gappa, coq-gappa and fiat-cryto)
    • updated to Rocq 9.0.1 (a few issues left with constraints = 9.0.0)
    • released expected next week
    • then starting 9.1
    • ideas to shorten the release delay (will set up a specific meeting to discuss this)
    • Nicolas: you could announce this on Zulip a specific meeting.
    • Sylvain: I'll try to make a roadmap for 9.1, so that maintainers see progress and are informed.

  • Rocq and async interruptions (E. J. Gallego Arias, cc #17266 , cc #19177, 30 min)

    • using memprof-limit in Rocq with Guillaume Munch, works surprisingly well and the documentation is excellent, thank you Guillaume.
    • longstanding problems with interruptions
    • demo by Emilio, He switches between files quickly, and the server is still responsive, even if some of the files have very long Qed times (for example). Sometimes there are crashes remaining
    • Emilio: #19177 helps but is not merged yet.
    • Emilio: but it is fairly easy to trigger races, and often we end up in a non-recoverable state. In the end I disabled the feature due to user complaints.
    • Emilio: it is hard to test this version. Either I forbid too many interruptions, and things get stuck somewhere, or I forbid too little and there are parts that get interrupted unsafely
    • Matthieu: what is the main source of crashes, data races?
    • Gaetan: can you open the diff of your PR and show one example that fixes a crash?
    • PMP: the problems you show us in the PR, they follow a similar pattern. Changes that are not atomic. Can you give me a specification when things should be fixed.
    • Guillaume (Munch-Maccagnoni): the issue is when you have an exception that arises in a place where the state is changing (could be inconsistent). The exception from the interruption should be programmed in such a way that it rolls back the state. The idea is to get rid of global state in the codebase, and instead expose primitives that deal with the cleanup. This is what Emilio did with his utils.
    • in case of exception, we need to be able to roll back the previous state
    • need to get rid of global states and expose primitives
    • Guillaume: I need to see better what happens. To me it's not an issue if you prevent interruptions for a while if it does not take too long. I need to see better, understand better your needs. If I understand correctly there are two topics, one is the Rocq core, and the other are the plugins that you don't have control over. The Rocq codebase can be fixed with some efforts, but what about plugins?
    • for plugins: they could declare themselves safe or not (default to unsafe)
    • but hard to know if things come from plugins
    • Gaetan, PMP: what if the plugin defines a Genarg intern, or a custom parsing rule? Random hooks? This form of containment is not practical. We cannot soundly approximate this.
    • Guillaume: we could look at code in the wild and work from concrete examples of things that are used today.
    • PMP: there are a few plugins in the CI that I would like to see out, but their developers pretend the code is fine. (I will not name names.)
    • Emilio: performance is affected by enabling this interruption method, so maybe this is conditional. It can be 3-4% depending on the sampling rate. (But then maybe we can get rid of polling, so this would be a win.) I think that having a flag to enable or disable it could be a good first step, so that people can experiment with it.
    • Guillaume: the 3-4% is before we start trying to improve performance, so we can optimize this and lower the cost.
    • Gaëtan in the way of making the Summary more functional, but will take a while, lot of work
    • conclusion: move towards merging the PR even if further work needed
    • slides with some pointers on rocq-lsp memprof-limits implementation: https://docs.google.com/presentation/d/1aoisY32raXwb8NXUL-9dadAPmvBAm2plpMP-bc2TdXs/edit?usp=sharing
    • example of error on Require Import Ltac2. after opening a few docs simultaneously. 
      Anomaly "The global environment cannot be accessed during the syntactic interpretation phase." Please report at 
http://rocq-prover.org/bugs/.%22

  • Update on Rocq with algebraic universes/variances/sort poly (Matthieu Sozeau, 15min)

    • still porting elpi and HB ti support polymorphic definitions, going relatively well (most problems on elpi side rather than algebraic universes in Rocq)
    • trie to complete formal proof of the algorithm and better understand it, almost done (max-plus algebra)
    • difference with the model in the original paper Z/N
    • trying to integrate in MetaRocq
    • still work remaining in optimizing (reducing number of universes), unclear on which API to provide, would require changes in pretyper
    • initial results seem to hint about already good improvement
    • try to port MathComp first to see if it works on such large development
    • depending on results, we may want to start a new Rocq 10 branch well in advance with algebraic univ and sort polymorphism (including new prelude/Corelib)
    • a bit of work to provide deprecation defs for sigT and the like
    • Nicolas: will we have the elimination-constraint branch merged soon? Then it should work even better.
    • discussions on development strategy: keeping a rocq10 branch (or rocq-next) on the side until it's ready enough to release
    • PMP: I can give my public comment about this. The one advantage of Rocq against Lean is that it is compatible with code from the past. We are literally sawing the branch we are sitting
      on by doing that. People may flock en masse to Lean if there is a difficult migration.
    • Pierre: if Rocq 10 is actually released when it is somewhat working, that could be a good strategy. For mathcomp 2, during two years we had two branches, and on the day we release mathc
      omp2 most of things were working.
    • Patrick: I'd like to see Coq more aggressive in getting new features. Every use of HoTT development would really like polymorphism, and elimination stuff.
    • Gabriel: would it be possible to have a core-next library and a separate library ecosystem on top of it, but it would work on the same Rocq release as the "current" stuff?
    • questions about compatibility layer? let's not add one more?
    • Nicolas: we can assume that the new corelib will be compatible with existing developments. The HoTT people are eager to try it.
    • Nicolas: when do you start the rocq-10 branch? Next week? Maybe you should merge the elimination-constraints stuff before? Can we announce for Christmas?