CoqWG20171003
This page is used to organize the next Coq Working Group (in French GT Coq). The framadate link to decide which day it will happen is:
The next Coq Working Group will take place on October 3rd and 4th at Inria Paris (2, rue Simone Iff). The room for the two days is Jacques-Louis Lions 1.
Streaming and recorded video will be available from M. Sozeau's YouTube channel: https://www.youtube.com/channel/UCgI_DseUNWbA9_tO88fyhoQ.
- 9:00 Coffee
- 10:00 8.7 debrief, recent evolution of the release management (T. Zimmermann and M. Dénès)
- 10:30 8.8 roadmap (M. Dénès)
- 11:00 Discussion on the future of tactics and SSReflect (T. Zimmermann)
- 12:00 Lunch
- 13:30 Strategic Priorities in Coq Development (E. Gallego)
- 14:00 PR discussion (part I)
- 19:00 Social event (TBA)
Some notes about this first day
- 9:00 Coffee
- 10:00 Coq Communities (E. Gallego)
- 11:00 Unifall status (M. Sozeau) Unifying Unifiers 2.pdf
- 11:30 Plan for the standard library (T. Zimmermann)
- 12:00 Lunch
- 13:30 Fun with template-coq (M. Sozeau) Fun with Template-Coq.pdf
- 14:00 Moving to GitHub issues (T. Zimmermann) Here is the link to my experiment: https://github.com/Zimmi48/bugzilla-test/
- 14:30 PR discussion (part II)
PR authors should get prepared to lead a quick discussion on each of them. Here is the list of the PRs we will try to discuss:
- Iff as a proper connective (herbelin)
- Experiment in bindings sumbool and sumor to sum (herbelin)
- Adding a flag to support different naming modes for evar hypotheses. (herbelin)
- Scoped options (ppedrot)
- Fix #4959: Ltac match fails to match Type with Type (maximedenes)
- Reducing temporary allocations in CClosure (ppedrot)
- An intropattern-style variant for split (herbelin)
- [pp] Optimized `Pp.t` gluing (ejgallego)
- Make some keywords into normal idents (SkySkimmer)
- [plugins] Remove Derive plugin. (ejgallego)
- Refine test for unresolved evars to be less sensitive to unification … (mattam82)
- mli-only files outside API (letouzey)
- Deprecate Proof term. (Zimmi48)
- an attempt to document known API problems (matejkosik)
- New strategy based on open scopes for deciding which notation to use among several of them (herbelin)
- Turning warning for deprecated notations on. (herbelin)
- Removing support for 8.5 compatibility. (herbelin)
- Fix rewrite in * side conditions (herbelin)
- New beta-iota compatibility refinements (herbelin)
- Handling evars in the VM (ppedrot)
- Uniformize references to Bugzilla (Zimmi48)
- Create checklist for pull requests. (Zimmi48)
- In printing, experimenting factorizing "match" clauses with same right-hand side. (herbelin)
- Miscellaneous extensions of notations (including granting BZ5585) (herbelin)
- intros '(x,y) (herbelin)
- Add HashConsing option (psteckler)
- changed statements of Rpower_lt and Rle_power and added lemmas (ybertot)
- Restore safety mechanisms on kernel names. (silene)
- Restoring test on ident validity while browsing directory structure. (herbelin)
- Iris CI: use opam to install dependencies (RalfJung)
- [general] Move declare to pretyping. (ejgallego)
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.