Coq Call 2024 04 02 - coq/coq GitHub Wiki

Topics

Chairman: Secretary:

Notes

  • attending: Emilio J Gallego Arias, Yves Bertot, Gaetan Gilbert, Guillaume Melquiond, Pierre-Marie Pédrot, Pierre Roux, Matthieu Sozeau

  • CI workers

    • sum up:
      • used to be on gitlab.com with free runners
      • they reduced the number of free minutes and it was no longer enough (even with light / full CI)
      • then Maxime set up something on INRIA gitlab custom runners, wasn't perfectly stable but was reasonnably OK
      • they changed the config so as to error instead of delaying jobs when lack of ressources -> all CI became red
      • used bench machines instead of INRIA custom runners (2 out of 4 machines we have, other 2 still used for benching, 6 parallel jobs / machine)
      • 12 parallel jobs are ok for our CI, probably on the edge
      • what next ? no news from INRIA CI team on custom runners, INRIA try to get more machines, we could wait
    • most time probably taken by fiat_crypto and unimath
    • no rule to add / remove things from CI
    • do we have a way to measure what is useful in CI to catch bugs ?
    • currently we are unable to rebuild the Docker image
      • we could use large INRIA CI runners to build it (works for Why3) would require tweaking our tags but probably feasible
    • EJGA: we could reduce amount of jobs (didn't understood how, maybe by merging multiple things in the same job to avoid the runner launching time) (Gaëtan: by merging the plugin jobs)
      • probably not that much to gain (1 min of loading per job)
      • but a lot of bandwidth (but remains inside INRIA's datacenter (Gaëtan: not sure about this, communication is between the bench machines somewhere in sophia and gitlab.inria.fr wherever it is))
    • memory is shared between jobs so fiat_crypto (very memory hungry) works aside light thing
    • should we buy more machines ?
      • comfort or difference between waiting a day or a few days to merge ? a night seems enough currently
      • probably no urgency

  • Extraction and opaque proofs: https://github.com/coq/coq/pull/18851

    • disable AccessOpaque by default
    • seems to work pretty well in CI
    • should be forbidden in tactics, maybe somewhat ok for now in commands if we deprecate it
    • seems we all agree to do it in 8.20
    • problemn still there in Compcert, bypassed by adding 20 "Extraction Constant" for things extraction want to extract whereas they are unused
      • no issue encountered with verified extraction
      • maybe the problemn is no longer there
      • we could check the history log of Compcert
    • we still need Print (for instance to debug tactics)

  • Tracing tactics

    • does that make any sense ?
    • approximation on tree of tactic calls works in 90% cases
    • what's the use case ? machine learning ? teaching ?
    • in "A; B", no intermediate point, would need higher order trees ? could execute A an arbitrary number of times because of backtrack that could come from B
    • the trace is a nightmarish higher order object
    • mostly prolog, although OCaml implemented tactic could do side effects
    • multiple use cases
      • unsound approximation
      • debug
    • in Lean they are able to show intermediate states in GUI because their tactic monad has no backtracking
    • difficulties with multigoal and distant side effect by unification
    • research subject: given an algebraic monad, what's the debug structure linked to that ? generic notion of callstack ?
    • [not mentioned during call, but added afterwards]: Jason Gross: I have a very old (from ~a decade ago) implementation of Trace here that stalled, IIRC, out only because I didn't have a good idea how to print traces. But, IIRC, it did faithfully record the entire trace, including backtracking (but not side effects of unification).