Pierre Letouzey edited this page Oct 23, 2017 · 25 revisions


This WG happened january 31st at the 3rd floor of Sophie Germain at 9.30 (coffee at 9) and was followed by a bug squashing session in the afternoon.


The talks were recorded and are available here. (They would be put on a streaming platform as soon as someone ensures that everything is politically correct.)

  • Arnaud Spiwack: I'll try to give a talk about the new proof engine and how to develop with it.
  • Enrico Tassi: Short intro to .vi and .aux files. [RFC] .aux files (e.g. API for ltac)
  • Thomas Braibant: Poll results.

Talking points

  • We should review the situation for an alpha release of 8.5 (what's in, what will not be able to be in, schedule).
    • Current schedule: end of march for α, june for β, september for release (not decided on 9 vs 8.5)

    • What's in: what's currently in trunk + universe polymorphism + -R/-I fix (see below) + at least one hook for CoqMT as a plugin.

    • Official build environment for win32 and osx

      'Not discussed'

About -R/-I

Decision to use Guillaume's patch + -L for (recursive for now) loadpath for ML plugins. -I dir -as logical includes dir as logical, putting _nothing_ in the unqualified scope (i.e. an -I0).

Coq will now be using -I theories -as Coq -I plugins -as Coq -I user-contrib -L plugins (* for ML ) -L user-contrib ( for ML in user contribs *)

-R can still be useful localy to avoid prefixing inside developments (most common use). It's not recommended to use it to load external libraries though.

From Foo Import Bar Baz. -> Import Foo.Bar Foo.Baz. is integrated.


Decision to make ReleasedSSR and CompCert private. Optimal solution would be to share upstream repository (as a git on gforge for example) to collaboratively fix on Coq updates.

Reviewed failures of the test-suite, most due to output changes using the STM.


Decision to take the first steps to move the website and benchmarking under local control (with easy ssh access to the machines). The website should use Inria's existing infrastructure (T. Braibant mailed Roquencourt), the bench on our shiny new pyrolyse. Moving from bugzilla seems not so pressing, github's issue tracker might be too simple-minded (e.g. to do multi-bug changes)

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.