CoqWG20140131
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.
- 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'
-
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)
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.