From 9b75f255957fd917579dc3c342ece61a628972cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 17 Jul 2023 10:58:44 +0200 Subject: [PATCH 01/47] First draft of Coq roadmap based on initial discussion at CUDW 2023. --- text/069-coq-roadmap.md | 180 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 text/069-coq-roadmap.md diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md new file mode 100644 index 00000000..c29cada5 --- /dev/null +++ b/text/069-coq-roadmap.md @@ -0,0 +1,180 @@ +- Title: Coq roadmap + +- Drivers: Théo Zimmermann + +---- + +# Summary + +This CEP aims to establish a roadmap for the Coq project. +It highlights both: + +- what are considered as important axes to work on in the future, +- what resources are available to work on these axes, and which axes we commit + to work on based on these resources. + +Resources mean availability of persons to conduct the work. For technical axes, +requiring changes in the Coq system, it includes availability of persons to +review and merge the changes. + +# Motivation + +Producing a roadmap for the Coq project is important for several reasons: + +- It helps the community to know what to expect from the Coq project in the + future, in particular what changes can reasonably be expected to become + part of next releases, and what changes are more likely to be delayed + because of lack of resources. + +- It helps Coq developers to focus on important axes, and to be more + efficient, by making sure that their work will be supported by other + developers, including reviewers. + +- It helps contributors to know what are the important axes where their + contribution is most likely to be welcome and where they can expect + the most support from the Coq developers. + +- It helps highlighting the axes where more resources are needed, and + where the Coq project should try to find more resources. + +# Detailed design + +This roadmap is a consolidated view created by the Coq developers, based on +their shared understanding of the priorities of the project and of the +resources available to work on these priorities. It is completed by a +discussion with the community, as part of the CEP process. + +The fact that an item is part of the roadmap does not mean that its design +is already fixed, as design can be part of the work to be done. Therefore, +disagreement can still arise on such items, and may require to be resolved +through PR reviews, or through the CEP process. However, if an item is +part of the roadmap, it means that the Coq developers are committed to +work on it, and that they have resources available to do so, including the +reviews, so the work should not stall because of lack of resources or lack +of interest. + +Rules : + +- An item cannot be part of the roadmap if it is not supported by at least + two persons, including at least one Coq maintainer to review the changes. +- No one should be committed to work on more than two items at the same time. + +## Priorities and resources + +### Kernel, theory + +#### Sort polymorphism + +- Gaëtan Gilbert, Nicolas Tabareau +- 3 to 6 months + +#### Algebraic universes + +- Matthieu Sozeau, Pierre-Marie Pédrot +- 1 year + +#### Rewrite rules + +- Yann ?, Théo Winterhalter + +#### Primitive projections + +Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. + +### Surface language + +#### Ltac2 + +- Gaëtan Gilbert, Pierre-Marie Pédrot + +#### AST / interpretation + +- Emilio? (probably to remove because other Emilio commitments) + +#### Arbitrary recursive notations + +- Hugo Herbelin, Pierre Roux + +#### Bi-dimensional notations + +- Emilio Jésus Gallego Arias, ??? (missing buddy) + +#### Nametab / libobject + +- Emilio Jésus Gallego Arias, ??? (missing buddy) + +### Tools + +#### Proved extraction + +- Yannick Forster, Matthieu Sozeau +- 6 months to 1 year + +Would require work on: + +- Prop included in Type +- Module dependency analysis +- Hugo Herbelin + Yannick Forster + +### Libraries and community + +#### Promote the Coq Platform + +- Théo Zimmermann, ??? + +Editorial work + documentation + +## Other axes, without resources + +### Kernel, theory + +#### Observational type theory + +#### Global fixpoints + +#### Primitive projections + +- Removal of compatibility layer + +#### Sections + +#### Modules + +### Surface language + +#### Removing clenv + +#### Unifall + +#### Unification heuristics + +(improving evarconv) + +#### Support for async tactics + +#### Reactive elaboration + +#### Functionalisation + +### Libraries and community + +#### Demote stdlib + +- Separation of the prelude +- Make stdlib a normal library + +#### Tooling for building libraries + +(Coq universe) + +# Drawbacks + +Is the proposed change affecting any other component of the system? How? + +# Alternatives + +Yes, do the related works. What do other systems do? + +# Unresolved questions + +Questions about the design that could not find an answer. From 564fa10f6ed6bfdd0114bfd2fe9d3e15647007c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 17 Jul 2023 11:39:46 +0200 Subject: [PATCH 02/47] Edits after meeting with Nicolas. --- text/069-coq-roadmap.md | 63 +++++++++++++++++++++++++---------------- 1 file changed, 38 insertions(+), 25 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index c29cada5..a5c01be1 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -1,6 +1,6 @@ - Title: Coq roadmap -- Drivers: Théo Zimmermann +- Drivers: Théo Zimmermann (@Zimmi48) ---- @@ -53,12 +53,26 @@ work on it, and that they have resources available to do so, including the reviews, so the work should not stall because of lack of resources or lack of interest. +The description of each item of the roadmap will include the available +resources, the expected duration of the work, and the expected outcome, +including any blocking issues that will need to be resolved to complete +the work, and any still unresolved questions to be answered. + Rules : - An item cannot be part of the roadmap if it is not supported by at least two persons, including at least one Coq maintainer to review the changes. - No one should be committed to work on more than two items at the same time. +Each Coq Call will start with a roundtable about progress on items of the +roadmap. + +Gaëtan Gilbert will be the technical coordinator of the roadmap, overseeing +progress being made. + +Théo Zimmermann will be the editorial coordinator of the roadmap, proposing +to add and remove items, to reflect the evolution of the project. + ## Priorities and resources ### Kernel, theory @@ -87,22 +101,10 @@ Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. - Gaëtan Gilbert, Pierre-Marie Pédrot -#### AST / interpretation - -- Emilio? (probably to remove because other Emilio commitments) - #### Arbitrary recursive notations - Hugo Herbelin, Pierre Roux -#### Bi-dimensional notations - -- Emilio Jésus Gallego Arias, ??? (missing buddy) - -#### Nametab / libobject - -- Emilio Jésus Gallego Arias, ??? (missing buddy) - ### Tools #### Proved extraction @@ -116,15 +118,7 @@ Would require work on: - Module dependency analysis - Hugo Herbelin + Yannick Forster -### Libraries and community - -#### Promote the Coq Platform - -- Théo Zimmermann, ??? - -Editorial work + documentation - -## Other axes, without resources +## Other axes, without sufficient resources ### Kernel, theory @@ -142,6 +136,18 @@ Editorial work + documentation ### Surface language +#### AST / interpretation + +- Emilio? + +#### Bi-dimensional notations + +- Emilio Jésus Gallego Arias, ??? (missing buddy) + +#### Nametab / libobject + +- Emilio Jésus Gallego Arias, ??? (missing buddy) + #### Removing clenv #### Unifall @@ -158,6 +164,12 @@ Editorial work + documentation ### Libraries and community +#### Promote the Coq Platform + +- Théo Zimmermann, ??? + +Editorial work + documentation + #### Demote stdlib - Separation of the prelude @@ -169,12 +181,13 @@ Editorial work + documentation # Drawbacks -Is the proposed change affecting any other component of the system? How? +TODO # Alternatives -Yes, do the related works. What do other systems do? +TODO # Unresolved questions -Questions about the design that could not find an answer. +- How to update the roadmap? Should this CEP be updated, or should we create new CEPs every few months to produce a new roadmap? Should we +also maintain a wiki page with the roadmap, to cover the live progress? \ No newline at end of file From 07b78d00e5fbe8bc9cb8a04ee8a63bbd6c56799f Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Mon, 17 Jul 2023 12:41:58 +0200 Subject: [PATCH 03/47] add Yann Leray --- text/069-coq-roadmap.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a5c01be1..c3de674e 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,7 +89,8 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules -- Yann ?, Théo Winterhalter +- Yann Leray, Théo Winterhalter +- 3 to 6 month #### Primitive projections @@ -190,4 +191,4 @@ TODO # Unresolved questions - How to update the roadmap? Should this CEP be updated, or should we create new CEPs every few months to produce a new roadmap? Should we -also maintain a wiki page with the roadmap, to cover the live progress? \ No newline at end of file +also maintain a wiki page with the roadmap, to cover the live progress? From 03caa41383fb64da9ac0a40ea4c5d4f51234e480 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 17 Jul 2023 14:23:29 +0200 Subject: [PATCH 04/47] Add Nicolas to the CEP drivers. --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index c3de674e..dec524c5 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -1,6 +1,6 @@ - Title: Coq roadmap -- Drivers: Théo Zimmermann (@Zimmi48) +- Drivers: Nicolas Tabareau (@tabareau), Théo Zimmermann (@Zimmi48) ---- From a3d819427155e6091df924033505cceb13c10762 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Tue, 18 Jul 2023 17:16:23 +0200 Subject: [PATCH 05/47] Draft rewrite rules for 069-coq-roadmap.md --- text/069-coq-roadmap.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index dec524c5..122640db 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,6 +89,10 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules +The goal is to add (unsafe) user-defined rewrite rules. It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. + +- Working Coq fork: https://github.com/Yann-Leray/coq (examples in https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). +- CEP: https://github.com/coq/ceps/pull/50 - Yann Leray, Théo Winterhalter - 3 to 6 month From 35f6767a4ef51c88e87ffb569f8a9a08c5c32bcb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Wed, 19 Jul 2023 15:01:11 +0200 Subject: [PATCH 06/47] 069 coq roadmap: sell a bit more rewrite rules --- text/069-coq-roadmap.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 122640db..b7ee7bd6 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,7 +89,9 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules -The goal is to add (unsafe) user-defined rewrite rules. It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. +The goal is to add (unsafe) user-defined rewrite rules. This features allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq currently permits: non-linearity, overlapping left-hand sides (*eg* one can write an addition on natural numbers that reduces on both sides: `0 + n` and `n + 0` both reducing to `n`). + +It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. - Working Coq fork: https://github.com/Yann-Leray/coq (examples in https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). - CEP: https://github.com/coq/ceps/pull/50 From 0d72bfcc9545aa8d819c4b6ce0002f847ef5fbf6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Wed, 19 Jul 2023 15:40:15 +0200 Subject: [PATCH 07/47] Update text/069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index b7ee7bd6..a4b912c8 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -91,7 +91,7 @@ to add and remove items, to reflect the evolution of the project. The goal is to add (unsafe) user-defined rewrite rules. This features allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq currently permits: non-linearity, overlapping left-hand sides (*eg* one can write an addition on natural numbers that reduces on both sides: `0 + n` and `n + 0` both reducing to `n`). -It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. +It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should be supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. - Working Coq fork: https://github.com/Yann-Leray/coq (examples in https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). - CEP: https://github.com/coq/ceps/pull/50 From cb6f23fa1b409c784977a70132a73d93dc04628e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 1 Aug 2023 15:55:41 +0200 Subject: [PATCH 08/47] Splitting very long lines. Co-authored-by: Jim Fehrle --- text/069-coq-roadmap.md | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a4b912c8..aa149e47 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -89,11 +89,21 @@ to add and remove items, to reflect the evolution of the project. #### Rewrite rules -The goal is to add (unsafe) user-defined rewrite rules. This features allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq currently permits: non-linearity, overlapping left-hand sides (*eg* one can write an addition on natural numbers that reduces on both sides: `0 + n` and `n + 0` both reducing to `n`). - -It would be deactivated by default and be optionally on by *eg* setting `Rewrite Rules On`. They should be supported by unification and the main reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. - -- Working Coq fork: https://github.com/Yann-Leray/coq (examples in https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). +The goal is to add (unsafe) user-defined rewrite rules. This features allows +users to add computation rules to axioms which can be useful for prototyping. +It also allows for different kinds of computation rules with respect to what Coq +currently permits: non-linearity, overlapping left-hand sides (*eg* one can write +an addition on natural numbers that reduces on both sides: `0 + n` and `n + 0` +both reducing to `n`). + +It would be deactivated by default and be optionally on by *eg* setting +`Rewrite Rules On`. They should be supported by unification and the main +reduction machines (not `vm_compute` and `native_compute` for now, Coq +should give a warning when those are used with rewrite rules on). Rewrite +rules would propagate to any module that requires the module that defines them. + +- Working Coq fork: https://github.com/Yann-Leray/coq (examples in +https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). - CEP: https://github.com/coq/ceps/pull/50 - Yann Leray, Théo Winterhalter - 3 to 6 month From 1e56e11c748e72f2e01e8a851121493de750a64c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 4 Aug 2023 17:14:34 +0200 Subject: [PATCH 09/47] Add description of the promote platform / demote stdlib items. --- text/069-coq-roadmap.md | 48 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 4 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index aa149e47..62ad0f09 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -183,14 +183,54 @@ Would require work on: #### Promote the Coq Platform -- Théo Zimmermann, ??? +The Coq Platform is already the officially recommended installation method. +We would like to make it clear to users that they are encouraged to rely on +the packages that it provides, and that libraries in the Platform should be +generally considered as a collaborative extended standard library for Coq +(the historical stdlib being only a part of this). -Editorial work + documentation +As part of this effort we should do: + +- Editorial work for curation of packages included in the Coq Platform + (to bring guarantees on their level of quality). + +- Consolidation of documentation, so that it is easy for users to find + documentation about the included packages, ideally with a consistant + presentation. + +- Infrastructure / automation work to stabilize the release process of + the Coq Platform and ensure that releases are more consistently + delivered according to a predefined schedule. #### Demote stdlib -- Separation of the prelude -- Make stdlib a normal library +As part of the promotion effort around the Coq Platform, we would like to +ensure that the stdlib does not enjoy special status and that Coq can be +used without it. We should consider stdlib components as libraries to +advertise for their own values as part of the Coq Platform packages, but +without their historical origin, or their development and release process +being tied to Coq, (mis)leading users to consider them as the only +officially recommended libraries. + +In particular, we should: + +- Identify consistent stdlib components that can be used independently + from each other and that would be worth distributing as separate + packages. Identify their maintainers and give them freedom to define + the future of the components they maintain, in the limits set by the + Coq Platform charter. Allow maintainers to extract stdlib components + to maintain and evolve them outside the core Coq repository and to have + their own release schedule and versioning scheme, in case they wish to + do so. + +- Extract the prelude + a minimum set of components that alternative + general libraries like MathComp and coq-stdpp need as a basis. + Make sure that this reduced core stdlib component can evolve to allow + other libraries to use newer features of Coq (like universe polymorphism, + SProp and primitive projections). + Stop including any other stdlib components as part of the `coq` opam + package and encourage maintainers of Coq packages in other distributions + to do the same. #### Tooling for building libraries From 440b7cd7319782ca5577d67a86a76a529ea00aa5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 7 Aug 2023 11:58:34 +0200 Subject: [PATCH 10/47] Fix typo. Co-authored-by: Jim Fehrle --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 62ad0f09..fd9da62d 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -195,7 +195,7 @@ As part of this effort we should do: (to bring guarantees on their level of quality). - Consolidation of documentation, so that it is easy for users to find - documentation about the included packages, ideally with a consistant + documentation about the included packages, ideally with a consistent presentation. - Infrastructure / automation work to stabilize the release process of From ca1ccbf7da74a0849d7fd5bfaa885fb2a4a0f51b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 26 Sep 2023 16:27:48 +0200 Subject: [PATCH 11/47] Update 069-coq-roadmap.md (fixpoints and sections) --- text/069-coq-roadmap.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index fd9da62d..a402102a 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -141,7 +141,12 @@ Would require work on: #### Observational type theory -#### Global fixpoints +#### Fixpoints + +- Global fixpoints: Hugo less convinced of the importance of global fixpoints vs modifying the fix/cofix rules of CIC so that they unfold for named fixpoints on the name rather than the body of the fix +- Fixpoints able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR #17950), a few weeks +- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR #17986), a few weeks +- Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73) #### Primitive projections @@ -149,6 +154,8 @@ Would require work on: #### Sections +- Design of a way to refer to the generalized version of a constant/inductive from within the inside of a section + #### Modules ### Surface language From cb57a6d7bda7af9ba8a6f75c512364c5535a384b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Sep 2023 17:10:02 +0200 Subject: [PATCH 12/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a402102a..4c1d8fee 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -135,6 +135,22 @@ Would require work on: - Module dependency analysis - Hugo Herbelin + Yannick Forster +### Cleanup + +#### Retiring the STM, step 1 + +The objective of the first step is to have coqc and coqtop not depend on the STM, while keeping coqidetop, coqc-vio and coqc-vos depend on it. +Sub items: + +- fix the kernel w.r.t. side effects and code paths in the stm. That is revive https://github.com/coq/coq/pull/16367 +- `par:` implemented using SEL (already done in vscoqtop, to be ported to Coq). Currently `par:` does not use the STM, but uses its code to spawn workers, it depends on `-thread` etc. +- make coqc-vio and coqc-vos legacy binaries using the stm library + +Resources: + +- Enrico Tassi, ??? I need a code reviewer +- 1 month of work, 6 months timeframe + ## Other axes, without sufficient resources ### Kernel, theory From 641d53ad64130dec77e3bdeb99d55f69ea3d11f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Sep 2023 17:12:28 +0200 Subject: [PATCH 13/47] Update text/069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 4c1d8fee..0296f77b 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -143,7 +143,7 @@ The objective of the first step is to have coqc and coqtop not depend on the STM Sub items: - fix the kernel w.r.t. side effects and code paths in the stm. That is revive https://github.com/coq/coq/pull/16367 -- `par:` implemented using SEL (already done in vscoqtop, to be ported to Coq). Currently `par:` does not use the STM, but uses its code to spawn workers, it depends on `-thread` etc. +- `par:` implemented using [SEL](https://github.com/gares/sel) (already done in vscoqtop, to be ported to Coq). Currently `par:` does not use the STM, but uses its code to spawn workers, it depends on `-thread` etc. - make coqc-vio and coqc-vos legacy binaries using the stm library Resources: From 24406ffd3f3ee44378f1bc95098bf8f57863a0a0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 26 Sep 2023 17:13:27 +0200 Subject: [PATCH 14/47] Update 069-coq-roadmap.md Talk about the universe polymorphism roadmap --- text/069-coq-roadmap.md | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index fd9da62d..c33b3272 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -84,7 +84,27 @@ to add and remove items, to reflect the evolution of the project. #### Algebraic universes -- Matthieu Sozeau, Pierre-Marie Pédrot +The goal is to support arbitrary universes (e.g. max(u+k, l)) in any position, +while generalizing the constraint resolution system to support more complex constraints +(e.g. v <= max(u + k, l)). The inference and checking algorithms are quite different from +the current one and will be less performant by at least an order of magnitude on the current +developments that are mostly using global universes. It should however be competitive on +universe-polymorphic code (with much less universes and constraints to consider by definition). + +This should enable a more user-friendly interface to universe +polymorphism, by reducing the number of "dummy" generated universes and constraints that +are here only to deal with the current limitation. Also, we would get rid of the mandatory +"refresh_universes" on the Coq API side, allowing to freely use inferered types and terms +in tactics/tactic languages. + +On the user side this mostly adds an enriched language to describe universes with +n's and max(). +Small syntactic incompatibilities related to universe declarations (e.g `@{u v + | u <= v +}` change +to `@{u v ?| u <= v + 2 ?}`. + +- Matthieu Sozeau, Pierre-Marie Pédrot. Joint work with Marc Bezem on the constraint + inference/checking algorithms. +- CEP: todo +- PR: https://github.com/coq/coq/pull/16022 - 1 year #### Rewrite rules From 161d40bc5316567d3321c3ccc2720cca31ea8097 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 27 Sep 2023 16:35:34 +0200 Subject: [PATCH 15/47] Update 069-coq-roadmap.md for sort poly --- text/069-coq-roadmap.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a402102a..ef0d130f 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -81,6 +81,19 @@ to add and remove items, to reflect the evolution of the project. - Gaëtan Gilbert, Nicolas Tabareau - 3 to 6 months +- ongoing PR https://github.com/coq/coq/pull/17836 (will need a followup for inductives) + +Extension of universe polymorphism to sort qualities. It becomes possible to have global references quantified over +sort qualities eg `foo@{s | u | } : Type@{s | u}` which could be instantiated to `foo@{SProp | v} : SProp` +(the quantification syntax needs both `|` to avoid ambiguity). + +This should allow having for instance a common inductive for SProp, Prop and Type instantations of sigma types +(instead of the current `sigT` `sig` `ex` and variations depending on if each of the 2 parameters and the output are SProp). + +Eventually may allow using a common implementation for Type and Prop setoid rewriting machinery +(Morphisms vs CMorphisms, RelationClasses vs CRelationsClasses). + +May also be useful when doing Observational Type Theory. #### Algebraic universes From 8b9c8fdcbc660e14232b80c7b06e689f5eab07fe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Oct 2023 16:27:39 +0200 Subject: [PATCH 16/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 54e7334e..13a3ee80 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -181,7 +181,7 @@ Sub items: Resources: -- Enrico Tassi, ??? I need a code reviewer +- Enrico Tassi, Gaetan Gilbert - 1 month of work, 6 months timeframe ## Other axes, without sufficient resources From 22b6e7b98cd45a736e01a7f83e08597def0bbb1a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 4 Oct 2023 11:51:19 +0200 Subject: [PATCH 17/47] Add ressources to "move stdlib to coq-community" --- text/069-coq-roadmap.md | 67 +++++++++++++++++++++++------------------ 1 file changed, 37 insertions(+), 30 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 54e7334e..efb56753 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -184,6 +184,43 @@ Resources: - Enrico Tassi, ??? I need a code reviewer - 1 month of work, 6 months timeframe +### Libraries and community + +#### Move stdlib to coq-community + +As part of the promotion effort around the Coq Platform, we would like to +ensure that the stdlib does not enjoy special status and that Coq can be +used without it. We should consider stdlib components as libraries to +advertise for their own values as part of the Coq Platform packages, but +without their historical origin, or their development and release process +being tied to Coq, (mis)leading users to consider them as the only +officially recommended libraries. + +In particular, we should: + +- Identify consistent stdlib components that can be used independently + from each other and that would be worth distributing as separate + packages. Identify their maintainers and give them freedom to define + the future of the components they maintain, in the limits set by the + Coq Platform charter. Allow maintainers to extract stdlib components + to maintain and evolve them outside the core Coq repository and to have + their own release schedule and versioning scheme, in case they wish to + do so. + +- Extract the prelude + a minimum set of components that alternative + general libraries like MathComp and coq-stdpp need as a basis. + Make sure that this reduced core stdlib component can evolve to allow + other libraries to use newer features of Coq (like universe polymorphism, + SProp and primitive projections). + Stop including any other stdlib components as part of the `coq` opam + package and encourage maintainers of Coq packages in other distributions + to do the same. + +Resources: + +- Cyril Cohen, Pierre Roux +- 6 months to 1 year + ## Other axes, without sufficient resources ### Kernel, theory @@ -258,36 +295,6 @@ As part of this effort we should do: the Coq Platform and ensure that releases are more consistently delivered according to a predefined schedule. -#### Demote stdlib - -As part of the promotion effort around the Coq Platform, we would like to -ensure that the stdlib does not enjoy special status and that Coq can be -used without it. We should consider stdlib components as libraries to -advertise for their own values as part of the Coq Platform packages, but -without their historical origin, or their development and release process -being tied to Coq, (mis)leading users to consider them as the only -officially recommended libraries. - -In particular, we should: - -- Identify consistent stdlib components that can be used independently - from each other and that would be worth distributing as separate - packages. Identify their maintainers and give them freedom to define - the future of the components they maintain, in the limits set by the - Coq Platform charter. Allow maintainers to extract stdlib components - to maintain and evolve them outside the core Coq repository and to have - their own release schedule and versioning scheme, in case they wish to - do so. - -- Extract the prelude + a minimum set of components that alternative - general libraries like MathComp and coq-stdpp need as a basis. - Make sure that this reduced core stdlib component can evolve to allow - other libraries to use newer features of Coq (like universe polymorphism, - SProp and primitive projections). - Stop including any other stdlib components as part of the `coq` opam - package and encourage maintainers of Coq packages in other distributions - to do the same. - #### Tooling for building libraries (Coq universe) From 1ec6a9c8850f9eaabdd04fe4d18bc63a47a36b3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 4 Oct 2023 12:41:10 +0200 Subject: [PATCH 18/47] small explanation of the ltac2 item --- text/069-coq-roadmap.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index efb56753..433afe50 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -150,6 +150,9 @@ Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. #### Ltac2 - Gaëtan Gilbert, Pierre-Marie Pédrot +- long term + +The goal is to get to the point where we can recommend new developments be Ltac2 only (no Ltac1). #### Arbitrary recursive notations From 1ca6088088cda480d2d362ddb9af98ba071d216d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 4 Oct 2023 12:42:21 +0200 Subject: [PATCH 19/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 3c8efdb0..3ac73e3b 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -184,7 +184,7 @@ Sub items: Resources: -- Enrico Tassi, Gaetan Gilbert +- Enrico Tassi, Gaëtan Gilbert - 1 month of work, 6 months timeframe ### Libraries and community From 5ac7604f4d0c5686549c97385c69e2b6fcfb8012 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 5 Oct 2023 10:09:22 +0200 Subject: [PATCH 20/47] Revert title of "Demote stdlib" section --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 3ac73e3b..539fbd3c 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -189,7 +189,7 @@ Resources: ### Libraries and community -#### Move stdlib to coq-community +#### Demote stdlib As part of the promotion effort around the Coq Platform, we would like to ensure that the stdlib does not enjoy special status and that Coq can be From 20ec62f129946e9cde1919ef9ffc982d3d5c715c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 6 Oct 2023 14:53:02 +0200 Subject: [PATCH 21/47] Wording improvement. Co-authored-by: Jim Fehrle --- text/069-coq-roadmap.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 539fbd3c..e2d8ee0a 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -30,8 +30,8 @@ Producing a roadmap for the Coq project is important for several reasons: efficient, by making sure that their work will be supported by other developers, including reviewers. -- It helps contributors to know what are the important axes where their - contribution is most likely to be welcome and where they can expect +- It helps contributors to know in what areas their + contribution is likely to get the most support from the Coq developers. - It helps highlighting the axes where more resources are needed, and From cf2940526155e28b7018054fb1856132de19a6d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Oct 2023 21:49:55 +0200 Subject: [PATCH 22/47] Update 069-coq-roadmap.md Move fixpoints/section (except global fixpoints) to section with resources --- text/069-coq-roadmap.md | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index e2d8ee0a..66a043a2 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -141,6 +141,17 @@ https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule. - Yann Leray, Théo Winterhalter - 3 to 6 month +#### Guard condition + +- Guard condition able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR #17950), a few weeks for discussions and reviewing +- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR #17986), a few weeks for discussions and reviewing +- Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73), a few weeks depending on discussions +- Refinement of the guard condition through `match` constructs (PR #14359), a few weeks for discussions and reviewing + +#### Sections + +- Design of a way to refer to the generalized version of a constant/inductive from within the inside of a section (depends on the time needed to reach a consensus on the design) + #### Primitive projections Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. @@ -230,12 +241,9 @@ Resources: #### Observational type theory -#### Fixpoints +#### Global fixpoints -- Global fixpoints: Hugo less convinced of the importance of global fixpoints vs modifying the fix/cofix rules of CIC so that they unfold for named fixpoints on the name rather than the body of the fix -- Fixpoints able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR #17950), a few weeks -- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR #17986), a few weeks -- Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73) +- Hugo less convinced of the importance of global fixpoints vs modifying the fix/cofix rules of CIC so that they unfold for named fixpoints on the name rather than the body of the fix #### Primitive projections From 66f4a7ad7a7f5995011e4bb0eea73aa1ca25a76a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Oct 2023 22:04:25 +0200 Subject: [PATCH 23/47] Update 069-coq-roadmap.md Link to general recursive notations --- text/069-coq-roadmap.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 66a043a2..fd1ea3b5 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -165,7 +165,9 @@ Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. The goal is to get to the point where we can recommend new developments be Ltac2 only (no Ltac1). -#### Arbitrary recursive notations +#### General recursive notations + +The objective is to grant wish coq/coq#7959 (see there for details). - Hugo Herbelin, Pierre Roux From a51d5f4e303a3f37cf866db5816d5e888d623013 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 10 Oct 2023 14:30:55 +0200 Subject: [PATCH 24/47] Extend Ltac2 roadmap a bit. --- text/069-coq-roadmap.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index fd1ea3b5..2759dd05 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -160,11 +160,23 @@ Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. #### Ltac2 +The overarching goal is to get to the point where we can recommend new +developments to only use Ltac2 (without having to load Ltac1). There are several +fronts on which to make progress. + +One major point is to make available in Ltac2 all the basic tactics from Ltac1. +The main missing part is currently the ssreflect framework. Exposing it in Ltac2 +implies writing a good chunk of boilerplate binding code for the Ltac2-OCaml FFI +and defining the corresponding grammar rules for the Ltac2 language. + +Another important thing for extensibility is the table feature. One should be +able to define global tables with several kind of indices through a vernacular +and extend them after the fact. With this feature, mutable definitions are just +a specific case of tables with a unit index. + - Gaëtan Gilbert, Pierre-Marie Pédrot - long term -The goal is to get to the point where we can recommend new developments be Ltac2 only (no Ltac1). - #### General recursive notations The objective is to grant wish coq/coq#7959 (see there for details). From fa6d9a713847bfe16652b30712ab3936c54ca115 Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Tue, 10 Oct 2023 15:47:07 +0200 Subject: [PATCH 25/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 2759dd05..61272c4e 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -190,8 +190,9 @@ The objective is to grant wish coq/coq#7959 (see there for details). - Yannick Forster, Matthieu Sozeau - 6 months to 1 year -Would require work on: +Replacement of Coq's current extraction mechanism (implemented as an OCaml plugin) by a re-implementation from scratch based on MetaCoq (and thus implemented in Coq itself). This new extraction framework already supports *verified* type and proof erasure based on the intermediate language LambdaBox, several verified intermediate compilation steps, and extraction to OCaml cmx files via [Malfunction](github.com/stedolan/malfunction). The goal is to support unverified extraction to the current back-ends OCaml, Haskell, Scheme, and JSON. To fully replace the current extraction mechanism several parts of it have to be re-implemented, including mli generation as well as Haskell, Scheme, and JSON file generation. +Other aspects that need re-examination because they are problematic already in the current extraction mechanism include - Prop included in Type - Module dependency analysis - Hugo Herbelin + Yannick Forster From 770a30b3d86050016516b761095d5ce4657ec804 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 10 Oct 2023 16:10:53 +0200 Subject: [PATCH 26/47] Update 069-coq-roadmap.md with proper links to PRs --- text/069-coq-roadmap.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 2759dd05..d64c246b 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -143,10 +143,10 @@ https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule. #### Guard condition -- Guard condition able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR #17950), a few weeks for discussions and reviewing -- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR #17986), a few weeks for discussions and reviewing +- Guard condition able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR coq/coq#17950), a few weeks for discussions and reviewing +- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR coq/coq#17986), a few weeks for discussions and reviewing - Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73), a few weeks depending on discussions -- Refinement of the guard condition through `match` constructs (PR #14359), a few weeks for discussions and reviewing +- Refinement of the guard condition through `match` constructs (PR coq/coq#14359), a few weeks for discussions and reviewing #### Sections From ec59e93f792bab421c1bed63cd863cb4aa9b4eb5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Oct 2023 16:34:50 +0200 Subject: [PATCH 27/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index d64c246b..ff8928d8 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -174,7 +174,7 @@ able to define global tables with several kind of indices through a vernacular and extend them after the fact. With this feature, mutable definitions are just a specific case of tables with a unit index. -- Gaëtan Gilbert, Pierre-Marie Pédrot +- Gaëtan Gilbert, Pierre-Marie Pédrot, (Enrico Tassi for the SSR part) - long term #### General recursive notations From 15122d1516a7241339da82e616b91c645f148adf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 10 Oct 2023 16:36:41 +0200 Subject: [PATCH 28/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index ff8928d8..0b22b1ba 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -174,6 +174,8 @@ able to define global tables with several kind of indices through a vernacular and extend them after the fact. With this feature, mutable definitions are just a specific case of tables with a unit index. +`coqdoc` needs to understand Ltac2 (link to definitions, skip bodies). + - Gaëtan Gilbert, Pierre-Marie Pédrot, (Enrico Tassi for the SSR part) - long term From 9f3238d900489ea768e05e593073e48cbe9a020c Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Wed, 11 Oct 2023 09:23:54 +0200 Subject: [PATCH 29/47] add renaming Coq -> Rocq --- text/069-coq-roadmap.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 0b22b1ba..604ef5ff 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -75,6 +75,28 @@ to add and remove items, to reflect the evolution of the project. ## Priorities and resources +### Change of Name: Coq -> Rocq + +- Yves Bertot, Nicolas TAbareau +- 3 to 6 months + +The Coq developer team has validated the renaming of Coq into Rocq. There are several steps to make this happen. + +#### Legal issues + +We are checking that we can actually use the new name from a legal point of view. + +#### Visual identity and website + +The change of name is an opportunity to redesign the visual identity of Rocq +and to give a fresher look to the historical website of Coq. + +#### Technical issues + +On the technical issues, the renaming practically means a huge amount of search&replace +in many parts of the code base and website links. We may ask also for user contributions +for more peripherical changes. + ### Kernel, theory #### Sort polymorphism From 993481d0cac6862c66c02fbb0f6a5514f3e8d38f Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Wed, 11 Oct 2023 09:25:55 +0200 Subject: [PATCH 30/47] minor fixes --- text/069-coq-roadmap.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 604ef5ff..30fcbdea 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -75,9 +75,9 @@ to add and remove items, to reflect the evolution of the project. ## Priorities and resources -### Change of Name: Coq -> Rocq +### Change of Name: `Coq` -> `Rocq` -- Yves Bertot, Nicolas TAbareau +- Yves Bertot, Nicolas Tabareau - 3 to 6 months The Coq developer team has validated the renaming of Coq into Rocq. There are several steps to make this happen. From cbbc0cec279d70b47be955814da4cf6e70f340cb Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Wed, 11 Oct 2023 10:32:56 +0200 Subject: [PATCH 31/47] fix name --- text/069-coq-roadmap.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 30fcbdea..ef25b443 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -75,12 +75,13 @@ to add and remove items, to reflect the evolution of the project. ## Priorities and resources -### Change of Name: `Coq` -> `Rocq` +### Change of Name: `Coq` -> `The Rocq Prover` - Yves Bertot, Nicolas Tabareau - 3 to 6 months -The Coq developer team has validated the renaming of Coq into Rocq. There are several steps to make this happen. +The Coq developer team has validated the renaming of Coq into the Rocq Prover. +There are several steps to make this happen. #### Legal issues @@ -88,14 +89,14 @@ We are checking that we can actually use the new name from a legal point of view #### Visual identity and website -The change of name is an opportunity to redesign the visual identity of Rocq +The change of name is an opportunity to redesign the visual identity of the Rocq Prover and to give a fresher look to the historical website of Coq. #### Technical issues On the technical issues, the renaming practically means a huge amount of search&replace -in many parts of the code base and website links. We may ask also for user contributions -for more peripherical changes. +in many parts of the code base, website links, etc. We may ask for user contributions +for more peripherical changes, for instance on user contributions. ### Kernel, theory From eb86523ab02912effc22f470739bc865b53594df Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 11 Oct 2023 11:00:01 +0200 Subject: [PATCH 32/47] Promise a CEP to plan stdlib changes --- text/069-coq-roadmap.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index ef25b443..eb3b5d57 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -239,7 +239,7 @@ Resources: ### Libraries and community -#### Demote stdlib +#### Boost stdlib development As part of the promotion effort around the Coq Platform, we would like to ensure that the stdlib does not enjoy special status and that Coq can be @@ -269,6 +269,12 @@ In particular, we should: package and encourage maintainers of Coq packages in other distributions to do the same. +The technical details (prelude content, split into packages, logpath, +mono/multi repo, call for maintainers, documentation, test-suite, +CI,...) will be discussed in a [CEP](https://github.com/coq/ceps/) to +ensure a reasonnable agreement is reached on those points before +implementing any actual change. + Resources: - Cyril Cohen, Pierre Roux From fa1f1d5d7f3dfd065ce6d7973b63e4ec713edaa0 Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Wed, 11 Oct 2023 12:14:50 +0200 Subject: [PATCH 33/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 61272c4e..2af4c8ad 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -190,7 +190,7 @@ The objective is to grant wish coq/coq#7959 (see there for details). - Yannick Forster, Matthieu Sozeau - 6 months to 1 year -Replacement of Coq's current extraction mechanism (implemented as an OCaml plugin) by a re-implementation from scratch based on MetaCoq (and thus implemented in Coq itself). This new extraction framework already supports *verified* type and proof erasure based on the intermediate language LambdaBox, several verified intermediate compilation steps, and extraction to OCaml cmx files via [Malfunction](github.com/stedolan/malfunction). The goal is to support unverified extraction to the current back-ends OCaml, Haskell, Scheme, and JSON. To fully replace the current extraction mechanism several parts of it have to be re-implemented, including mli generation as well as Haskell, Scheme, and JSON file generation. +Alternative to Coq's current extraction mechanism (implemented as an OCaml plugin) by a re-implementation from scratch based on MetaCoq (and thus implemented in Coq itself). This new extraction framework already supports *verified* type and proof erasure based on the intermediate language LambdaBox, several verified intermediate compilation steps, and extraction to OCaml cmx files via [Malfunction](github.com/stedolan/malfunction). The goal is to support unverified extraction to the current back-ends OCaml, Haskell, Scheme, and JSON. To serve as a drop-in alternative to the current extraction mechanism several parts of it have to be re-implemented, including mli generation as well as Haskell, Scheme, and JSON file generation. Other aspects that need re-examination because they are problematic already in the current extraction mechanism include - Prop included in Type From 6b98014c55373b421fa78b8d28a08aa2eb1d9060 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Oct 2023 14:56:03 +0200 Subject: [PATCH 34/47] Update 069-coq-roadmap.md: docstrings --- text/069-coq-roadmap.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a3ea7f36..b26a8959 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -222,6 +222,13 @@ Other aspects that need re-examination because they are problematic already in t - Module dependency analysis - Hugo Herbelin + Yannick Forster +#### Attaching comments to declarations + +- Hugo Herbelin + ?? +- time needed to converge on the design + +PR [#18193](https://github.com/coq/coq/pull/18193) implements a table for binding comments to declarations, but it lacks surface syntax. + ### Cleanup #### Retiring the STM, step 1 From f8ebc9fcdc3ee812683a4c2cc1b8df2d45ccc9b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 24 Oct 2023 13:50:17 +0200 Subject: [PATCH 35/47] Restructure roadmap into short, medium and long term. With special focus on short term roadmap for now. --- text/069-coq-roadmap.md | 103 +++++++++++++++++++++++++++++++++------- 1 file changed, 85 insertions(+), 18 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index b26a8959..3dc77ae5 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -6,12 +6,14 @@ # Summary -This CEP aims to establish a roadmap for the Coq project. +This CEP aims to establish a short term roadmap for the Coq project (while +also stating the need for a medium and long term roadmap as well). + It highlights both: -- what are considered as important axes to work on in the future, -- what resources are available to work on these axes, and which axes we commit - to work on based on these resources. +- what are considered as priorities for the short term future, +- what priorities we commit to make progress on, based on the available + resources. Resources mean availability of persons to conduct the work. For technical axes, requiring changes in the Coq system, it includes availability of persons to @@ -26,19 +28,59 @@ Producing a roadmap for the Coq project is important for several reasons: part of next releases, and what changes are more likely to be delayed because of lack of resources. -- It helps Coq developers to focus on important axes, and to be more - efficient, by making sure that their work will be supported by other - developers, including reviewers. +- It helps Coq developers to choose priorities together, and to work more + efficiently toward those by making sure that their work will be supported + by other developers, including reviewers. -- It helps contributors to know in what areas their - contribution is likely to get - the most support from the Coq developers. +- It helps contributors to know in what areas their contribution is likely + to receive the most support from the Coq developers. -- It helps highlighting the axes where more resources are needed, and - where the Coq project should try to find more resources. +- It helps highlighting other priorities where progress is not possible for + lack of resources are needed, and where the Coq project should aim to find + more resources. # Detailed design +The Coq roadmap is declined at three levels: short, medium and long term. +Each of these levels address different needs, but they should be checked +for consistency with each other. + +- The short term roadmap is focused on priorities on which we are committed + to progress in the coming months and that are thus the most likely to + actually happen. We define a commitment from the Coq team as a commitment + of several (at least two) contributors, including at least one relevant + maintainer to review the work proposed by other contributors. The work + can include implementation work when the design is already clear, work on + the design from ideas that are well understood, or even exploratory work, + but we should only list the parts that are likely to converge in the + specified time-frame (i.e., if it is not clear if exploratory work will + lead to a solution that can be implemented, we should only commit on the + exploratory work). + +- The medium term roadmap is focused on areas where we see important progress + being needed, which could take several years to complete, and for which we + do not always have the ressources needed. It is used to guide the renewal + of the short term roadmap, but also the search for new resources to make + progress in these areas. The medium term roadmap should contains high level + descriptions of the areas requiring progress, but can contain rough plans + for how to proceed to make progress in these areas if the team already has a + vision about the steps needed. + +- The long term roadmap is focused on what our vision for the future of Coq is + and not necessarily how we are going to achieve it. It is used to provide + general ideas that we can check our medium and short term roadmaps against, + and to give users more clarity on what the future of Coq could look like. It + should include our vision of what kind of users Coq will target in the future. + +As creating a roadmap and keeping it updated and aligned with the actual goals +of the team members requires a change of culture, we do not try to create all +of these levels at the same time. In this CEP, we aim to produce a complete +short term roadmap, and to start a sketch of the medium term roadmap. We will +use our experience building the short term roadmap and keeping it up-to-date +to improve the process and to start building more precisely the other levels. + +## Detailed design for the short term roadmap + This roadmap is a consolidated view created by the Coq developers, based on their shared understanding of the priorities of the project and of the resources available to work on these priorities. It is completed by a @@ -73,7 +115,22 @@ progress being made. Théo Zimmermann will be the editorial coordinator of the roadmap, proposing to add and remove items, to reflect the evolution of the project. -## Priorities and resources +Once adopted through the CEP process, the roadmap will be kept up-to-date +in a living document on the wiki (while the merged step will represent a +point in time). From time to time, we will go back to using the CEP process +to trigger a discussion with the community on the updated roadmap (and also +to address more precisely the medium and long term levels of the roadmap). + +## Short term roadmap + +As this short term roadmap is focused on priorities for which we have +committed resources, it should not be considered as an exhaustive list of +the important aspects on which we hope Coq to progress in the future (more +can be found in the medium term roadmap). Rather, it gives clarity of what +should be the upcoming changes in the next releases. Yet, some changes may +still find their way in the next releases without being listed first in +this short term roadmap (although for significant changes, it would be +better if they would). ### Change of Name: `Coq` -> `The Rocq Prover` @@ -288,7 +345,9 @@ Resources: - Cyril Cohen, Pierre Roux - 6 months to 1 year -## Other axes, without sufficient resources +## Medium term roadmap + +TODO: clean up and restructure this part. ### Kernel, theory @@ -365,13 +424,21 @@ As part of this effort we should do: # Drawbacks -TODO +Creating and updating a roadmap requires significant work in itself. Our +view is that this work should be nonetheless useful by making the rest of +the work around Coq more efficient. # Alternatives -TODO +We could either do nothing, or try to coordinate work on selected topics +only, without creating a global overview and unified process. However, +experience leads us to believe that this global overview and unified +process is needed to create a shared understanding of the priorities of +the project and to make significant progress toward them. # Unresolved questions -- How to update the roadmap? Should this CEP be updated, or should we create new CEPs every few months to produce a new roadmap? Should we -also maintain a wiki page with the roadmap, to cover the live progress? +We leave many questions for future work, including the frequency of the +CEPs needed to update the roadmap, how the regular discussion of the work +on roadmap priorities will take place, and how to build the medium and +long term roadmap. From 99efed43786d784b960516afa893ead807e532a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 24 Oct 2023 15:49:12 +0200 Subject: [PATCH 36/47] fixup! Restructure roadmap Co-authored-by: Pierre Roux --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 3dc77ae5..326288e1 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -36,7 +36,7 @@ Producing a roadmap for the Coq project is important for several reasons: to receive the most support from the Coq developers. - It helps highlighting other priorities where progress is not possible for - lack of resources are needed, and where the Coq project should aim to find + lack of resources, and where the Coq project should aim to find more resources. # Detailed design From 8e062506dcea68707a3e4c4679ecca2400556adc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 24 Oct 2023 15:55:36 +0200 Subject: [PATCH 37/47] Fix typo. --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 326288e1..5595344b 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -202,7 +202,7 @@ to `@{u v ?| u <= v + 2 ?}`. #### Rewrite rules -The goal is to add (unsafe) user-defined rewrite rules. This features allows +The goal is to add (unsafe) user-defined rewrite rules. This feature allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq currently permits: non-linearity, overlapping left-hand sides (*eg* one can write From e622f78a657233824578d83b89d3da72961a1ad7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 26 Oct 2023 12:26:54 +0200 Subject: [PATCH 38/47] Add a paragraph about parsing --- text/069-coq-roadmap.md | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 5595344b..ccc23d60 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -259,12 +259,32 @@ a specific case of tables with a unit index. - Gaëtan Gilbert, Pierre-Marie Pédrot, (Enrico Tassi for the SSR part) - long term -#### General recursive notations - -The objective is to grant wish coq/coq#7959 (see there for details). +#### Notations - Hugo Herbelin, Pierre Roux +##### General recursive notations + +The objective is to grant wish [#7959](https://github.com/coq/coq/issues/7959) +(see there for details). + +##### Parsing + +We plan to remove the recovery mechanism of the camlp5/coqpp parsing +engine (see [#17876](https://github.com/coq/coq/pull/17876)). This +will make the parser simpler and easier to understand and will enable +to actually implement `no associativity`, which is currently just an +alias for `left associativity`. This should also pave the way to lift +the restriction that a same parsing level cannot be both left and +right associative, avoiding conflicts between libraries. See +[CEP 71](https://github.com/coq/ceps/pull/71) for more details. + +We will finally precise the design of a more liberal handling of +associativity levels, based on arbitrary strings and ordering +constraints (alike universe constraints) rather than the current 0 to +100 integers. This should ease combination of various libraries by +limiting the current conflicts on notations. + ### Tools #### Proved extraction From 8f5fef3735e6ffa908b8c2742a595bcd40b5afc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 7 Nov 2023 14:54:01 +0100 Subject: [PATCH 39/47] Wording improvements. Co-authored-by: Jim Fehrle --- text/069-coq-roadmap.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index ccc23d60..350e9388 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -41,7 +41,7 @@ Producing a roadmap for the Coq project is important for several reasons: # Detailed design -The Coq roadmap is declined at three levels: short, medium and long term. +The Coq roadmap is defined at three levels: short, medium and long term. Each of these levels address different needs, but they should be checked for consistency with each other. @@ -59,7 +59,7 @@ for consistency with each other. - The medium term roadmap is focused on areas where we see important progress being needed, which could take several years to complete, and for which we - do not always have the ressources needed. It is used to guide the renewal + do not always have the resources needed. It is used to guide the renewal of the short term roadmap, but also the search for new resources to make progress in these areas. The medium term roadmap should contains high level descriptions of the areas requiring progress, but can contain rough plans From 84ddd432ed4c561f594bffcca7b70b487a734c1f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 7 Nov 2023 15:36:24 +0100 Subject: [PATCH 40/47] Move things around and detail a bit more some aspects of the medium term roadmap. --- text/069-coq-roadmap.md | 159 ++++++++++++++++++++++------------------ 1 file changed, 89 insertions(+), 70 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index 350e9388..e304918b 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -104,7 +104,9 @@ Rules : - An item cannot be part of the roadmap if it is not supported by at least two persons, including at least one Coq maintainer to review the changes. -- No one should be committed to work on more than two items at the same time. +- No one should commit to more work than they can realistically undertake + at the same time (which will be a different amount depending on whether + someone can work full time on Coq or not). Each Coq Call will start with a roundtable about progress on items of the roadmap. @@ -171,12 +173,18 @@ This should allow having for instance a common inductive for SProp, Prop and Typ (instead of the current `sigT` `sig` `ex` and variations depending on if each of the 2 parameters and the output are SProp). Eventually may allow using a common implementation for Type and Prop setoid rewriting machinery -(Morphisms vs CMorphisms, RelationClasses vs CRelationsClasses). +(`Morphisms` vs `CMorphisms`, `RelationClasses` vs `CRelationsClasses`). May also be useful when doing Observational Type Theory. #### Algebraic universes +- Matthieu Sozeau, Pierre-Marie Pédrot. Joint work with Marc Bezem on the constraint + inference/checking algorithms. +- CEP: todo +- PR: https://github.com/coq/coq/pull/16022 +- 1 year + The goal is to support arbitrary universes (e.g. max(u+k, l)) in any position, while generalizing the constraint resolution system to support more complex constraints (e.g. v <= max(u + k, l)). The inference and checking algorithms are quite different from @@ -194,14 +202,14 @@ On the user side this mostly adds an enriched language to describe universes wit Small syntactic incompatibilities related to universe declarations (e.g `@{u v + | u <= v +}` change to `@{u v ?| u <= v + 2 ?}`. -- Matthieu Sozeau, Pierre-Marie Pédrot. Joint work with Marc Bezem on the constraint - inference/checking algorithms. -- CEP: todo -- PR: https://github.com/coq/coq/pull/16022 -- 1 year - #### Rewrite rules +- Working Coq fork: https://github.com/Yann-Leray/coq (examples in +https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). +- CEP: https://github.com/coq/ceps/pull/50 +- Yann Leray, Théo Winterhalter +- 3 to 6 month + The goal is to add (unsafe) user-defined rewrite rules. This feature allows users to add computation rules to axioms which can be useful for prototyping. It also allows for different kinds of computation rules with respect to what Coq @@ -215,49 +223,15 @@ reduction machines (not `vm_compute` and `native_compute` for now, Coq should give a warning when those are used with rewrite rules on). Rewrite rules would propagate to any module that requires the module that defines them. -- Working Coq fork: https://github.com/Yann-Leray/coq (examples in -https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). -- CEP: https://github.com/coq/ceps/pull/50 -- Yann Leray, Théo Winterhalter -- 3 to 6 month - -#### Guard condition - -- Guard condition able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR coq/coq#17950), a few weeks for discussions and reviewing -- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR coq/coq#17986), a few weeks for discussions and reviewing -- Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73), a few weeks depending on discussions -- Refinement of the guard condition through `match` constructs (PR coq/coq#14359), a few weeks for discussions and reviewing - -#### Sections - -- Design of a way to refer to the generalized version of a constant/inductive from within the inside of a section (depends on the time needed to reach a consensus on the design) - -#### Primitive projections - -Debate on the design to be had between Hugo Herbelin and Pierre-Marie Pédrot. - ### Surface language -#### Ltac2 +#### Make SSReflect available in Ltac2 -The overarching goal is to get to the point where we can recommend new -developments to only use Ltac2 (without having to load Ltac1). There are several -fronts on which to make progress. - -One major point is to make available in Ltac2 all the basic tactics from Ltac1. -The main missing part is currently the ssreflect framework. Exposing it in Ltac2 +The main missing tactics in Ltac2 are currently those of SSReflect. Exposing them in Ltac2 implies writing a good chunk of boilerplate binding code for the Ltac2-OCaml FFI and defining the corresponding grammar rules for the Ltac2 language. -Another important thing for extensibility is the table feature. One should be -able to define global tables with several kind of indices through a vernacular -and extend them after the fact. With this feature, mutable definitions are just -a specific case of tables with a unit index. - -`coqdoc` needs to understand Ltac2 (link to definitions, skip bodies). - -- Gaëtan Gilbert, Pierre-Marie Pédrot, (Enrico Tassi for the SSR part) -- long term +- Enrico Tassi and Pierre-Marie Pédrot #### Notations @@ -299,17 +273,13 @@ Other aspects that need re-examination because they are problematic already in t - Module dependency analysis - Hugo Herbelin + Yannick Forster -#### Attaching comments to declarations - -- Hugo Herbelin + ?? -- time needed to converge on the design - -PR [#18193](https://github.com/coq/coq/pull/18193) implements a table for binding comments to declarations, but it lacks surface syntax. - ### Cleanup #### Retiring the STM, step 1 +- Enrico Tassi, Gaëtan Gilbert +- 1 month of work, 6 months timeframe + The objective of the first step is to have coqc and coqtop not depend on the STM, while keeping coqidetop, coqc-vio and coqc-vos depend on it. Sub items: @@ -317,15 +287,13 @@ Sub items: - `par:` implemented using [SEL](https://github.com/gares/sel) (already done in vscoqtop, to be ported to Coq). Currently `par:` does not use the STM, but uses its code to spawn workers, it depends on `-thread` etc. - make coqc-vio and coqc-vos legacy binaries using the stm library -Resources: - -- Enrico Tassi, Gaëtan Gilbert -- 1 month of work, 6 months timeframe - ### Libraries and community #### Boost stdlib development +- Cyril Cohen, Pierre Roux +- 6 months to 1 year + As part of the promotion effort around the Coq Platform, we would like to ensure that the stdlib does not enjoy special status and that Coq can be used without it. We should consider stdlib components as libraries to @@ -360,24 +328,52 @@ CI,...) will be discussed in a [CEP](https://github.com/coq/ceps/) to ensure a reasonnable agreement is reached on those points before implementing any actual change. -Resources: - -- Cyril Cohen, Pierre Roux -- 6 months to 1 year - ## Medium term roadmap -TODO: clean up and restructure this part. +This part should be considered as a sketch, so not everything in there +is presented at the same level of detail yet. ### Kernel, theory +#### Streamline the use of `SProp` + +Short-term work on sort polymorphism should make it easier to adapt +all tactics and libraries so that `SProp` becomes actually usable. + +#### Guard condition + +There are several ways to make the guard condition evolve. Some +usability issues today could be lifted if they are properly +justified as not extending the theoretical set of functions that can +be defined. The guard condition could be made more flexible by +allowing to choose between a very safe mode, a normal / legacy mode, +an experimental / extended mode, and the disabled mode that can +already been set today. + +Here are some of the items that could possibly be worked on in the +relative short-term depending on availability of reviewers and +consensus on how to handle them: + +- Guard condition able to treat nested inductive types as mutual inductive types (recomputing the recursive structure dynamically), Hugo (PR coq/coq#17950), a few weeks for discussions and reviewing +- Guard condition able to detect uniform parameters of inner fixpoints, Hugo (PR coq/coq#17986), a few weeks for discussions and reviewing +- Expanded constructors of a branch in a `match` considered smaller for the guard condition (CEP #73), a few weeks depending on discussions +- Refinement of the guard condition through `match` constructs (PR coq/coq#14359), a few weeks for discussions and reviewing + +#### Sections + +- Design of a way to refer to the generalized version of a constant/inductive from within the inside of a section (depends on the time needed to reach a consensus on the design) + #### Observational type theory #### Global fixpoints - Hugo less convinced of the importance of global fixpoints vs modifying the fix/cofix rules of CIC so that they unfold for named fixpoints on the name rather than the body of the fix -#### Primitive projections +#### Streamline the use of primitive projections + +Some discussions still need to happen to create a precise plan on how to proceed. + +One item that is often discussed is the following: - Removal of compatibility layer @@ -389,17 +385,34 @@ TODO: clean up and restructure this part. ### Surface language -#### AST / interpretation +#### Ltac2 -- Emilio? +The overarching goal is to get to the point where we can recommend new +developments to only use Ltac2 (without having to load Ltac1). There are several +fronts on which to make progress. -#### Bi-dimensional notations +One major point is to make available in Ltac2 all the basic tactics from Ltac1. +The main missing part is currently the ssreflect framework. -- Emilio Jésus Gallego Arias, ??? (missing buddy) +Another important thing for extensibility is the table feature. One should be +able to define global tables with several kind of indices through a vernacular +and extend them after the fact. With this feature, mutable definitions are just +a specific case of tables with a unit index. -#### Nametab / libobject +`coqdoc` needs to understand Ltac2 (link to definitions, skip bodies). -- Emilio Jésus Gallego Arias, ??? (missing buddy) +#### Attaching comments to declarations + +- Hugo Herbelin + ?? +- time needed to converge on the design + +PR [#18193](https://github.com/coq/coq/pull/18193) implements a table for binding comments to declarations, but it lacks surface syntax. + +#### AST / interpretation + +#### Bi-dimensional notations + +#### Nametab / libobject #### Removing clenv @@ -415,6 +428,12 @@ TODO: clean up and restructure this part. #### Functionalisation +### Tools + +#### Remove CoqIDE + +See [068-coqide-split.md](068-coqide-split.md). + ### Libraries and community #### Promote the Coq Platform From f46000b21452d69710b17333386a59e48c2943a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 18 Dec 2023 10:32:00 +0100 Subject: [PATCH 41/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index e304918b..a8107ab8 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -162,7 +162,7 @@ for more peripherical changes, for instance on user contributions. #### Sort polymorphism - Gaëtan Gilbert, Nicolas Tabareau -- 3 to 6 months +- DONE (8.19) - ongoing PR https://github.com/coq/coq/pull/17836 (will need a followup for inductives) Extension of universe polymorphism to sort qualities. It becomes possible to have global references quantified over From 20a90fceb0d5ba11ef932fc3e68c202ed1b59182 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 6 Feb 2024 13:20:46 +0100 Subject: [PATCH 42/47] Link to stdlib CEP --- text/069-coq-roadmap.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index a8107ab8..fb6edad8 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -324,7 +324,7 @@ In particular, we should: The technical details (prelude content, split into packages, logpath, mono/multi repo, call for maintainers, documentation, test-suite, -CI,...) will be discussed in a [CEP](https://github.com/coq/ceps/) to +CI,...) will be discussed in this CEP: https://github.com/coq/ceps/pull/83 to ensure a reasonnable agreement is reached on those points before implementing any actual change. From 5487a1b66e9d511e0dd0983da3e015f70cb9a796 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 6 Feb 2024 13:26:29 +0100 Subject: [PATCH 43/47] Move parsing-recovery-mechanism removal to longer term --- text/069-coq-roadmap.md | 44 +++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 17 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index fb6edad8..cd3f91ac 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -242,23 +242,6 @@ and defining the corresponding grammar rules for the Ltac2 language. The objective is to grant wish [#7959](https://github.com/coq/coq/issues/7959) (see there for details). -##### Parsing - -We plan to remove the recovery mechanism of the camlp5/coqpp parsing -engine (see [#17876](https://github.com/coq/coq/pull/17876)). This -will make the parser simpler and easier to understand and will enable -to actually implement `no associativity`, which is currently just an -alias for `left associativity`. This should also pave the way to lift -the restriction that a same parsing level cannot be both left and -right associative, avoiding conflicts between libraries. See -[CEP 71](https://github.com/coq/ceps/pull/71) for more details. - -We will finally precise the design of a more liberal handling of -associativity levels, based on arbitrary strings and ordering -constraints (alike universe constraints) rather than the current 0 to -100 integers. This should ease combination of various libraries by -limiting the current conflicts on notations. - ### Tools #### Proved extraction @@ -401,6 +384,33 @@ a specific case of tables with a unit index. `coqdoc` needs to understand Ltac2 (link to definitions, skip bodies). +#### Parsing + +We plan to remove the recovery mechanism of the camlp5/coqpp parsing +engine (see [#17876](https://github.com/coq/coq/pull/17876)). This +will make the parser simpler and easier to understand and will enable +to actually implement `no associativity`, which is currently just an +alias for `left associativity`. This should also pave the way to lift +the restriction that a same parsing level cannot be both left and +right associative, avoiding conflicts between libraries. See +[CEP 71](https://github.com/coq/ceps/pull/71) for more details. + +A first step required in this direction is to enable declaring +notations at the same level than previous notations with a common +prefix, without knowing the said level. This will make it possible to +modify levels of notations without breaking backward compatibility +with their dependencies. Once this first step done, users will need +wait to require the Coq version implementing it, then use it to +finally enable changing levels of notations that currently use the +recovery mechanism. Fixing the levels of those notations will +eventually enable to remove the recovery mechanism. + +We will finally precise the design of a more liberal handling of +associativity levels, based on arbitrary strings and ordering +constraints (alike universe constraints) rather than the current 0 to +100 integers. This should ease combination of various libraries by +limiting the current conflicts on notations. + #### Attaching comments to declarations - Hugo Herbelin + ?? From a4a81c18a1a1f9c65b95131e70b6eaec59ad1ba7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 6 Feb 2024 13:29:46 +0100 Subject: [PATCH 44/47] Add people and timing to parsing task --- text/069-coq-roadmap.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index cd3f91ac..f266576e 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -386,6 +386,9 @@ a specific case of tables with a unit index. #### Parsing +- Hugo Herbelin, Pierre Roux +- 2 years + We plan to remove the recovery mechanism of the camlp5/coqpp parsing engine (see [#17876](https://github.com/coq/coq/pull/17876)). This will make the parser simpler and easier to understand and will enable From 43f96b1d3ac6642c8ad1daffbd6da769b6c77cec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 22 Feb 2024 13:27:22 +0100 Subject: [PATCH 45/47] Update 069-coq-roadmap.md --- text/069-coq-roadmap.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index f266576e..aeac322d 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -208,7 +208,7 @@ to `@{u v ?| u <= v + 2 ?}`. https://github.com/Yann-Leray/coq/blob/rewrite-rules/test-suite/success/rewrule.v). - CEP: https://github.com/coq/ceps/pull/50 - Yann Leray, Théo Winterhalter -- 3 to 6 month +- DONE (8.20) The goal is to add (unsafe) user-defined rewrite rules. This feature allows users to add computation rules to axioms which can be useful for prototyping. @@ -276,6 +276,7 @@ Sub items: - Cyril Cohen, Pierre Roux - 6 months to 1 year +- [CEP #83](https://github.com/coq/ceps/pull/83) As part of the promotion effort around the Coq Platform, we would like to ensure that the stdlib does not enjoy special status and that Coq can be @@ -323,6 +324,8 @@ is presented at the same level of detail yet. Short-term work on sort polymorphism should make it easier to adapt all tactics and libraries so that `SProp` becomes actually usable. +For tactics it's mostly a matter of waiting for bugs to be reported so we know what it broken. + #### Guard condition There are several ways to make the guard condition evolve. Some From 609c3b42659a103c08a5c7b80c29dd9e19273b48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 10 Sep 2024 16:47:37 +0200 Subject: [PATCH 46/47] update roadmap: remove sort poly (done), add template poly section --- text/069-coq-roadmap.md | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index aeac322d..ffa27694 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -159,23 +159,21 @@ for more peripherical changes, for instance on user contributions. ### Kernel, theory -#### Sort polymorphism +#### Template polymorphism -- Gaëtan Gilbert, Nicolas Tabareau -- DONE (8.19) -- ongoing PR https://github.com/coq/coq/pull/17836 (will need a followup for inductives) +- Gaëtan Gilbert, Pierre Maria Pédrot +- in progress (maybe done by 8.21) +- notably https://github.com/coq/coq/pull/19228 -Extension of universe polymorphism to sort qualities. It becomes possible to have global references quantified over -sort qualities eg `foo@{s | u | } : Type@{s | u}` which could be instantiated to `foo@{SProp | v} : SProp` -(the quantification syntax needs both `|` to avoid ambiguity). +Make template poly more usable and more robust, basing the metatheory on sort poly. -This should allow having for instance a common inductive for SProp, Prop and Type instantations of sigma types -(instead of the current `sigT` `sig` `ex` and variations depending on if each of the 2 parameters and the output are SProp). +TODO: -Eventually may allow using a common implementation for Type and Prop setoid rewriting machinery -(`Morphisms` vs `CMorphisms`, `RelationClasses` vs `CRelationsClasses`). - -May also be useful when doing Observational Type Theory. +- metatheory in metacoq (?) +- allow template univs which don't appear in the conclusion + (eg `u` in `eq : forall A:Type@{u}, A -> A -> Prop`) +- remove above-Prop restriction in template poly (?) +- I feel like I forgot something but can't remember what #### Algebraic universes From fcf08d088eaa7a696f8b1308d07cbc9d573dda60 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 26 Sep 2024 19:06:55 +0200 Subject: [PATCH 47/47] Fix various typos. --- text/069-coq-roadmap.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/069-coq-roadmap.md b/text/069-coq-roadmap.md index ffa27694..cdba9e87 100644 --- a/text/069-coq-roadmap.md +++ b/text/069-coq-roadmap.md @@ -42,7 +42,7 @@ Producing a roadmap for the Coq project is important for several reasons: # Detailed design The Coq roadmap is defined at three levels: short, medium and long term. -Each of these levels address different needs, but they should be checked +Each of these levels addresses different needs, but they should be checked for consistency with each other. - The short term roadmap is focused on priorities on which we are committed @@ -61,7 +61,7 @@ for consistency with each other. being needed, which could take several years to complete, and for which we do not always have the resources needed. It is used to guide the renewal of the short term roadmap, but also the search for new resources to make - progress in these areas. The medium term roadmap should contains high level + progress in these areas. The medium term roadmap should contain high level descriptions of the areas requiring progress, but can contain rough plans for how to proceed to make progress in these areas if the team already has a vision about the steps needed. @@ -118,7 +118,7 @@ Théo Zimmermann will be the editorial coordinator of the roadmap, proposing to add and remove items, to reflect the evolution of the project. Once adopted through the CEP process, the roadmap will be kept up-to-date -in a living document on the wiki (while the merged step will represent a +in a living document on the wiki (while the merged CEP will represent a point in time). From time to time, we will go back to using the CEP process to trigger a discussion with the community on the updated roadmap (and also to address more precisely the medium and long term levels of the roadmap).