diff options
88 files changed, 570 insertions, 510 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d2e335d45..1814aaff1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -311,7 +311,7 @@ ci-hott: <<: *ci-template-vars EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" -ci-iris-coq: +ci-iris-lambda-rust: <<: *ci-template ci-math-classes: diff --git a/.travis.yml b/.travis.yml index c38038452..196f4b22a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -50,7 +50,7 @@ env: - TEST_TARGET="ci-flocq TIMED=1" - TEST_TARGET="ci-formal-topology TIMED=1" - TEST_TARGET="ci-hott TIMED=1" - - TEST_TARGET="ci-iris-coq TIMED=1" + - TEST_TARGET="ci-iris-lambda-rust TIMED=1" - TEST_TARGET="ci-math-classes TIMED=1" - TEST_TARGET="ci-math-comp TIMED=1" - TEST_TARGET="ci-sf TIMED=1" diff --git a/API/API.mli b/API/API.mli index 879323a37..a41009fa2 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1914,7 +1914,11 @@ module Summary : sig type frozen - type marshallable + + type marshallable = + [ `Yes (* Full data will be marshalled to disk *) + | `No (* Full data will be store in memory, e.g. for Undo *) + | `Shallow ] (* Only part of the data will be marshalled to a slave process *) type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -2060,7 +2064,8 @@ end module States : sig - val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b + type state + val with_state_protection : ('a -> 'b) -> 'a -> 'b end @@ -3713,7 +3718,7 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtBack of vernac_part_of_script * Stateid.t + | VtMeta | VtUnknown and vernac_qed_type = | VtKeep @@ -4512,6 +4517,9 @@ end module Proof_global : sig + + type state + type proof_mode = { name : string; set : unit -> unit ; @@ -5787,6 +5795,16 @@ end module Vernacentries : sig + + type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + val freeze_interp_state : Summary.marshallable -> interp_state + val unfreeze_interp_state : interp_state -> unit + val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5814,11 +5832,11 @@ end module Stm : sig type doc - type state val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] end (************************************************************************) @@ -15,10 +15,7 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. - The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see bug #148). This could be disabled via - Unset Omega UseLocalDefs. -- The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see bug #148). This could be disabled via + such as "x := 5 : Z" (see BZ#148). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. @@ -2397,7 +2394,7 @@ Tactics a registered setoid equality before starting to reduce in H. This is unlikely to break any script. Should this happen nonetheless, one can insert manually some "unfold ... in H" before rewriting. -- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101) +- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101) - "rewrite ... in" now accepts a clause as place where to rewrite instead of juste a simple hypothesis name. For instance: rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H @@ -2974,11 +2971,11 @@ Incompatibilities Bugs - Improved localisation of errors in Syntactic Definitions -- Induction principle creation failure in presence of let-in fixed (#238) -- Inversion bugs fixed (#212 and #220) -- Omega bug related to Set fixed (#180) -- Type-checking inefficiency of nested destructuring let-in fixed (#216) -- Improved handling of let-in during holes resolution phase (#239) +- Induction principle creation failure in presence of let-in fixed (BZ#238) +- Inversion bugs fixed (BZ#212 and BZ#220) +- Omega bug related to Set fixed (BZ#180) +- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216) +- Improved handling of let-in during holes resolution phase (BZ#239) Efficiency @@ -2991,18 +2988,18 @@ Changes from V7.3 to V7.3.1 Bug fixes - Corrupted Field tactic and Match Context tactic construction fixed - - Checking of names already existing in Assert added (PR#182) - - Invalid argument bug in Exact tactic solved (PR#183) - - Colliding bound names bug fixed (PR#202) - - Wrong non-recursivity test for Record fixed (PR#189) - - Out of memory/seg fault bug related to parametric inductive fixed (PR#195) + - Checking of names already existing in Assert added (BZ#182) + - Invalid argument bug in Exact tactic solved (BZ#183) + - Colliding bound names bug fixed (BZ#202) + - Wrong non-recursivity test for Record fixed (BZ#189) + - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195) - Setoid_replace/Setoid_rewrite bug wrt "==" fixed Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and - LetTac (PR#192) + LetTac (BZ#192) Changes from V7.2 to V7.3 ========================= diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2bc337028..db02f7834 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -4,13 +4,13 @@ Thank you for your interest in contributing to Coq! There are many ways to contr ## Bug Reports -Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue on the [Coq GitHub repository](https://github.com/coq/coq/issues) (you'll need a GitHub account). You can file a bug for any of the following: +Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue in the [Coq issue tracker](https://github.com/coq/coq/issues) (you'll need a GitHub account). You can file a bug for any of the following: - An anomaly. These are always considered bugs, so Coq will even ask you to file a bug report! - An error you didn't expect. If you're not sure whether it's a bug or intentional, feel free to file a bug anyway. We may want to improve the documentation or error message. - Missing documentation. It's helpful to track where the documentation should be improved, so please file a bug if you can't find or don't understand some bit of documentation. - An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you. -- Bugs in CoqIDE should also be filed on the [GitHub issue tracker](https://github.com/coq/coq/issues). Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features. +- Bugs in CoqIDE should also be filed in the [Coq issue tracker](https://github.com/coq/coq/issues). Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features. It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. @@ -40,7 +40,7 @@ Here are a few tags Coq developers may add to your PR and what they mean. In gen Currently the process for contributing to the documentation is the same as for changing anything else in Coq, so please submit a pull request as described above. -Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Aissue%20label%3A%22kind%3A%20documentation%22%20). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. +Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/). diff --git a/Makefile.ci b/Makefile.ci index b5a26d96e..54ebf211f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -11,7 +11,7 @@ CI_TARGETS=ci-all \ ci-formal-topology \ ci-geocoq \ ci-hott \ - ci-iris-coq \ + ci-iris-lambda-rust \ ci-math-classes \ ci-math-comp \ ci-metacoq \ diff --git a/config/coq_config.mli b/config/coq_config.mli index 8bc044c3a..6a834a304 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -61,7 +61,6 @@ val plugins_dirs : string list val all_src_dirs : string list val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) -val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *) val browser : string (** default web browser to use, may be overridden by environment diff --git a/configure.ml b/configure.ml index a7acdf532..0952b15f5 100644 --- a/configure.ml +++ b/configure.ml @@ -258,7 +258,6 @@ module Prefs = struct let macintegration = ref true let browser = ref (None : string option) let withdoc = ref false - let geoproof = ref false let byteonly = ref false let flambda_flags = ref [] let debug = ref true @@ -321,8 +320,6 @@ let args_options = Arg.align [ "<command> Use <command> to open URL %s"; "-with-doc", arg_bool Prefs.withdoc, "(yes|no) Compile the documentation or not"; - "-with-geoproof", arg_bool Prefs.geoproof, - "(yes|no) Use Geoproof binding or not"; "-byte-only", Arg.Set Prefs.byteonly, " Compiles only bytecode version of Coq"; "-nodebug", Arg.Clear Prefs.debug, @@ -1073,7 +1070,6 @@ let write_configml f = pr_l "flambda_flags" !Prefs.flambda_flags; pr_i "vo_magic_number" vo_magic; pr_i "state_magic_number" state_magic; - pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; pr_s "wwwcoq" !Prefs.coqwebsite; pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js index 371c5adc0..5ff618a83 100644 --- a/dev/Coq_Bugzilla_autolink.user.js +++ b/dev/Coq_Bugzilla_autolink.user.js @@ -10,25 +10,59 @@ var regex = /BZ#(\d+)/g; var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>'; -function doNode(node) +function doTitle(node) { node.innerHTML = node.innerHTML.replace(regex,substr); } +function filter(node) +{ + if (node.nodeName == '#text') + { + return NodeFilter.FILTER_ACCEPT; + } + else if(node.nodeName == 'A') + { + return NodeFilter.FILTER_REJECT; + } + return NodeFilter.FILTER_SKIP; +} var comments = document.getElementsByClassName("comment-body"); -for(var i=0; i<comments.length; i++) +function doNode(parent) { - var pars = comments[i].getElementsByTagName("p"); - for(var j=0; j<pars.length; j++) + var nodes = document.createTreeWalker(parent,NodeFilter.SHOW_ALL,{ acceptNode : filter },false); + var node; + while(node=nodes.nextNode()) { - doNode(pars[j]); + var content = node.textContent; + var matches = regex.exec(content); + + if(matches && matches.length > 1) + { + var range = document.createRange(); + var start = content.search(regex); + var end = start + matches[0].length; + range.setStart(node, start); + range.setEnd(node, end); + var linkNode = document.createElement("a"); + linkNode.href = "https://coq.inria.fr/bugs/show_bug.cgi?id=" + matches[1]; + range.surroundContents(linkNode); + + //handle multiple matches in one text node + doNode(linkNode.parentNode); + } } } +for(var i=0; i<comments.length; i++) +{ + doNode(comments[i]); +} + // usually 1 or 0 titles... var titles = document.getElementsByClassName("js-issue-title"); for(var i=0; i<titles.length; i++) { - doNode(titles[i]); + doTitle(titles[i]); } diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 43525dcd4..545846da5 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -43,6 +43,9 @@ : ${Iris_CI_BRANCH:=master} : ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} +: ${lambdaRust_CI_BRANCH:=master} +: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git} + ######################################################################## # HoTT ######################################################################## diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-lambda-rust.sh index c49b6ed9c..cf24d202d 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -4,25 +4,38 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp - Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq +lambdaRust_CI_DIR=${CI_BUILD_DIR}/lambdaRust install_ssreflect # Add or update the opam repo we need for dependency resolution opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev -# Setup Iris first, extract required version of std++ -git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} -stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o) +# Setup lambdaRust first +git_checkout ${lambdaRust_CI_BRANCH} ${lambdaRust_CI_GITURL} ${lambdaRust_CI_DIR} + +# Extract required version of Iris +Iris_VERSION=$(cat ${lambdaRust_CI_DIR}/opam | fgrep coq-iris | egrep 'dev\.([0-9.-]+)' -o) +Iris_URL=$(opam show coq-iris.$Iris_VERSION -f upstream-url) +read -a Iris_URL_PARTS <<< $(echo $Iris_URL | tr '#' ' ') + +# Setup Iris +git_checkout ${Iris_CI_BRANCH} ${Iris_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]} -# Ask opam where to get this std++, separating at the # +# Extract required version of std++ +stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o) stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url) read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ') # Setup std++ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} + +# Build std++ ( cd ${stdpp_CI_DIR} && make && make install ) -# Build iris now -( cd ${Iris_CI_DIR} && make ) +# Build iris +( cd ${Iris_CI_DIR} && make && make install ) + +# Build lambdaRust +( cd ${lambdaRust_CI_DIR} && make && make install ) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 892c9931b..8b1fc7c8f 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -214,11 +214,6 @@ The following command-line options are recognized by the commands {\tt % % Switch on the debug flag. -\item[{\tt -with-geoproof} (yes|no)]\ % - - Enable or not special functions for Geoproof within {\CoqIDE} (default - is yes). - \item[{\tt -color} (on|off|auto)]\ % Enable or not the coloring of output of {\tt coqtop}. Default is auto, diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 75f3d18de..436099e74 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -13,8 +13,7 @@ line. Without argument, the main screen is displayed with an ``unnamed buffer'', and with a file name as argument, another buffer displaying the contents of that file. Additionally, \verb|coqide| accepts the same options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having -obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. - +obviously no meaning for \CoqIDE{} being ignored. \begin{figure}[t] \begin{center} diff --git a/ide/coqide.ml b/ide/coqide.ml index 2c8ce0049..842d06859 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1325,25 +1325,6 @@ let main files = Minilib.log "End of Coqide.main" -(** {2 Geoproof } *) - -(** This function check every tenth of second if GeoProof has send - something on his private clipboard *) - -let check_for_geoproof_input () = - let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in - let handler () = match cb_Dr#text with - |None -> true - |Some "Ack" -> true - |Some s -> - on_current_term (fun sn -> sn.buffer#insert (s ^ "\n")); - (* cb_Dr#clear does not work so i use : *) - cb_Dr#set_text "Ack"; - true - in - ignore (GMain.Timeout.add ~ms:100 ~callback:handler) - - (** {2 Argument parsing } *) (** By default, the coqtop we try to launch is exactly the current coqide diff --git a/ide/coqide.mli b/ide/coqide.mli index 39b4d9ae2..42dab9ec5 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -40,5 +40,3 @@ val set_signal_handlers : unit -> unit (** Emergency saving of opened files as "foo.v.crashcoqide", and exit (if the integer isn't 127). *) val crash_save : int -> unit - -val check_for_geoproof_input : unit -> unit diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 73a30b18f..8d99cc3e6 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -142,7 +142,6 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - if !Coq_config.with_geoproof then Coqide.check_for_geoproof_input (); os_specific_init (); try GMain.main (); diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1cea307d7..a0a749bfb 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2132,8 +2132,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = ~pattern_mode:true ~ltacvars env c in pattern_of_glob_constr c -let interp_notation_constr ?(impls=empty_internalization_env) nenv a = - let env = Global.env () in +let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; @@ -2212,4 +2211,3 @@ let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_ let int_env,bl = intern_context global_level env impl_env params in let x = interp_glob_context_evars env evdref shift bl in int_env, x - diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0a4eaf838..75e99dd9b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -182,7 +182,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_ (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) -val interp_notation_constr : ?impls:internalization_env -> +val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes * notation_var_internalization_type) Id.Map.t * notation_constr * reversibility_flag diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index bc7146884..ea412a7d6 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -502,7 +502,7 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtBack of vernac_part_of_script * Stateid.t + | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list diff --git a/kernel/names.ml b/kernel/names.ml index e524f4258..cb27104d1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -113,8 +113,7 @@ struct module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = Id.t -> Id.t let hashcons hident = function | Name id -> Name (hident id) @@ -236,8 +235,7 @@ struct module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = @@ -869,8 +867,7 @@ struct module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) let eq ((c,b) as x) ((c',b') as y) = diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 5e20c1b51..400f9feee 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -78,12 +78,12 @@ let subst_opaque sub = function let iter_direct_opaque f = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> - Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) + Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> - Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) + Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) let join_opaque { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> ignore(Future.join cu) @@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) @@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | Some u -> Future.force u let get_constraints { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd) + | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp - then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd) + then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i let get_proof { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Future.chain ~pure:true cu fst + | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in - Future.chain ~pure:true pt (fun c -> + Future.chain pt (fun c -> force_constr (List.fold_right subst_substituted l (from_val c))) module FMap = Future.UUIDMap diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 22e109b01..f93b24b3e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -266,7 +266,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain body (fun ((body,uctx),side_eff) -> let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in @@ -535,7 +535,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~pure:true body + const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -628,7 +628,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~pure:true + const_entry_body = Future.chain ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), ()); diff --git a/kernel/univ.ml b/kernel/univ.ml index bae782f5d..7fe4f8274 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -121,8 +121,7 @@ module Level = struct (** Hashcons on levels + their hash *) module Self = struct - type _t = t - type t = _t + type nonrec t = t type u = unit let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash @@ -755,8 +754,7 @@ struct module HInstancestruct = struct - type _t = t - type t = _t + type nonrec t = t type u = Level.t -> Level.t let hashcons huniv a = diff --git a/lib/future.ml b/lib/future.ml index d9463aa0f..09285ea27 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -6,12 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* To deal with side effects we have to save/restore the system state *) -type freeze -let freeze = ref (fun () -> assert false : unit -> freeze) -let unfreeze = ref (fun _ -> () : freeze -> unit) -let set_freeze f g = freeze := f; unfreeze := g - let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ @@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f exception NotReady of string exception NotHere of string + let _ = CErrors.register_handler (function | NotReady name -> !not_ready_msg name | NotHere name -> !not_here_msg name @@ -59,7 +54,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) - | Val of 'a * freeze option + | Val of 'a | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = @@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with - | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) + | Finished v -> unnamed, UUID.invalid, id, ref (Val v) | Ongoing (name, x) -> try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c with CEphemeron.InvalidKey -> @@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with | Val _ | Closure _ | Delegated _ -> false let peek_val kx = let _, _, _, x = get kx in match !x with - | Val (v, _) -> Some v + | Val v -> Some v | Exn _ | Closure _ | Delegated _ -> None let uuid kx = let _, id, _, _ = get kx in id -let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) -let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) +let from_val ?(fix_exn=id) v = create fix_exn (Val v) +let from_here ?(fix_exn=id) v = create fix_exn (Val v) let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn @@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn = let _, _, fix_exn, c = get ck in assert (match !c with Delegated _ -> true | _ -> false); begin match v with - | `Val v -> c := Val (v, None) + | `Val v -> c := Val v | `Exn e -> c := Exn (fix_exn e) | `Comp f -> let _, _, _, comp = get f in c := !comp end; signal () in @@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn = ck, assignement signal ck (* TODO: get rid of try/catch to be stackless *) -let rec compute ~pure ck : 'a value = +let rec compute ck : 'a value = let _, _, fix_exn, c = get ck in match !c with - | Val (x, _) -> `Val x + | Val x -> `Val x | Exn (e, info) -> `Exn (e, info) - | Delegated wait -> wait (); compute ~pure ck + | Delegated wait -> wait (); compute ck | Closure f -> try let data = f () in - let state = if pure then None else Some (!freeze ()) in - c := Val (data, state); `Val data + c := Val data; `Val data with e -> let e = CErrors.push e in let e = fix_exn e in @@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value = | (NotReady _, _) -> `Exn e | _ -> c := Exn e; `Exn e -let force ~pure x = match compute ~pure x with +let force x = match compute x with | `Val v -> v | `Exn e -> Exninfo.iraise e -let chain ~pure ck f = +let chain ck f = let name, uuid, fix_exn, c = get ck in create ~uuid ~name fix_exn (match !c with - | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) + | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) | Exn _ as x -> x - | Val (v, None) when pure -> Val (f v, None) - | Val (v, Some _) when pure -> Val (f v, None) - | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) - | Val (v, None) -> - match !ck with - | Finished _ -> CErrors.anomaly(Pp.str - "Future.chain ~pure:false call on an already joined computation.") - | Ongoing _ -> CErrors.anomaly(Pp.strbrk( - "Future.chain ~pure:false call on a pure computation. "^ - "This can happen if the computation was initial created with "^ - "Future.from_val or if it was Future.chain ~pure:true with a "^ - "function and later forced."))) + | Val v -> Val (f v)) let create fix_exn f = create fix_exn (Closure f) let replace kx y = let _, _, _, x = get kx in match !x with - | Exn _ -> x := Closure (fun () -> force ~pure:false y) + | Exn _ -> x := Closure (fun () -> force y) | _ -> CErrors.anomaly (Pp.str "A computation can be replaced only if is_exn holds.") -let purify f x = - let state = !freeze () in - try - let v = f x in - !unfreeze state; - v - with e -> - let e = CErrors.push e in !unfreeze state; Exninfo.iraise e - -let transactify f x = - let state = !freeze () in - try f x - with e -> - let e = CErrors.push e in !unfreeze state; Exninfo.iraise e - -let purify_future f x = if is_over x then f x else purify f x -let compute x = purify_future (compute ~pure:false) x -let force ~pure x = purify_future (force ~pure) x -let chain ~pure x f = - let y = chain ~pure x f in - if is_over x then ignore(force ~pure y); +let chain x f = + let y = chain x f in + if is_over x then ignore(force y); y -let force x = force ~pure:false x let join kx = let v = force kx in @@ -205,12 +169,11 @@ let join kx = let sink kx = if is_val kx then ignore(join kx) let split2 x = - chain ~pure:true x (fun x -> fst x), - chain ~pure:true x (fun x -> snd x) + chain x (fun x -> fst x), chain x (fun x -> snd x) let map2 f x l = CList.map_i (fun i y -> - let xi = chain ~pure:true x (fun x -> + let xi = chain x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in @@ -226,6 +189,5 @@ let print f kx = match !x with | Delegated _ -> str "Delegated" ++ uid | Closure _ -> str "Closure" ++ uid - | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) - | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x) + | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) diff --git a/lib/future.mli b/lib/future.mli index acfce51a0..853f81cea 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -6,42 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Futures: asynchronous computations with some purity enforcing +(* Futures: asynchronous computations. * * A Future.computation is like a lazy_t but with some extra bells and whistles - * to deal with imperative code and eventual delegation to a slave process. + * to deal with eventual delegation to a slave process. * - * Example of a simple scenario taken into account: - * - * let f = Future.from_here (number_of_constants (Global.env())) in - * let g = Future.chain ~pure:false f (fun n -> - * n = number_of_constants (Global.env())) in - * ... - * Lemmas.save_named ...; - * ... - * let b = Future.force g in - * - * The Future.computation f holds a (immediate, no lazy here) value. - * We then chain to obtain g that (will) hold false if (when it will be - * run) the global environment has a different number of constants, true - * if nothing changed. - * Before forcing g, we add to the global environment one more constant. - * When finally we force g. Its value is going to be *true*. - * This because Future.from_here stores in the computation not only the initial - * value but the entire system state. When g is forced the state is restored, - * hence Global.env() returns the environment that was actual when f was - * created. - * Last, forcing g is run protecting the system state, hence when g finishes, - * the actual system state is restored. - * - * If you compare this with lazy_t, you see that the value returned is *false*, - * that is counter intuitive and error prone. - * - * Still not all computations are impure and access/alter the system state. - * This class can be optimized by using ~pure:true, but there is no way to - * statically check if this flag is misused, hence use it with care. - * - * Other differences with lazy_t is that a future computation that produces + * One difference with lazy_t is that a future computation that produces * and exception can be substituted for another computation of the same type. * Moreover a future computation can be delegated to another execution entity * that will be allowed to set the result. Finally future computations can @@ -113,27 +83,17 @@ val is_exn : 'a computation -> bool val peek_val : 'a computation -> 'a option val uuid : 'a computation -> UUID.t -(* [chain pure c f] chains computation [c] with [f]. - * [chain] forces immediately the new computation if the old one is_over (Exn or Val). - * The [pure] parameter is tricky: - * [pure]: - * When pure is true, the returned computation will not keep a copy - * of the global state. - * [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in] - * is invalid. It works if one forces [c''] since the whole computation - * will be executed in one go. It will not work, and raise an anomaly, if - * one forces c' and then c''. - * [join c; chain ~pure:false c g] is invalid and fails at runtime. - * [force c; chain ~pure:false c g] is correct. - *) -val chain : pure:bool -> - 'a computation -> ('a -> 'b) -> 'b computation +(* [chain c f] chains computation [c] with [f]. + * [chain] is eager, that is to say, it won't suspend the new computation + * if the old one is_over (Exn or Val). +*) +val chain : 'a computation -> ('a -> 'b) -> 'b computation (* Forcing a computation *) val force : 'a computation -> 'a val compute : 'a computation -> 'a value -(* Final call, no more *inpure* chain allowed since the state is lost. +(* Final call. * Also the fix_exn function is lost, hence error reporting can be incomplete * in a computation obtained by chaining on a joined future. *) val join : 'a computation -> 'a @@ -148,19 +108,8 @@ val map2 : ('a computation -> 'b -> 'c) -> 'a list computation -> 'b list -> 'c list -(* Once set_freeze is called we can purify a computation *) -val purify : ('a -> 'b) -> 'a -> 'b -(* And also let a function alter the state but backtrack if it raises exn *) -val transactify : ('a -> 'b) -> 'a -> 'b - (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.t) -> 'a computation -> Pp.t -type freeze -(* These functions are needed to get rid of side effects. - Thy are set for the outermos layer of the system, since they have to - deal with the whole system state. *) -val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit - val customize_not_ready_msg : (string -> Pp.t) -> unit val customize_not_here_msg : (string -> Pp.t) -> unit diff --git a/library/states.ml b/library/states.ml index 03e4610a6..27e0a94f9 100644 --- a/library/states.ml +++ b/library/states.ml @@ -37,5 +37,3 @@ let with_state_protection f x = with reraise -> let reraise = CErrors.push reraise in (unfreeze st; iraise reraise) - -let with_state_protection_on_exception = Future.transactify diff --git a/library/states.mli b/library/states.mli index 780a4e8dc..accd0e7ea 100644 --- a/library/states.mli +++ b/library/states.mli @@ -30,10 +30,3 @@ val replace_summary : state -> Summary.frozen -> state val with_state_protection : ('a -> 'b) -> 'a -> 'b -(** [with_state_protection_on_exception f x] applies [f] to [x] and restores the - state of the whole system as it was before applying [f] only if an - exception is raised. Unlike [with_state_protection] it also takes into - account the proof state *) - -val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b - diff --git a/man/coqtop.1 b/man/coqtop.1 index 62d17aa67..b1fbb3262 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -140,12 +140,6 @@ dump globalizations in file f (to be used by ) .TP -.BI \-with\-geoproof \ (yes|no) -to (de)activate special functions for Geoproof within Coqide (default is -.I yes -) - -.TP .B \-impredicative\-set set sort Set impredicative diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 1524079f4..6d3d4b743 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -10,7 +10,7 @@ open Context.Named.Declaration let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = - Future.chain ~pure:true x begin fun ((b,ctx),fx) -> + Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index cf97ae3ab..4bc3dba36 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction: * bug fixes: - many concerning Records. -- a Stack Overflow with mutual inductive (PR#320) +- a Stack Overflow with mutual inductive (BZ#320) - some optimizations have been removed since they were not type-safe: For example if e has type: type 'x a = A Then: match e with A -> A -----X----> e @@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction: - the dummy constant "__" have changed. see README - - a few bug-fixes (#191 and others) + - a few bug-fixes (BZ#191 and others) 7.2 -> 7.3 diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0f537abec..f708307c3 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -145,7 +145,7 @@ let rec pp_expr par env args = | MLrel n -> let id = get_db_name n env in (* Try to survive to the occurrence of a Dummy rel. - TODO: we should get rid of this hack (cf. #592) *) + TODO: we should get rid of this hack (cf. BZ#592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in apply (Id.print id) | MLapp (f,args') -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1e8854249..76fcd5ec8 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -549,3 +549,12 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +(* We only "purify" on exceptions *) +let funind_purify f x = + let st = Vernacentries.freeze_interp_state `No in + try f x + with e -> + let e = CErrors.push e in + Vernacentries.unfreeze_interp_state st; + Exninfo.iraise e diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 2e2ced790..d41abee87 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -123,3 +123,5 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +val funind_purify : ('a -> 'b) -> ('a -> 'b) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 299753766..9cb2a0a3f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -759,7 +759,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - States.with_state_protection_on_exception + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> let env = Global.env () in let evd = ref (Evd.from_env env) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 74c454334..76f859ed7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1595,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - States.with_state_protection_on_exception (fun () -> + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> com_terminate tcc_lemma_name tcc_lemma_constr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index bcd5b388a..0bf6e3d15 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -468,7 +468,9 @@ let register_ltac local tacl = let () = List.iter iter_rec recvars in List.map map rfun in - let defs = Future.transactify defs () in + (* STATE XXX: Review what is going on here. Why does this needs + protection? Why is not the STM level protection enough? Fishy *) + let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 23f96b5a3..469e1a011 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,7 +156,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with - const_entry_body = Future.chain ~pure:true ce.const_entry_body + const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cd4d1dcf6..621178982 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -373,11 +373,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in - fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) + fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> Future.from_val (univctx, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> + Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index b46556ea6..01b75e496 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { proof }) -> + | `Valid (Some { Vernacentries.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/stm.ml b/stm/stm.ml index d1693519d..84a4c5cc5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -22,7 +22,18 @@ open Pp open CErrors open Feedback open Vernacexpr -open Vernac_classifier + +(* Protect against state changes *) +let stm_purify f x = + let st = Vernacentries.freeze_interp_state `No in + try + let res = f x in + Vernacentries.unfreeze_interp_state st; + res + with e -> + let e = CErrors.push e in + Vernacentries.unfreeze_interp_state st; + Exninfo.iraise e let execution_error ?loc state_id msg = feedback ~id:state_id @@ -138,10 +149,12 @@ type step = | `Qed of qed_t * Stateid.t | `Sideff of seff_t * Stateid.t | `Alias of alias_t ] + type visit = { step : step; next : Stateid.t } let mkTransTac cast cblock cqueue = Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false } + let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } @@ -152,14 +165,11 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; type cached_state = | Empty | Error of Exninfo.iexn - | Valid of state -and state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} + | Valid of Vernacentries.interp_state + type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } + type 'vcs state_info = { (* TODO: Make this record private to VCS *) mutable n_reached : int; (* debug cache: how many times was computed *) mutable n_goals : int; (* open goals: indentation *) @@ -715,6 +725,7 @@ module State : sig ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit + val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref val install_cached : Stateid.t -> unit @@ -722,16 +733,18 @@ module State : sig val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn + (* to send states across worker/master *) - type frozen_state - val get_cached : Stateid.t -> frozen_state - val same_env : frozen_state -> frozen_state -> bool + val get_cached : Stateid.t -> Vernacentries.interp_state + val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool type proof_part + type partial_state = - [ `Full of frozen_state - | `Proof of Stateid.t * proof_part ] - val proof_part_of_frozen : frozen_state -> proof_part + [ `Full of Vernacentries.interp_state + | `ProofOnly of Stateid.t * proof_part ] + + val proof_part_of_frozen : Vernacentries.interp_state -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -742,39 +755,29 @@ module State : sig be removed in the state handling refactoring. *) val cur_id : Stateid.t ref - end = struct (* {{{ *) + open Vernacentries + (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy let fix_exn_ref = ref (fun x -> x) - (* helpers *) - let freeze_global_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; - shallow = (marshallable = `Shallow) } - let unfreeze_global_state { system; proof } = - States.unfreeze system; Proof_global.unfreeze proof - - (* hack to make futures functional *) - let () = Future.set_freeze - (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) - - type frozen_state = state type proof_part = Proof_global.state * Summary.frozen_bits (* only meta counters *) + type partial_state = - [ `Full of frozen_state - | `Proof of Stateid.t * proof_part ] - let proof_part_of_frozen { proof; system } = + [ `Full of Vernacentries.interp_state + | `ProofOnly of Stateid.t * proof_part ] + + let proof_part_of_frozen { Vernacentries.proof; system } = proof, Summary.project_summary (States.summary_of_state system) summary_pstate let freeze marshallable id = - VCS.set_state id (Valid (freeze_global_state marshallable)) + VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable)) + let freeze_invalid id iexn = VCS.set_state id (Error iexn) let is_cached ?(cache=`No) id only_valid = @@ -797,9 +800,13 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - if Stateid.equal id !cur_id then () (* optimization *) - else begin unfreeze_global_state s; cur_id := id end - | { state = Error ie } -> cur_id := id; Exninfo.iraise ie + Vernacentries.unfreeze_interp_state s; + cur_id := id + + | { state = Error ie } -> + cur_id := id; + Exninfo.iraise ie + | _ -> (* coqc has a 1 slot cache and only for valid states *) if VCS.is_interactive () = `No && Stateid.equal id !cur_id then () @@ -819,13 +826,13 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with proof = + then { s with Vernacentries.proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `Proof(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,counters)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = @@ -895,11 +902,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (freeze_global_state `No) + init_state := Some (Vernacentries.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - unfreeze_global_state Option.(get !init_state) + Vernacentries.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -994,7 +1001,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) @@ -1011,18 +1018,18 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e | _ -> false in - let aux_interp cmd = + let aux_interp st cmd = if is_filtered_command cmd then - stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr) + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else match cmd with - | VernacShow ShowScript -> ShowScript.show_script () + | VernacShow ShowScript -> ShowScript.show_script (); st | expr -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) - in aux_interp expr + in aux_interp st expr (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1036,8 +1043,8 @@ module Backtrack : sig (* we could navigate the dag, but this ways easy *) val branches_of : Stateid.t -> backup - (* To be installed during initialization *) - val undo_vernac_classifier : vernac_expr -> vernac_classification + (* Returns the state that the command should backtract to *) + val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when end = struct (* {{{ *) @@ -1105,7 +1112,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtBack (true, Stateid.initial), VtNow + Stateid.initial, VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -1113,20 +1120,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtBack (true, oid), VtNow + oid, VtNow with Not_found -> - VtBack (true, id), VtNow) + id, VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtBack (true, oid), VtNow + oid, VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,tactic,undo) -> let value = (if tactic then 1 else 0) - undo in if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in - VtBack (true, oid), VtLater + oid, VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1143,17 +1150,17 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - VtBack (true, oid), VtLater + oid, VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - VtBack (true, oid), VtLater + oid, VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtBack (VCS.is_interactive () = `Yes, Stateid.of_int id), VtNow - | _ -> VtUnknown, VtNow + Stateid.of_int id, VtNow + | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> CErrors.user_err ~hdr:"undo_vernac_classifier" @@ -1429,18 +1436,28 @@ end = struct (* {{{ *) * the few errors tactics don't catch, like the "fix" tactic building * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in + (* STATE: We use the current installed imperative state *) + let st = Vernacentries.freeze_interp_state `No in if not drop then begin - let checked_proof = Future.chain ~pure:false future_proof (fun p -> + let checked_proof = Future.chain future_proof (fun p -> + + (* Unfortunately close_future_proof and friends are not pure so we need + to set the state manually here *) + Vernacentries.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + + let st = Vernacentries.freeze_interp_state `No in stm_vernac_interp stop - ~proof:(pobject, terminator) + ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; + (* STATE: Restore the state XXX: handle exn *) + Vernacentries.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1457,7 +1474,7 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else - let is_tac e = match classify_vernac e with + let is_tac e = match Vernac_classifier.classify_vernac e with | VtProofStep _, _ -> true | _ -> false in @@ -1480,7 +1497,7 @@ end = struct (* {{{ *) | _, None -> None | Some (prev, o, `Cmd { cast = { expr }}), Some n when is_tac expr && State.same_env o n -> (* A pure tactic *) - Some (id, `Proof (prev, State.proof_part_of_frozen n)) + Some (id, `ProofOnly (prev, State.proof_part_of_frozen n)) | Some _, Some s -> msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) @@ -1575,9 +1592,16 @@ end = struct (* {{{ *) (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; - stm_vernac_interp stop ~proof + (* STATE SPEC: + * - start: First non-expired state! [This looks very fishy] + * - end : start + qed + * => takes nothing from the itermediate states. + *) + (* STATE We use the state resulting from reaching start. *) + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }; + expr = (VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> @@ -1633,10 +1657,9 @@ end = struct (* {{{ *) let pr = Future.from_val (map (Option.get (Global.body_of_constant_body c))) in let uc = - Future.chain - ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~pure:true pr discharge in - let pr = Future.chain ~pure:true pr Constr.hcons in + Future.chain uc Univ.hcons_universe_context_set in + let pr = Future.chain pr discharge in + let pr = Future.chain pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; @@ -1812,7 +1835,7 @@ end = struct (* {{{ *) Option.iter VCS.restore vcs; try Reach.known_state ~cache:`No id; - Future.purify (fun () -> + stm_purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in @@ -1826,7 +1849,14 @@ end = struct (* {{{ *) else begin let (i, ast) = r_ast in Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); - stm_vernac_interp r_state_fb ast; + (* STATE SPEC: + * - start : id + * - return: id + * => captures state id in a future closure, which will + discard execution state but for the proof + univs. + *) + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress @@ -1865,7 +1895,8 @@ end = struct (* {{{ *) | VernacRedirect (_,(_,e)) -> find ~time ~fail e | VernacFail e -> find ~time ~fail:true e | e -> e, time, fail in find ~time:false ~fail:false e in - Vernacentries.with_fail fail (fun () -> + let st = Vernacentries.freeze_interp_state `No in + Vernacentries.with_fail st fail (fun () -> (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> @@ -1957,8 +1988,14 @@ end = struct (* {{{ *) VCS.restore r_doc; VCS.print (); Reach.known_state ~cache:`No r_where; + (* STATE *) + let st = Vernacentries.freeze_interp_state `No in try - stm_vernac_interp r_for { r_what with verbose = true }; + (* STATE SPEC: + * - start: r_where + * - end : after execution of r_what + *) + ignore(stm_vernac_interp r_for st { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -2166,14 +2203,20 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { proof } -> + | Valid { Vernacentries.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); - Option.iter (fun expr -> stm_vernac_interp id { + (* STATE SPEC: + * - start: Modifies the input state adding a proof. + * - end : maybe after recovery command. + *) + (* STATE: We use an updated state with proof *) + let st = Vernacentries.freeze_interp_state `No in + Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; - strlen = 0 }) + strlen = 0 } )) recovery_command | _ -> assert false end @@ -2211,10 +2254,12 @@ let known_state ?(redefine_qed=false) ~cache id = let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in - let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); - reach ~safe_id id; - cherry_pick_non_pstate ()) id + let rec pure_cherry_pick_non_pstate safe_id id = + stm_purify (fun id -> + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + reach ~safe_id id; + cherry_pick_non_pstate ()) + id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = @@ -2247,7 +2292,10 @@ let known_state ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach view.next; - stm_vernac_interp id x); + (* State resulting from reach *) + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x) + ); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> @@ -2255,18 +2303,23 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - stm_vernac_interp id x; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - stm_vernac_interp id x; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; - (try stm_vernac_interp id x; + + (try + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in @@ -2316,14 +2369,18 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - stm_vernac_interp id ~proof x; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> - reach eop; stm_vernac_interp id x; Proof_global.discard_all () + reach eop; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); + Proof_global.discard_all () ), `Yes, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; @@ -2344,7 +2401,8 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - stm_vernac_interp id ?proof x; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); @@ -2360,7 +2418,10 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> - reach view.next; stm_vernac_interp id x; update_global_env () + reach view.next; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); + update_global_env () ), cache, true | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; @@ -2414,7 +2475,6 @@ let new_doc { doc_type ; require_libs } = State.restore_root_state (); let doc = VCS.init doc_type Stateid.initial in - set_undo_classifier Backtrack.undo_vernac_classifier; begin match doc_type with | Interactive ln -> @@ -2505,7 +2565,7 @@ let check_task name (tasks,rcbackup) i = RemoteCounter.restore rcbackup; let vcs = VCS.backup () in try - let rc = Future.purify (Slaves.check_task name tasks) i in + let rc = stm_purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false @@ -2515,7 +2575,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = Future.purify (Slaves.finish_task name u d p t) i in + let u = stm_purify (Slaves.finish_task name u d p t) i in VCS.restore vcs; u in try @@ -2545,7 +2605,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; VCS.delete_branch brname; VCS.gc (); - Reach.known_state ~redefine_qed:true ~cache:`No qed_id; + let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2578,7 +2638,38 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_transaction ?(newtip=Stateid.fresh ()) +let process_back_meta_command ~part_of_script ~newtip ~head oid aast w = + match part_of_script, w with + | true, w -> + let id = VCS.new_node ~id:newtip () in + let { mine; others } = Backtrack.branches_of oid in + let valid = VCS.get_branch_pos head in + List.iter (fun branch -> + if not (List.mem_assoc branch (mine::others)) then + ignore(merge_proof_branch ~valid aast VtDrop branch)) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + let head = VCS.current_branch () in + List.iter (fun b -> + if not(VCS.Branch.equal b head) then begin + VCS.checkout b; + VCS.commit (VCS.new_node ()) (Alias (oid,aast)); + end) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + VCS.commit id (Alias (oid,aast)); + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + + | false, VtNow -> + stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid); + Backtrack.backto oid; + VCS.checkout_shallowest_proof_branch (); + Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok + + | false, VtLater -> + anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.") + +let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2587,47 +2678,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.checkout head; let rc = begin stm_prerr_endline (fun () -> - " classified as: " ^ string_of_vernac_classification c); + " classified as: " ^ Vernac_classifier.string_of_vernac_classification c); match c with - (* Back *) - | VtBack (true, oid), w -> - let id = VCS.new_node ~id:newtip () in - let { mine; others } = Backtrack.branches_of oid in - let valid = VCS.get_branch_pos head in - List.iter (fun branch -> - if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch ~valid x VtDrop branch)) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - let head = VCS.current_branch () in - List.iter (fun b -> - if not(VCS.Branch.equal b head) then begin - VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias (oid,x)); - end) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias (oid,x)); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtBack (false, id), VtNow -> - stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); - Backtrack.backto id; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(VCS.is_interactive ()) id; `Ok - | VtBack (false, id), VtLater -> - anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") - + (* Meta *) + | VtMeta, _ -> + let id, w = Backtrack.undo_vernac_classifier expr in + process_back_meta_command ~part_of_script ~newtip ~head id x w (* Query *) - | VtQuery (false, route), VtNow -> - begin - let query_sid = VCS.cur_tip () in - try stm_vernac_interp ~route (VCS.cur_tip ()) x - with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e) - end; `Ok - (* Part of the script commands don't set the query route *) - | VtQuery (true, _route), w -> + | VtQuery (false,route), VtNow -> + let query_sid = VCS.cur_tip () in + (try + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp ~route query_sid st x) + with e -> + let e = CErrors.push e in + Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok + | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) @@ -2696,7 +2762,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - stm_vernac_interp (VCS.get_branch_pos head) x; `Ok + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); + `Ok | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in @@ -2717,12 +2785,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in - Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *) + let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *) let step () = VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in - Reach.known_state ~cache:(VCS.is_interactive ()) mid; - stm_vernac_interp id x; + let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then begin @@ -2854,7 +2923,7 @@ let add ~doc ~ontop ?newtip verb (loc, ast) = let indentation, strlen = compute_indentation ?loc ontop in CWarnings.set_current_loc loc; (* XXX: Classifiy vernac should be moved inside process transaction *) - let clas = classify_vernac ast in + let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in match process_transaction ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip @@ -2869,17 +2938,17 @@ type focus = { } let query ~doc ~at ~route s = - Future.purify (fun s -> + stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~cache:`Yes at; let loc, ast = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; - let clas = classify_vernac ast in + let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtBack (_,id), _ -> (* TODO: can this still happen ? *) - ignore(process_transaction aast (VtBack (false,id), VtNow)) + | VtMeta , _ -> (* TODO: can this still happen ? *) + ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow)) | _ -> ignore(process_transaction aast (VtQuery (false, route), VtNow))) s diff --git a/stm/stm.mli b/stm/stm.mli index c65cf6a9a..31f4599d3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -217,16 +217,10 @@ val state_ready_hook : (Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t -type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool -} - val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 158ad9084..3aa2cd707 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -31,7 +31,7 @@ let string_of_vernac_type = function Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route - | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b + | VtMeta -> "Meta " let string_of_vernac_when = function | VtLater -> "Later" @@ -53,9 +53,6 @@ let make_polymorphic (a, b as x) = VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b | _ -> x -let undo_classifier = ref (fun _ -> assert false) -let set_undo_classifier f = undo_classifier := f - let rec classify_vernac e = let static_classifier e = match e with (* Univ poly compatibility: we run it now, so that we can just @@ -75,7 +72,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtBack _ | VtProofMode _ ), _ as x -> x + | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow @@ -191,7 +188,7 @@ let rec classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e + | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 2fa1e0b8d..fe42a03a3 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification val declare_vernac_classifier : Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit -(** Set by Stm *) -val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6f7e61f6b..e8a78d72d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2471,7 +2471,7 @@ let exceed_bound n = function (* We delay thinning until the completion of the whole intros tactic to ensure that dependent hypotheses are cleared in the right - dependency order (see bug #1000); we use fresh names, not used in + dependency order (see BZ#1000); we use fresh names, not used in the tactic, for the hyps to clear *) (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]: [b]: compatibility flag, if false at toplevel, do not complete incomplete diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v new file mode 100644 index 000000000..edd5c8d73 --- /dev/null +++ b/test-suite/bugs/closed/5762.v @@ -0,0 +1,28 @@ +(* Supporting imp. params. in inductive or fixpoints mutually defined with a notation *) + +Reserved Notation "* a" (at level 70). +Inductive P {n : nat} : nat -> Prop := +| c m : *m +where "* m" := (P m). + +Reserved Notation "##". +Inductive I {A:Type} := C : ## where "##" := I. + +(* The following was working in 8.6 *) + +Require Import Vector. + +Reserved Notation "# a" (at level 70). +Fixpoint f {n : nat} (v:Vector.t nat n) : nat := + match v with + | nil _ => 0 + | cons _ _ _ v => S (#v) + end +where "# v" := (f v). + +(* The following was working in 8.6 *) + +Reserved Notation "%% a" (at level 70). +Record R := + {g : forall {A} (a:A), a=a where "%% x" := (g x); + k : %% 0 = eq_refl}. diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 7d7d01c1b..e2928f78d 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -76,7 +76,7 @@ Various checks for coqdoc <br/> <span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="variable">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 844fb3031..de3182d1a 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -59,7 +59,7 @@ Various checks for coqdoc \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v index b3dfb33cd..b9c359888 100644 --- a/test-suite/ideal-features/complexity/evars_subst.v +++ b/test-suite/ideal-features/complexity/evars_subst.v @@ -1,4 +1,4 @@ -(* Bug report #932 *) +(* BZ#932 *) (* Expected time < 1.00s *) (* Let n be the number of let-in. The complexity comes from the fact diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index b3dfb33cd..b9c359888 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -1,4 +1,4 @@ -(* Bug report #932 *) +(* BZ#932 *) (* Expected time < 1.00s *) (* Let n be the number of let-in. The complexity comes from the fact diff --git a/test-suite/interactive/Back.v b/test-suite/interactive/Back.v index b813a79ab..22364254d 100644 --- a/test-suite/interactive/Back.v +++ b/test-suite/interactive/Back.v @@ -1,5 +1,5 @@ (* Check that reset remains synchronised with the compilation unit cache *) -(* See bug #1030 *) +(* See BZ#1030 *) Section multiset_defs. Require Import Plus. diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v index 220e2b369..0a6b1f06d 100644 --- a/test-suite/modules/objects2.v +++ b/test-suite/modules/objects2.v @@ -2,7 +2,7 @@ the logical objects in the environment *) -(* Bug #1118 (simplified version), submitted by Evelyne Contejean +(* BZ#1118 (simplified version), submitted by Evelyne Contejean (used to failed in pre-V8.1 trunk because of a call to lookup_mind for structure objects) *) diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index fafb478ba..61ae4edbd 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -7,7 +7,7 @@ Check | a :: l => f a :: F _ _ f l end). -(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *) +(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf BZ#860) *) Check let fix f (m : nat) : nat := match m with diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 7c9b89f9d..306532c0d 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -1,7 +1,7 @@ Set Implicit Arguments. Unset Strict Implicit. -(* Suggested by Pierre Casteran (bug #169) *) +(* Suggested by Pierre Casteran (BZ#169) *) (* Argument 3 is needed to typecheck and should be printed *) Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). Check (compose (C:=nat) S). diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 9a5edb813..75b66e463 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -7,12 +7,12 @@ Ltac f H := split; [a H|e H]. Print Ltac f. (* Test printing of match context *) -(* Used to fail after translator removal (see bug #1070) *) +(* Used to fail after translator removal (see BZ#1070) *) Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end. Print Ltac g. -(* Test an error message (#5390) *) +(* Test an error message (BZ#5390) *) Lemma myid (P : Prop) : P <-> P. Proof. split; auto. Qed. diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index 69dc9aca7..d52a853aa 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,4 @@ -(* Cf coqbugs #546 *) +(* Cf BZ#546 *) Require Import Omega. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 06f807f29..893d75b77 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -64,7 +64,7 @@ Check (fun x:I1 => end). (* Check implicit parameters of inductive types (submitted by Pierre - Casteran and also implicit in #338) *) + Casteran and also implicit in BZ#338) *) Set Implicit Arguments. Unset Strict Implicit. @@ -80,7 +80,7 @@ Inductive Finite (A : Set) : LList A -> Prop := | Finite_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). -(* Check positivity modulo reduction (cf bug #983) *) +(* Check positivity modulo reduction (cf bug BZ#983) *) Record P:Type := {PA:Set; PB:Set}. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 850f09434..45c71615f 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -1,6 +1,6 @@ Axiom magic : False. -(* Submitted by Dachuan Yu (bug #220) *) +(* Submitted by Dachuan Yu (BZ#220) *) Fixpoint T (n : nat) : Type := match n with | O => nat -> Prop @@ -16,7 +16,7 @@ Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l. inversion 1. Abort. -(* Submitted by Pierre Casteran (bug #540) *) +(* Submitted by Pierre Casteran (BZ#540) *) Set Implicit Arguments. Unset Strict Implicit. @@ -64,7 +64,7 @@ elim magic. elim magic. Qed. -(* Submitted by Boris Yakobowski (bug #529) *) +(* Submitted by Boris Yakobowski (BZ#529) *) (* Check that Inversion does not fail due to unnormalized evars *) Set Implicit Arguments. @@ -100,7 +100,7 @@ intros a b H. inversion H. Abort. -(* Check non-regression of bug #1968 *) +(* Check non-regression of BZ#1968 *) Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t). Goal forall o, foo2 o -> 0 = 1. @@ -130,7 +130,7 @@ Proof. intros. inversion H. Abort. -(* Bug #2314 (simplified): check that errors do not show as anomalies *) +(* BZ#2314 (simplified): check that errors do not show as anomalies *) Goal True -> True. intro. @@ -158,7 +158,7 @@ reflexivity. Qed. (* Up to September 2014, Mapp below was called MApp0 because of a bug - in intro_replacing (short version of bug 2164.v) + in intro_replacing (short version of BZ#2164.v) (example taken from CoLoR) *) Parameter Term : Type. diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v index d5e1a38cf..6c59bf6ed 100644 --- a/test-suite/success/Mod_type.v +++ b/test-suite/success/Mod_type.v @@ -1,4 +1,4 @@ -(* Check bug #1025 submitted by Pierre-Luc Carmel Biron *) +(* Check BZ#1025 submitted by Pierre-Luc Carmel Biron *) Module Type FOO. Parameter A : Type. @@ -18,7 +18,7 @@ Module Bar : BAR. End Bar. -(* Check bug #2809: correct printing of modules with notations *) +(* Check BZ#2809: correct printing of modules with notations *) Module C. Inductive test : Type := diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 4d04f2cf9..e3f90f6d9 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -1,5 +1,5 @@ (* Check that "where" clause behaves as if given independently of the *) -(* definition (variant of bug #1132 submitted by Assia Mahboubi) *) +(* definition (variant of BZ#1132 submitted by Assia Mahboubi) *) Fixpoint plus1 (n m:nat) {struct n} : nat := match n with diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index ecbf04e41..470e4f058 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -86,7 +86,7 @@ intros; omega. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index b8f8660e9..6fd936935 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -132,7 +132,7 @@ intros. omega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros. diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v index c4d086a34..4e726335c 100644 --- a/test-suite/success/Omega2.v +++ b/test-suite/success/Omega2.v @@ -1,6 +1,6 @@ Require Import ZArith Omega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 801ece9e3..0df3d5685 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -88,7 +88,7 @@ romega with nat. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m : nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 42730f2e1..3ddf6a40f 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -132,7 +132,7 @@ intros. romega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. @@ -146,7 +146,7 @@ intros x y. romega. Qed. -(* Besson #1298 *) +(* Besson BZ#1298 *) Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. Proof. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 87e8c8e33..43eda67ea 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -1,6 +1,6 @@ Require Import ZArith ROmega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index 0576f3c68..2789c6c9a 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -4,7 +4,7 @@ rename n into p. induction p; auto. Qed. -(* Submitted by Iris Loeb (#842) *) +(* Submitted by Iris Loeb (BZ#842) *) Section rename. diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index 361c787e2..76aac39a5 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -1,5 +1,5 @@ (* To shorten interactive scripts, it is better that Try catches - non-existent names in Unfold [cf bug #263] *) + non-existent names in Unfold [cf BZ#263] *) Lemma lem1 : True. try unfold i_dont_exist. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 90a60daa6..0219c3bfd 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -12,7 +12,7 @@ assumption. assumption. Qed. -(* Simplification of bug 711 *) +(* Simplification of BZ#711 *) Parameter f : true = false. Goal let p := f in True. @@ -37,7 +37,7 @@ Goal True. case Refl || ecase Refl. Abort. -(* Submitted by B. Baydemir (bug #1882) *) +(* Submitted by B. Baydemir (BZ#1882) *) Require Import List. @@ -385,7 +385,7 @@ intros. Fail destruct H. Abort. -(* Check keep option (bug #3791) *) +(* Check keep option (BZ#3791) *) Goal forall b:bool, True. intro b. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index c36313ec1..627794832 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -23,7 +23,7 @@ Definition f1 frm0 a1 : B := f frm0 a1. (* Checks that solvable ? in the type part of the definition are harmless *) Definition f2 frm0 a1 : B := f frm0 a1. -(* Checks that sorts that are evars are handled correctly (bug 705) *) +(* Checks that sorts that are evars are handled correctly (BZ#705) *) Require Import List. Fixpoint build (nl : list nat) : @@ -58,7 +58,7 @@ Check (forall y n : nat, {q : nat | y = q * n}) -> forall n : nat, {q : nat | x = q * n}). -(* Check instantiation of nested evars (bug #1089) *) +(* Check instantiation of nested evars (BZ#1089) *) Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). @@ -188,7 +188,7 @@ Abort. End Additions_while. -(* Two examples from G. Melquiond (bugs #1878 and #1884) *) +(* Two examples from G. Melquiond (BZ#1878 and BZ#1884) *) Parameter F1 G1 : nat -> Prop. Goal forall x : nat, F1 x -> G1 x. @@ -207,7 +207,7 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := | (existT _ k v)::l' => (existT _ k v):: (filter A l') end. -(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by +(* BZ#2000: used to raise Out of memory in 8.2 while it should fail by lack of information on the conclusion of the type of j *) Goal True. @@ -381,7 +381,7 @@ Section evar_evar_occur. Check match g _ with conj a b => f _ a b end. End evar_evar_occur. -(* Eta expansion (bug #2936) *) +(* Eta expansion (BZ#2936) *) Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c diff --git a/test-suite/success/if.v b/test-suite/success/if.v index 9fde95e80..c81d2b9bf 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -3,7 +3,7 @@ Check (fun b : bool => if b then Type else nat). -(* Check correct use of if-then-else predicate annotation (cf bug 690) *) +(* Check correct use of if-then-else predicate annotation (cf BZ#690) *) Check fun b : bool => if b as b0 return (if b0 then b0 = true else b0 = false) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index ee69df977..a329894aa 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -1,5 +1,5 @@ (* Thinning introduction hypothesis must be done after all introductions *) -(* Submitted by Guillaume Melquiond (bug #1000) *) +(* Submitted by Guillaume Melquiond (BZ#1000) *) Goal forall A, A -> True. intros _ _. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 29e373eaa..0f22a1f0a 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -147,7 +147,7 @@ check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not - seen as intro pattern or constr (bug #984) *) + seen as intro pattern or constr (BZ#984) *) Ltac afi tac := intros; tac. Goal 1 = 2. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 352abb2af..b8a8ff756 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -31,7 +31,7 @@ Proof. end). Abort. -(* Submitted by Roland Zumkeller (bug #888) *) +(* Submitted by Roland Zumkeller (BZ#888) *) (* The Fix and CoFix rules expect a subgoal even for closed components of the (co-)fixpoint *) @@ -43,7 +43,7 @@ Goal nat -> nat. exact 0. Qed. -(* Submitted by Roland Zumkeller (bug #889) *) +(* Submitted by Roland Zumkeller (BZ#889) *) (* The types of metas were in metamap and they were not updated when passing through a binder *) @@ -56,7 +56,7 @@ Goal forall n : nat, nat -> n = 0. end). Abort. -(* Submitted by Roland Zumkeller (bug #931) *) +(* Submitted by Roland Zumkeller (BZ#931) *) (* Don't turn dependent evar into metas *) Goal (forall n : nat, n = 0 -> Prop) -> Prop. @@ -65,7 +65,7 @@ intro P. reflexivity. Abort. -(* Submitted by Jacek Chrzaszcz (bug #1102) *) +(* Submitted by Jacek Chrzaszcz (BZ#1102) *) (* le problème a été résolu ici par normalisation des evars présentes dans les types d'evars, mais le problème reste a priori ouvert dans diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 5b87e877b..1bfb8580b 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. (* Check that inversion of names of mutual inductive fixpoints works *) -(* (cf bug #1031) *) +(* (cf BZ#1031) *) Inductive tree : Set := | node : nat -> forest -> tree diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 6f7498d65..1ffc02673 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 => (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)). -(* Core of an example submitted by Ralph Matthes (#849) +(* Core of an example submitted by Ralph Matthes (BZ#849) It used to fail because of the K-variable x in the type of "sum_rec ..." which was not in the scope of the evar ?B. Solved by a head @@ -131,7 +131,7 @@ try case nonemptyT_intro. (* check that it fails w/o anomaly *) Abort. (* Test handling of return type and when it is decided to make the - predicate dependent or not - see "bug" #1851 *) + predicate dependent or not - see "bug" BZ#1851 *) Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True). intros. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index fc74225d7..286340459 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -20,8 +20,7 @@ intro P; pattern P. apply lem2. Abort. -(* Check managing of universe constraints in inversion *) -(* Bug report #855 *) +(* Check managing of universe constraints in inversion (BZ#855) *) Inductive dep_eq : forall X : Type, X -> X -> Prop := | intro_eq : forall (X : Type) (f : X), dep_eq X f f @@ -40,7 +39,7 @@ Proof. Abort. -(* Submitted by Bas Spitters (bug report #935) *) +(* Submitted by Bas Spitters (BZ#935) *) (* This is a problem with the status of the type in LetIn: is it a user-provided one or an inferred one? At the current time, the diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v index 886533586..87b7a9a3b 100644 --- a/theories/Init/Tauto.v +++ b/theories/Init/Tauto.v @@ -27,7 +27,7 @@ Local Ltac simplif flags := | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => (* generalize (id0 id1); intro; clear id0 does not work - (see Marco Maggiesi's bug PR#301) + (see Marco Maggiesi's BZ#301) so we instead use Assert and exact. *) assert X2; [exact (id0 id1) | clear id0] | id: forall (_ : ?X1), ?X2|- _ => diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e9fdaac5b..19fcd9993 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -685,7 +685,6 @@ let parse_args arglist = |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) |"-require" -> add_require (next (), None, Some false) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) - |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d596e36f3..f0215b678 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -74,7 +74,6 @@ let print_usage_channel co command = \n -emacs tells Coq it is executed under Emacs\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ -\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d736975d3..cf63fbdc3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -119,7 +119,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtBack can be removed + document. Hopefully this is fixed when VtMeta can be removed and Undo etc... are just interpreted regularly. *) (* XXX: The classifier can emit warnings so we need to guard @@ -127,7 +127,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) = let wflags = CWarnings.get_flags () in CWarnings.set_flags "none"; let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with - | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true + | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; diff --git a/vernac/command.ml b/vernac/command.ml index a1a87d54e..f58ed065c 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in - { ce with const_entry_body = Future.chain ~pure:true proof_out + { ce with const_entry_body = Future.chain proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let warn_implicits_in_term = @@ -550,13 +550,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in - let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in @@ -708,7 +707,7 @@ let do_mutual_inductive indl cum poly prv finite = (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) - List.iter Metasyntax.add_notation_interpretation ntns; + List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) @@ -1110,7 +1109,7 @@ let interp_recursive isfix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = Metasyntax.with_syntax_protection (fun () -> - List.iter (Metasyntax.set_notation_for_interpretation impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.map4 (fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls)) fixctximpenvs fixctxs fixl fixccls) @@ -1176,7 +1175,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind fixpoint_message (Some indexes) fixnames; end; (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation ntns + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then @@ -1207,7 +1206,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n cofixpoint_message fixnames end; (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation ntns + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns let extract_decreasing_argument limit = function | (na,CStructRec) -> na diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d45665dd4..9ab89c883 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function (* Try all combinations... not optimal *) let env = Global.env() in { const with const_entry_body = - Future.chain ~pure:true const.const_entry_body + Future.chain const.const_entry_body (fun ((body, ctx), eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index b2d48bb2f..9376afa8c 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1318,7 +1318,7 @@ let to_map l = let fold accu (x, v) = Id.Map.add x v accu in List.fold_left fold Id.Map.empty l -let add_notation_in_scope local df c mods scope = +let add_notation_in_scope local df env c mods scope = let open SynData in let sd = compute_syntax_data df mods in (* Prepare the interpretation *) @@ -1329,7 +1329,7 @@ let add_notation_in_scope local df c mods scope = ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map sd.recvars; } in - let (acvars, ac, reversible) = interp_notation_constr nenv c in + let (acvars, ac, reversible) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in @@ -1349,7 +1349,7 @@ let add_notation_in_scope local df c mods scope = Lib.add_anonymous_leaf (inNotation notation); sd.info -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = +let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) @@ -1368,7 +1368,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) ninterp_var_type = to_map i_vars; ninterp_rec_vars = to_map recvars; } in - let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in + let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in let interp = make_interpretation_vars recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse = is_not_printable onlyparse (not reversible) ac in @@ -1395,33 +1395,33 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in (* Notations with only interpretation *) -let add_notation_interpretation ((loc,df),c,sc) = - let df' = add_notation_interpretation_core false df c sc false false None in +let add_notation_interpretation env ((loc,df),c,sc) = + let df' = add_notation_interpretation_core false df env c sc false false None in Dumpglob.dump_notation (loc,df') sc true -let set_notation_for_interpretation impls ((_,df),c,sc) = +let set_notation_for_interpretation env impls ((_,df),c,sc) = (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) -let add_notation local c ((loc,df),modifiers) sc = +let add_notation local env c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in let compat = get_compat_version modifiers in - try add_notation_interpretation_core local df c sc onlyparse onlyprint compat + try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat with NoSyntaxRule -> (* Try to determine a default syntax rule *) - add_notation_in_scope local df c modifiers sc + add_notation_in_scope local df env c modifiers sc else (* Declare both syntax and interpretation *) - add_notation_in_scope local df c modifiers sc + add_notation_in_scope local df env c modifiers sc in Dumpglob.dump_notation (loc,df') sc true @@ -1436,13 +1436,13 @@ let add_notation_extra_printing_rule df k v = let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) -let add_infix local ((loc,inf),modifiers) pr sc = +let add_infix local env ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) let metas = [inject_var "x"; inject_var "y"] in let c = mkAppC (pr,metas) in let df = "x "^(quote_notation_token inf)^" y" in - add_notation local c ((loc,df),modifiers) sc + add_notation local env c ((loc,df),modifiers) sc (**********************************************************************) (* Delimiters and classes bound to scopes *) @@ -1498,7 +1498,7 @@ let try_interp_name_alias = function | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found -let add_syntactic_definition ident (vars,c) local onlyparse = +let add_syntactic_definition env ident (vars,c) local onlyparse = let nonprintable = ref false in let vars,pat = try [], NRef (try_interp_name_alias (vars,c)) @@ -1509,7 +1509,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse = ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; } in - let nvars, pat, reversible = interp_notation_constr nenv c in + let nvars, pat, reversible = interp_notation_constr env nenv c in let () = nonprintable := not reversible in let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in List.map map vars, pat diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 9cd00cbcb..b3049f1b7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -11,15 +11,16 @@ open Vernacexpr open Notation open Constrexpr open Notation_term +open Environ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> (lstring * syntax_modifier list) -> +val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> constr_expr -> +val add_notation : locality_flag -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -33,11 +34,11 @@ val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : - (lstring * constr_expr * scope_name option) -> unit + env -> (lstring * constr_expr * scope_name option) -> unit (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.internalization_env -> +val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (** Add only the parsing/printing rule of a notation *) @@ -47,7 +48,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> +val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 81218308f..785c842ba 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -556,7 +556,7 @@ let declare_mutual_definition l = let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation first.prg_notations; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in diff --git a/vernac/record.ml b/vernac/record.ml index 18e7796ca..9a8657c3c 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -72,7 +72,7 @@ let interp_fields_evars env evars impls_env nots l = | None -> LocalAssum (i,t') | Some b' -> LocalDef (i,b',t') in - List.iter (Metasyntax.set_notation_for_interpretation impls) no; + List.iter (Metasyntax.set_notation_for_interpretation env impls) no; (EConstr.push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], impls_env) nots l diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 66427b709..e08cb8387 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -430,11 +430,11 @@ let vernac_arguments_scope locality r scl = let vernac_infix locality local = let local = enforce_module_locality locality local in - Metasyntax.add_infix local + Metasyntax.add_infix local (Global.env()) let vernac_notation locality local = let local = enforce_module_locality locality local in - Metasyntax.add_notation local + Metasyntax.add_notation local (Global.env()) (***********) (* Gallina *) @@ -953,7 +953,7 @@ let vernac_hints locality poly local lb h = let vernac_syntactic_definition locality lid x local y = Dumpglob.dump_definition lid false "syndef"; let local = enforce_module_locality locality local in - Metasyntax.add_syntactic_definition (snd lid) x local y + Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y let vernac_declare_implicits locality r l = let local = make_section_locality locality in @@ -2148,23 +2148,48 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -let with_fail b f = - if not b then f () +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +let s_cache = ref (States.freeze ~marshallable:`No) +let s_proof = ref (Proof_global.freeze ~marshallable:`No) + +let invalidate_cache () = + s_cache := Obj.magic 0; + s_proof := Obj.magic 0 + +let freeze_interp_state marshallable = + { system = (s_cache := States.freeze ~marshallable; !s_cache); + proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + shallow = marshallable = `Shallow } + +let unfreeze_interp_state { system; proof } = + if (!s_cache != system) then (s_cache := system; States.unfreeze system); + if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) + +(* XXX STATE: this type hints that restoring the state should be the + caller's responsibility *) +let with_fail st b f = + if not b + then f () else begin try (* If the command actually works, ignore its effects on the state. * Note that error has to be printed in the right state, hence * within the purified function *) - Future.purify - (fun v -> - try f v; raise HasNotFailed - with - | HasNotFailed as e -> raise e - | e -> - let e = CErrors.push e in - raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))) - () + try f (); raise HasNotFailed + with + | HasNotFailed as e -> raise e + | e -> + let e = CErrors.push e in + raise (HasFailed (CErrors.iprint + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> + (* Restore the previous state XXX Careful here with the cache! *) + invalidate_cache (); + unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2175,7 +2200,7 @@ let with_fail b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof (loc,c) = +let interp ?(verbosely=true) ?proof st (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function @@ -2188,7 +2213,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") | VernacLocal _ -> user_err Pp.(str "Locality specified twice") | VernacFail v -> - with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) + with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v @@ -2227,3 +2252,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = in if verbosely then Flags.verbosely (aux false) c else aux false c + +let interp ?verbosely ?proof st cmd = + unfreeze_interp_state st; + interp ?verbosely ?proof st cmd; + freeze_interp_state `No diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a09011d24..56635c801 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,11 +14,21 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> interp_state +val unfreeze_interp_state : interp_state -> unit + (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Vernacexpr.vernac_expr Loc.located -> unit + interp_state -> + Vernacexpr.vernac_expr Loc.located -> interp_state (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -28,7 +38,9 @@ val interp : val make_cases : string -> string list list -val with_fail : bool -> (unit -> unit) -> unit +(* XXX STATE: this type hints that restoring the state should be the + caller's responsibility *) +val with_fail : interp_state -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind |