Coq Call 2024 04 02

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

Topics

• CI workers [Gaëtan, ??min]
• Extraction and opaque proofs: https://github.com/coq/coq/pull/18851 (Emilio, 10 mins)
• Tracing tactics (Emilio, 10 mins)

Chairman: Secretary:

Notes

• issues about the inria "custom runner" https://gitlab.inria.fr/inria-ci/custom-runner/-/issues/28 https://gitlab.inria.fr/inria-ci/custom-runner/-/issues/29

• 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).