aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/README-developers.md21
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rw-r--r--doc/sphinx/changes.rst4
-rw-r--r--ide/idetop.ml12
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--stm/proofBlockDelimiter.ml24
-rw-r--r--stm/stm.ml59
-rw-r--r--stm/vernac_classifier.ml19
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--toplevel/vernac.ml13
-rw-r--r--vernac/g_vernac.mlg23
-rw-r--r--vernac/ppvernac.ml34
-rw-r--r--vernac/vernacentries.ml107
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacexpr.ml17
-rw-r--r--vernac/vernacprop.ml39
-rw-r--r--vernac/vernacprop.mli15
18 files changed, 217 insertions, 190 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 408d36df7f..9ed7180807 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -120,15 +120,18 @@ Currently available artifacts are:
Additionally, an experimental Dune build is provided:
https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev
-- the Coq documentation, built in the `doc:*` jobs. When submitting
- a documentation PR, this can help reviewers checking the rendered result:
-
- + Coq's Reference Manual [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
- + Coq's Standard Library Documentation [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base
- + Coq's ML API Documentation [master branch]
- https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc
+- the Coq documentation, built in the `doc:*` jobs. When submitting a
+ documentation PR, this can help reviewers checking the rendered
+ result. **@coqbot** will automatically post links to these
+ artifacts in the PR checks section. Furthemore, these artifacts are
+ automatically deployed at:
+
+ + Coq's Reference Manual [master branch]:
+ <https://coq.github.io/doc/master/refman/>
+ + Coq's Standard Library Documentation [master branch]:
+ <https://coq.github.io/doc/master/stdlib/>
+ + Coq's ML API Documentation [master branch]:
+ <https://coq.github.io/doc/master/api/>
### GitLab and Windows
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index ad22c394d8..3923fea30e 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -56,14 +56,14 @@
# NB: stdpp and Iris refs are gotten from the opam files in the Iris
# and lambdaRust repos respectively.
-: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
+: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
-: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
+: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
: "${lambdaRust_CI_REF:=master}"
-: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}"
+: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
########################################################################
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 6ac55e7bf4..c591a1f1de 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -894,8 +894,8 @@ Standard Library
and other packages. They are still delimited by `%int` and `%uint`.
- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
- and `int31` are no longer available merely by `Require`ing the files
- that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax`
+ and `int31` are no longer available merely by :cmd:`Require`\ing the files
+ that define the inductives. You must :cmd:`Import` `Coq.Strings.String.StringSyntax`
(after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
`Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
`Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7c6fa8951b..7e55eb4d13 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [
["Printing";"Unfocused"];
["Diffs"]]
-let is_known_option cmd = match Vernacprop.under_control cmd with
+let is_known_option cmd = match cmd with
| VernacSetOption (_, o, OptionSetTrue)
| VernacSetOption (_, o, OptionSetString _)
| VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
(** Check whether a command is forbidden in the IDE *)
-let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
+let ide_cmd_checks ~last_valid { CAst.loc; v } =
let user_error s =
try CErrors.user_err ?loc ~hdr:"IDE" (str s)
with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
let info = Stateid.add info ~valid:last_valid Stateid.dummy in
Exninfo.raise ~info e
in
- if is_debug cmd then
+ if is_debug v.expr then
user_error "Debug mode not available in the IDE"
-let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
+let ide_cmd_warns ~id { CAst.loc; v } =
let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
- if is_known_option cmd then
+ if is_known_option v.expr then
warn "Set this option from the IDE menu instead";
- if is_navigation_vernac cmd || is_undo cmd then
+ if is_navigation_vernac v.expr || is_undo v.expr then
warn "Use IDE navigation instead"
(** Interpretation (cf. [Ide_intf.interp]) *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index d220058120..92a93489f4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -180,7 +180,7 @@ let is_proof_termination_interactively_checked recsl =
let classify_as_Fixpoint recsl =
Vernac_classifier.classify_vernac
- (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacFixpoint(NoDischarge, List.map snd recsl)}))
let classify_funind recsl =
match classify_as_Fixpoint recsl with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 798c62d549..6eb8c42d1d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
++ fnl () ++
msg
in
@@ -1532,7 +1532,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
++ fnl () ++
CErrors.print reraise
in
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 129444c3b3..a487799b74 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -77,17 +77,18 @@ include Util
(* ****************** - foo - bar - baz *********************************** *)
let static_bullet ({ entry_point; prev_node } as view) =
+ let open Vernacexpr in
assert (not (Vernacprop.has_Fail entry_point.ast));
- match Vernacprop.under_control entry_point.ast with
- | Vernacexpr.VernacBullet b ->
+ match entry_point.ast.CAst.v.expr with
+ | VernacBullet b ->
let base = entry_point.indentation in
let last_tac = prev_node entry_point in
crawl view ~init:last_tac (fun prev node ->
if node.indentation < base then `Stop else
if node.indentation > base then `Cont node else
if Vernacprop.has_Fail node.ast then `Stop
- else match Vernacprop.under_control node.ast with
- | Vernacexpr.VernacBullet b' when b = b' ->
+ else match node.ast.CAst.v.expr with
+ | VernacBullet b' when b = b' ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = of_bullet_val b }
| _ -> `Stop) entry_point
@@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+ recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)})
}
| `Not -> `Leaks
@@ -109,16 +110,17 @@ let () = register_proof_block_delimiter
(* ******************** { block } ***************************************** *)
let static_curly_brace ({ entry_point; prev_node } as view) =
- assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
+ let open Vernacexpr in
+ assert(entry_point.ast.CAst.v.expr = VernacEndSubproof);
crawl view (fun (nesting,prev) node ->
if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
- else match Vernacprop.under_control node.ast with
- | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+ else match node.ast.CAst.v.expr with
+ | VernacSubproof _ when nesting = 0 ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = unit_val }
- | Vernacexpr.VernacSubproof _ ->
+ | VernacSubproof _ ->
`Cont (nesting - 1,node)
- | Vernacexpr.VernacEndSubproof ->
+ | VernacEndSubproof ->
`Cont (nesting + 1,node)
| _ -> `Cont (nesting,node)) (-1, entry_point)
@@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+ recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof })
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 69dbebbc57..7f0632bd7c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -571,7 +571,7 @@ end = struct (* {{{ *)
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
- (match Vernacprop.under_control x with
+ (match x.CAst.v.Vernacexpr.expr with
| VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
| VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
| VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i
@@ -1054,9 +1054,9 @@ end = struct (* {{{ *)
end (* }}} *)
(* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
set_id_for_feedback ?route dummy_doc id;
- Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending
+ Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
@@ -1078,7 +1078,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t =
| _ -> false
in
(* XXX unsupported attributes *)
- let cmd = Vernacprop.under_control expr in
+ let cmd = expr.CAst.v.expr in
if is_filtered_command cmd then
(stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
else begin
@@ -1141,7 +1141,7 @@ end = struct (* {{{ *)
| { step = `Fork ((_,_,_,l),_) } -> l, false,0
| { step = `Cmd { cids = l; ctac } } -> l, ctac,0
| { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
- begin match Vernacprop.under_control expr with
+ begin match expr.CAst.v.expr with
| VernacUndo n -> [], false, n
| _ -> [],false,0
end
@@ -1171,7 +1171,7 @@ end = struct (* {{{ *)
if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
then undo_costly_in_batch_mode v;
try
- match Vernacprop.under_control v with
+ match v.CAst.v.expr with
| VernacResetInitial ->
Stateid.initial
| VernacResetName {CAst.v=name} ->
@@ -1532,7 +1532,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_qed_delay_proof ~st ~id:stop
- ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in
+ ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1683,7 +1683,7 @@ end = struct (* {{{ *)
*)
(* STATE We use the state resulting from reaching start. *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc (Proved (opaque,None)));
+ ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
`OK proof
end
with e ->
@@ -1977,13 +1977,14 @@ end = struct (* {{{ *)
let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
{ indentation; verbose; expr = e; strlen } : unit
=
- let e, time, batch, fail =
- let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function
- | VernacTime (batch,e) -> find ~time:true ~batch ~fail e
- | VernacRedirect (_,e) -> find ~time ~batch ~fail e
- | VernacFail e -> find ~time ~batch ~fail:true e
- | e -> CAst.make ?loc e, time, batch, fail) v in
- find ~time:false ~batch:false ~fail:false e in
+ let cl, time, batch, fail =
+ let rec find ~time ~batch ~fail cl = match cl with
+ | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl
+ | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl
+ | ControlFail :: cl -> find ~time ~batch ~fail:true cl
+ | cl -> cl, time, batch, fail in
+ find ~time:false ~batch:false ~fail:false e.CAst.v.control in
+ let e = CAst.map (fun cmd -> { cmd with control = cl }) e in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_fail ~st fail (fun () ->
(if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
@@ -2151,14 +2152,14 @@ let collect_proof keep cur hd brkind id =
| VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
| _ -> false in
let is_defined = function
- | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+ | _, { expr = e } -> is_defined_expr e.CAst.v.expr
&& (not (Vernacprop.has_Fail e)) in
let proof_using_ast = function
| VernacProof(_,Some _) -> true
| _ -> false
in
let proof_using_ast = function
- | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+ | Some (_, v) when proof_using_ast v.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail v.expr)) -> Some v
| _ -> None in
let has_proof_using x = proof_using_ast x <> None in
@@ -2167,14 +2168,14 @@ let collect_proof keep cur hd brkind id =
| _ -> assert false
in
let proof_no_using = function
- | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
+ | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v
| _ -> assert false in
let has_proof_no_using = function
| VernacProof(_,None) -> true
| _ -> false
in
let has_proof_no_using = function
- | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+ | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail v.expr))
| _ -> false in
let too_complex_to_delegate = function
@@ -2191,7 +2192,7 @@ let collect_proof keep cur hd brkind id =
let view = VCS.visit id in
match view.step with
| (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
- when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+ when too_complex_to_delegate x.expr.CAst.v.expr ->
`Sync(no_name,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
| `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
@@ -2212,7 +2213,7 @@ let collect_proof keep cur hd brkind id =
(try
let name, hint = name ids, get_hint_ctx loc in
let t, v = proof_no_using last in
- v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr;
+ v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr;
`ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
@@ -2235,7 +2236,7 @@ let collect_proof keep cur hd brkind id =
| _ -> false
in
match cur, (VCS.visit id).step, brkind with
- | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+ | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr
&& (not (Vernacprop.has_Fail x.expr)) ->
`Sync (no_name,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
@@ -2350,8 +2351,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
term.` could also fail in this case, however that'd be a bug I do
believe as proof injection shouldn't happen here. *)
let extract_pe (x : aast) =
- match Vernacprop.under_control x.expr with
- | VernacEndProof pe -> pe
+ match x.expr.CAst.v.expr with
+ | VernacEndProof pe -> x.expr.CAst.v.control, pe
| _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -2486,7 +2487,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x));
+ let control, pe = extract_pe x in
+ ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
@@ -2526,7 +2528,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let _st = match proof with
| None -> stm_vernac_interp id st x
| Some (proof, info) ->
- stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)
+ let control, pe = extract_pe x in
+ stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe
in
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
@@ -2873,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let queue =
if VCS.is_vio_doc () &&
VCS.((get_branch head).kind = `Master) &&
- may_pierce_opaque (Vernacprop.under_control x.expr)
+ may_pierce_opaque x.expr.CAst.v.expr
then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
@@ -2939,7 +2942,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
VCS.commit id (mkTransCmd x l true `MainQueue);
(* We can't replay a Definition since universes may be differently
* inferred. This holds in Coq >= 8.5 *)
- let action = match Vernacprop.under_control x.expr with
+ let action = match x.expr.CAst.v.expr with
| VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
| _ -> ReplayCommand x in
VCS.propagate_sideff ~action
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 5af576dad2..8d600c2859 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -202,18 +202,17 @@ let classify_vernac e =
try Vernacextend.get_vernac_classifier s l
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
- let rec static_control_classifier v = v |> CAst.with_val (function
- | VernacExpr (atts, e) ->
- static_classifier ~atts e
- | VernacTimeout (_,e) -> static_control_classifier e
- | VernacTime (_,e) | VernacRedirect (_, e) ->
- static_control_classifier e
- | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
- (* XXX why is Fail not always Query? *)
- (match static_control_classifier e with
+ let static_control_classifier ({ CAst.v ; _ } as cmd) =
+ (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (* XXX why is Fail not always Query? *)
+ if Vernacprop.has_Fail cmd then
+ (match static_classifier ~atts:v.attrs v.expr with
| VtQuery | VtProofStep _ | VtSideff _
| VtMeta as x -> x
| VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
- | VtStartProof _ | VtProofMode _ -> VtQuery))
+ | VtStartProof _ | VtProofMode _ -> VtQuery)
+ else
+ static_classifier ~atts:v.attrs v.expr
+
in
static_control_classifier e
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index f37feb24de..78640334e2 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -340,8 +340,8 @@ let print_anyway_opts = [
let print_anyway c =
let open Vernacexpr in
- match c with
- | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts
+ match c.expr with
+ | VernacSetOption (_, opt, _) -> List.mem opt print_anyway_opts
| _ -> false
(* We try to behave better when goal printing raises an exception
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7a59a4dd12..e9d8263b85 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -20,14 +20,10 @@ open Vernacprop
Use the module Coqtoplevel, which catches these exceptions
(the exceptions are explained only at the toplevel). *)
-let checknav_simple ({ CAst.loc; _ } as cmd) =
- if is_navigation_vernac cmd && not (is_reset cmd) then
+let checknav { CAst.loc; v = { expr } } =
+ if is_navigation_vernac expr && not (is_reset expr) then
CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
-let checknav_deep ({ CAst.loc; _ } as cmd) =
- if is_deep_navigation_vernac cmd then
- CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
-
(* Echo from a buffer based on position.
XXX: Should move to utility file. *)
let vernac_echo ?loc in_chan = let open Loc in
@@ -60,7 +56,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
due to the way it prints. *)
let com = if state.time
then begin
- CAst.make ?loc @@ VernacTime(state.time,com)
+ CAst.map (fun cmd -> { cmd with control = ControlTime state.time :: cmd.control }) com
end else com in
let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
@@ -108,7 +104,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
(* Printing of AST for -compile-verbose *)
Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
- checknav_simple ast;
+ checknav ast;
let state =
Flags.silently (interp_vernac ~check ~interactive ~state) ast in
@@ -122,7 +118,6 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
iraise (e, info)
let process_expr ~state loc_ast =
- checknav_deep loc_ast;
interp_vernac ~interactive:true ~check:true ~state loc_ast
(******************************************************************************)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index fdf43196b0..8a94a010a0 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -72,16 +72,29 @@ let parse_compat_version = let open Flags in function
CErrors.user_err ~hdr:"get_compat_version"
Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
+(* For now we just keep the top-level location of the whole
+ vernacular, that is to say, including attributes and control flags;
+ this is not very convenient for advanced clients tho, so in the
+ future it'd be cool to actually locate the attributes and control
+ flags individually too. *)
+let add_control_flag ~loc ~flag { CAst.v = cmd } =
+ CAst.make ~loc { cmd with control = flag :: cmd.control }
+
}
GRAMMAR EXTEND Gram
GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
vernac_control: FIRST
- [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
- | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
- | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
- | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
- | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
+ [ [ IDENT "Time"; c = vernac_control ->
+ { add_control_flag ~loc ~flag:(ControlTime false) c }
+ | IDENT "Redirect"; s = ne_string; c = vernac_control ->
+ { add_control_flag ~loc ~flag:(ControlRedirect s) c }
+ | IDENT "Timeout"; n = natural; c = vernac_control ->
+ { add_control_flag ~loc ~flag:(ControlTimeout n) c }
+ | IDENT "Fail"; c = vernac_control ->
+ { add_control_flag ~loc ~flag:ControlFail c }
+ | v = decorated_vernac ->
+ { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ]
]
;
decorated_vernac:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 873a119e39..f91983d31c 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1268,6 +1268,16 @@ let string_of_definition_object_kind = let open Decls in function
| VernacEndSubproof ->
return (str "}")
+let pr_control_flag (p : control_flag) =
+ let w = match p with
+ | ControlTime _ -> keyword "Time"
+ | ControlRedirect s -> keyword "Redirect" ++ spc() ++ qs s
+ | ControlTimeout n -> keyword "Timeout " ++ int n
+ | ControlFail -> keyword "Fail" in
+ w ++ spc ()
+
+let pr_vernac_control flags = Pp.prlist pr_control_flag flags
+
let rec pr_vernac_flag (k, v) =
let k = keyword k in
let open Attributes in
@@ -1283,19 +1293,11 @@ let pr_vernac_attributes =
| [] -> mt ()
| flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
- let rec pr_vernac_control v =
- let return = tag_vernac v in
- match v.v with
- | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
- | VernacTime (_,v) ->
- return (keyword "Time" ++ spc() ++ pr_vernac_control v)
- | VernacRedirect (s, v) ->
- return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
- | VernacTimeout(n,v) ->
- return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
- | VernacFail v->
- return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
-
- let pr_vernac v =
- try pr_vernac_control v
- with e -> CErrors.print e
+let pr_vernac ({v = {control; attrs; expr}} as v) =
+ try
+ tag_vernac v
+ (pr_vernac_control control ++
+ pr_vernac_attributes attrs ++
+ pr_vernac_expr expr ++
+ sep_end expr)
+ with e -> CErrors.print e
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8712b8e958..4ae9d6d54f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2274,7 +2274,33 @@ let locate_if_not_already ?loc (e, info) =
| None -> (e, Option.cata (Loc.add_loc info) info loc)
| Some l -> (e, info)
-exception End_of_input
+let mk_time_header =
+ (* Drop the time header to print the command, we should indeed use a
+ different mechanism to `-time` commands than the current hack of
+ adding a time control to the AST. *)
+ let pr_time_header vernac =
+ let vernac = match vernac with
+ | { v = { control = ControlTime _ :: control; attrs; expr }; loc } ->
+ CAst.make ?loc { control; attrs; expr }
+ | _ -> vernac
+ in
+ Topfmt.pr_cmd_header vernac
+ in
+ fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
+
+let interp_control_flag ~time_header (f : control_flag) ~st
+ (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
+ match f with
+ | ControlFail ->
+ with_fail ~st (fun () -> fn ~st);
+ st.Vernacstate.lemmas
+ | ControlTimeout timeout ->
+ vernac_timeout ~timeout (fun () -> fn ~st) ()
+ | ControlTime batch ->
+ let header = if batch then Lazy.force time_header else Pp.mt () in
+ System.with_time ~batch ~header (fun () -> fn ~st) ()
+ | ControlRedirect s ->
+ Topfmt.with_output_to_file s (fun () -> fn ~st) ()
(* EJGA: We may remove this, only used twice below *)
let vernac_require_open_lemma ~stack f =
@@ -2635,7 +2661,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
-and interp_expr ?proof ~atts ~st c =
+and interp_expr ~atts ~st c =
let stack = st.Vernacstate.lemmas in
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
@@ -2665,6 +2691,8 @@ and interp_expr ?proof ~atts ~st c =
without a considerable amount of refactoring.
*)
and vernac_load ~verbosely fname =
+ let exception End_of_input in
+
(* Note that no proof should be open here, so the state here is just token for now *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
let fname =
@@ -2685,7 +2713,7 @@ and vernac_load ~verbosely fname =
try
let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
let stack =
- v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack })
+ v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
(parse_sentence proof_mode input) in
load_loop ~stack
with
@@ -2698,23 +2726,36 @@ and vernac_load ~verbosely fname =
CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
()
-and interp_control ?proof ~st v = match v with
- | { v=VernacExpr (atts, cmd) } ->
- let before_univs = Global.universes () in
- let pstack = interp_expr ?proof ~atts ~st cmd in
- if before_univs == Global.universes () then pstack
- else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack
- | { v=VernacFail v } ->
- with_fail ~st (fun () -> interp_control ?proof ~st v);
- st.Vernacstate.lemmas
- | { v=VernacTimeout (timeout,v) } ->
- vernac_timeout ~timeout (interp_control ?proof ~st) v
- | { v=VernacRedirect (s, v) } ->
- Topfmt.with_output_to_file s (interp_control ?proof ~st) v
- | { v=VernacTime (batch, cmd) }->
- let header = if batch then Topfmt.pr_cmd_header cmd else Pp.mt () in
- System.with_time ~batch ~header (interp_control ?proof ~st) cmd
-
+and interp_control ~st ({ v = cmd } as vernac) =
+ let time_header = mk_time_header vernac in
+ List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+ cmd.control
+ (fun ~st ->
+ let before_univs = Global.universes () in
+ let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+ if before_univs == Global.universes () then pstack
+ else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
+ ~st
+
+(* Interpreting a possibly delayed proof *)
+let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
+ let stack = st.Vernacstate.lemmas in
+ let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+ let () = match pe with
+ | Admitted ->
+ save_lemma_admitted_delayed ~proof ~info
+ | Proved (_,idopt) ->
+ save_lemma_proved_delayed ~proof ~info ~idopt in
+ stack
+
+let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } =
+ let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
+ List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+ control
+ (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+ ~st
+
+(* General interp with management of state *)
let () =
declare_int_option
{ optdepr = false;
@@ -2724,11 +2765,11 @@ let () =
optwrite = ((:=) default_timeout) }
(* Be careful with the cache here in case of an exception. *)
-let interp ?(verbosely=true) ~st cmd =
+let interp_gen ~verbosely ~st ~interp_fn cmd =
Vernacstate.unfreeze_interp_state st;
try vernac_timeout (fun st ->
let v_mod = if verbosely then Flags.verbosely else Flags.silently in
- let ontop = v_mod (interp_control ~st) cmd in
+ let ontop = v_mod (interp_fn ~st) cmd in
Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
Vernacstate.freeze_interp_state ~marshallable:false
) st
@@ -2738,18 +2779,10 @@ let interp ?(verbosely=true) ~st cmd =
Vernacstate.invalidate_cache ();
iraise exn
-let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t =
- let stack = st.Vernacstate.lemmas in
- let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
- try
- let () = match pe with
- | Admitted ->
- save_lemma_admitted_delayed ~proof ~info
- | Proved (_,idopt) ->
- save_lemma_proved_delayed ~proof ~info ~idopt in
- { st with Vernacstate.lemmas = stack }
- with exn ->
- let exn = CErrors.push exn in
- let exn = locate_if_not_already ?loc exn in
- Vernacstate.invalidate_cache ();
- iraise exn
+(* Regular interp *)
+let interp ?(verbosely=true) ~st cmd =
+ interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
+
+let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
+ interp_gen ~verbosely:false ~st
+ ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e618cdcefe..e65f9d3cfe 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -17,8 +17,8 @@ val interp_qed_delayed_proof
: proof:Proof_global.proof_object
-> info:Lemmas.Info.t
-> st:Vernacstate.t
- -> ?loc:Loc.t
- -> Vernacexpr.proof_end
+ -> control:Vernacexpr.control_flag list
+ -> Vernacexpr.proof_end CAst.t
-> Vernacstate.t
(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c15baf6157..d4b2029e99 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -415,12 +415,17 @@ type nonrec vernac_expr =
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
-type vernac_control_r =
- | VernacExpr of Attributes.vernac_flags * vernac_expr
+type control_flag =
+ | ControlTime of bool
(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)
- | VernacTime of bool * vernac_control
- | VernacRedirect of string * vernac_control
- | VernacTimeout of int * vernac_control
- | VernacFail of vernac_control
+ | ControlRedirect of string
+ | ControlTimeout of int
+ | ControlFail
+
+type vernac_control_r =
+ { control : control_flag list
+ ; attrs : Attributes.vernac_flags
+ ; expr : vernac_expr
+ }
and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 747998c6cc..903a28e953 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,47 +13,26 @@
open Vernacexpr
-let rec under_control v = v |> CAst.with_val (function
- | VernacExpr (_, c) -> c
- | VernacRedirect (_,c)
- | VernacTime (_,c)
- | VernacFail c
- | VernacTimeout (_,c) -> under_control c
- )
-
-let rec has_Fail v = v |> CAst.with_val (function
- | VernacExpr _ -> false
- | VernacRedirect (_,c)
- | VernacTime (_,c)
- | VernacTimeout (_,c) -> has_Fail c
- | VernacFail _ -> true)
+(* Does this vernacular involve Fail? *)
+let has_Fail { CAst.v } = List.mem ControlFail v.control
(* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let is_navigation_vernac_expr = function
+let is_navigation_vernac = function
| VernacResetInitial
| VernacResetName _
| VernacBack _ -> true
| _ -> false
-let is_navigation_vernac c =
- is_navigation_vernac_expr (under_control c)
-
-let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
- | VernacTime (_,c) -> is_deep_navigation_vernac c
- | VernacRedirect (_, c)
- | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
- | VernacExpr _ -> false)
-
(* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = CAst.with_val (function
- | VernacExpr ( _, VernacResetInitial)
- | VernacExpr (_, VernacResetName _) -> true
- | _ -> false)
+let is_reset = function
+ | VernacResetInitial
+ | VernacResetName _ -> true
+ | _ -> false
-let is_debug cmd = match under_control cmd with
+let is_debug = function
| VernacSetOption (_, ["Ltac";"Debug"], _) -> true
| _ -> false
-let is_undo cmd = match under_control cmd with
+let is_undo = function
| VernacUndo _ | VernacUndoTo _ -> true
| _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index 8875b86d94..320878e401 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -13,16 +13,9 @@
open Vernacexpr
-(* Return the vernacular command below control (Time, Timeout, Redirect, Fail).
- Beware that Fail can change many properties of the underlying command, since
- a success of Fail means the command was backtracked over. *)
-val under_control : vernac_control -> vernac_expr
-
val has_Fail : vernac_control -> bool
-
-val is_navigation_vernac : vernac_control -> bool
-val is_deep_navigation_vernac : vernac_control -> bool
-val is_reset : vernac_control -> bool
-val is_debug : vernac_control -> bool
-val is_undo : vernac_control -> bool
+val is_navigation_vernac : vernac_expr -> bool
+val is_reset : vernac_expr -> bool
+val is_debug : vernac_expr -> bool
+val is_undo : vernac_expr -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 08:58:50 +0000