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:

https://framadate.org/gtpksTqOKNOmLpws

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)