diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 52 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 | ||||
| -rw-r--r-- | dev/doc/changes.md | 6 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 31 |
4 files changed, 74 insertions, 36 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 000f21c254..318562338d 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -6,19 +6,21 @@ This document describes how patches, submitted as pull requests (PRs) on the ## Code owners -The [CODEOWNERS](../../.github/CODEOWNERS) file describes, for each part of the -system, two owners. One is the principal maintainer of the component, the other -is the secondary maintainer. +The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of +the code. Sometime there is one principal maintainer and one or several +secondary maintainer(s). Sometimes, it is a team of code owners and all of its +members act as principal maintainers for the component. When a PR is submitted, GitHub will automatically ask the principal -maintainer for a review. If the PR touches several parts, all the -corresponding principal maintainers will be asked for a review. +maintainer (or the code owner team) for a review. If the PR touches several +parts, all the corresponding owners will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. -If a principal maintainer submits a PR that changes the component they own, they -must assign the secondary maintainer as reviewer. They should also do it if they -know they are not available to do the review. +If a principal maintainer submits a PR or is a co-author of a PR that is +submitted and this PR changes the component they own, they must request a +review from a secondary maintainer. They can also delegate the review if they +know they are not available to do it. ## Reviewing @@ -35,17 +37,29 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. -In all cases, maintainers can delegate reviews to the other maintainer of the -same component, except if it would lead to a maintainer reviewing their own -patch. +When a PR received lots of comments or if the PR has not been opened for long +and the assignee thinks that some other developers might want to comment, +it is recommended that they announce their intention to merge and wait a full +working day (or more if deemed useful) before the actual merge, as a sort of +last call for comments. + +In all cases, maintainers can delegate reviews to the other maintainers, +except if it would lead to a maintainer reviewing their own patch. A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. +When none of the maintainers have commented nor self-assigned a PR in a delay +of five working days, any maintainer of another component who feels comfortable +reviewing the PR can assign it to themselves. To prevent misunderstandings, +maintainers should not hesitate to announce in advance when they shall be +unavailable for more than five working days. + (*) In case a component is touched in a trivial way (adding/removing one file in a `Makefile`, etc), or by applying a systematic refactoring process (global renaming for instance) that has been reviewed globally, the assignee can -say in a comment they think a review is not required and proceed with the merge. +say in a comment they think a review is not required from every code owner and +proceed with the merge. ### Breaking changes @@ -54,7 +68,8 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or +the [`dev/doc/changes.md`](changes.md) file. If overlays are missing, ask the author to prepare them and label the PR with the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. @@ -78,9 +93,9 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis, you should connect using your GitHub account; -being part of the Coq organization on GitHub should give you the permission -to do so. +To restart a job on Travis or on AppVeyor, you should connect using your GitHub +account; being part of the Coq organization on GitHub should give you the +permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done using a GitHub account); if you are part of the [Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" @@ -93,9 +108,10 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR +is not a candidate for backporting), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. Don't use the GitHub interface to fix these conflicts. +to `master` directly. DON'T USE the GitHub interface to fix these conflicts. To merge the PR proceed in the following way ``` diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 91ab57f1e9..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to use Coq libraries. The provided `.ocamlinit` file does this automatically. +## ocamldebug + +You can use `ocamldebug` with Dune; after a build, do: + +``` +dune exec dev/dune-dbg +(ocd) source dune_db +``` + +or + +``` +dune exec dev/dune-dbg checker +(ocd) source dune_db +``` + +for the checker. Unfortunately, dependency handling here is not fully +refined, so you need to build enough of Coq once to use this target +[it will then correctly compute the deps and rebuild if you call the +script again] This will be fixed in the future. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/doc/changes.md b/dev/doc/changes.md index eb5b9ee1d3..b1fdfafd3a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -32,6 +32,12 @@ Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are deprecated. Use TYPED AS instead. +- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x + = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will + be bound with type `'a` in the expression, unlike the old system + where `atts : Vernacexpr.vernac_flags` was bound in the expression + and had to be manually parsed. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac223f..774552237a 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in |