CoqWG20140606
This WG took place June 6th at PPS/Sophie Germain, 3rd floor, in the morning, from 9.30am to noon (coffee at 9am) and continued in the afternoon.
If you intend to give a talk, please add your name and title here and any information you'd like to give.
- Carst Tankink, A Quick jEdit+Coq demo (15min). I'll give a quick demo of the adaptation of Isabelle/jEdit's codebase to work with Coq, to allow asynchronous proof authoring.
- Pierre Boutillier, Review and proposal about manpower organization in Coq. (10min + discussions)
- Pierre-Marie Pédrot, Less global, better multigoal, fewer by default, ... tactics (30 min)
- (Meta)data storage and installation (.glob, .aux, .cm*, .native, .o, .v, .vo, ...)
- SDK and precompiled plugins for 8.5
- Towards a bit more primitive notations for the standard library (e.g. for "existT", "exist", "proj1_sig", etc, for "S", for "eq_rect", for groupoid laws of equality, ...)? (not discussed)
- avoiding re-typing ltac bindings at use-time?
- Update on the migration of web/bugzilla/contribs, benchmarking tools
- release process, bug support policy
Frédéric Blanqui, Pierre Boutillier, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond, Matthieu Sozeau, Arnaud Spiwack, Carst Tankink, Enrico Tassi.
A nice presentation with features such as constants hyperlinked in the editing window, or intermediate subgoals printed when partially evaluating a 3-steps tactic such as "rewrite H1, H2, H3".
Discussion on completely separating the development of interfaces from the development of Coq; discussion on favoring adding new GUI extensions to CoqIDE, Jedit, PG, ...
Maxime asks about what to do with fixing guard for inductive and coinductive. At the current time, it is decided to go the safest way.
The idea is to move the parsing/pretting part of TACTIC EXTEND in ML files to "Tactic Notation"s in v-files. So, in TACTIC EXTEND, only lines of the form '"kwd" constr(c) ident(id)' are accepted, and used for interpreting Ltac expressions of the form "kwd c1 ipat:id".
Also, TACTIC EXTEND would produce arguments at the glob-level rather than at the type-level as now; it is the ml code which would be in charge of typing.
Patch is accepted.
Decision taken also to have the checker completely independent of the rest of the code (in particular this means having two univ.ml).
Pierre Letouzey explains that sometimes anomalies are caught. The policy is not to do such catching.
Matthieu proposed syntax "Type{foo}" for declaring an explicit universe level and <%22constant@%7Bfoo> bar}" for instantiation of universe parameter of a constant.
Discussion about the alternative <%22Type@%7Bfoo%7D%22>.
Xavier Clerc is working on using INRIA's Jenkins for compilation tests (see https://ci.inria.fr/coq)
pyrolyse.rocq.inria.fr is a host for heavy compilation
coq.rocq.inria.fr is a host for web server
Generated files .cm*, .native, .o are at the date of the WG in a hidden directory .coq-native and .aux are hidden files.
Long discussion which seems to converge toward having a non hidden directory "coq-build" local to each directory for all generated files except the .vi and.vo files.
Pull requests on coq github: being clearer on whether this repository is officially watched by coq developpers or not
No consensus found on "service" given to users
Discussion on making developments in Coq more visible world wide.
Reminder that a check-list file exists in coq-dev-tools/distrib/RELEASE to ensure optimal releasing process (to be updated though)
About the concrete point of checking consistency between the official and effective versions of ocaml required, it has been suggested to use Jenkins
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.