CoqWG20140905
This WG took place September 5th at PPS/Sophie Germain, 3rd floor, in the morning, from 10.30am to 13:30am, then, on an a less formal way during the afternoon.
Pierre Boutillier, Hugo Herbelin, Pierre-Marie Pédrot, Matthieu Sozeau, Bas Spitters, Arnaud Spiwack.
- Parsing issues: decision to parse <Type@%7Bu>} only when u is a reference to a universe; no parsing for things like <Type@%7BTop.17%7D>.
- Decision to wait for support from Benjamin Grégoire for supporting vm_compute on polymorphic definitions and from Maxime Dénès for supporting native_compute.
- checker still to adapt
Matthieu is going to introduce a primitive notion of types with projections for elimination, distinct from the inductive types based on pattern-matching. Decision to compile "match t as x with C y1..yn => t end" into "let x := t in let y1 := proj1 x in ... let yn := projn x in t"
The idea of providing a module Tactics.V82 which contains the 8.4 tactics.mli is discussed and seems to be the preferred one for leaving time to users for porting their tactics to the new engine.
Pierre Boutillier and Enrico Tassi converge on a similar procedure to release packages on Windows and MacOS, with eventually an ocaml compiler for building compatible plugins.
Hugo proposed a patch for naming evars by name, for printing instance and for being able to reparse evars with instances. Discussed syntax is "?id@[x:=t;y:=u]".
Discussions on giving the possibility of naming evars in refine and co is discussed. Possible notation is ?[id] to mean this is a hole to be named id.
Decision to expect the new cbn to replace simpl (with a flag to restore the old behavior of the name "simpl"). Tentative syntax will be "simpl delta_flag contextually_flag" with "delta_flag" being [cst1 ... cstn] or -[cst1 ... cstn] and contextually_flag being "cst" or "cst at occs".
- Discussion on having local definitions in evars instances or not? The historical motivation for that was: Consider the unification problem x':T, y':=phi(x'):U |- ?n[x:=x',y:=y'] == psi(y',x') where x:T, y:=phi(x):U |- ?n : V. Thanks to let-in in the instance, it is easy to invert the substitution and infer ?n = psi(y,x) rather than psi(y,phi(x')).
- Discussion on the semantics of the new Undo and Back in the state transition machine which. They are now document-level commands, i.e. saved as commands. However their semantics changed since they both undo the last command while before Undo was undoing the last tactic invocation and Back the last command. In particular, "Undo" after "Undo" undoes the effect of the first "Undo".
- Decision to unify the order of env and sigma in OCaml code: env first, then sigma.
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.