diff options
38 files changed, 391 insertions, 192 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fb4d073337..f344c5cf55 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -37,8 +37,12 @@ /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes -/doc/ @silene -# Secondary maintainer @maximedenes +/dev/doc/changes.md @ghost +# Trick to avoid getting review requests +# each time someone modifies the dev changelog + +/doc/ @maximedenes +# Secondary maintainer @silene /man/ @silene # Secondary maintainer @maximedenes @@ -104,8 +108,8 @@ /plugins/btauto/ @ppedrot # Secondary maintainer @herbelin -# I don't know Pierre Corbineau's GitHub nickname -/plugins/cc/ @herbelin +/plugins/cc/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/derive/ @aspiwack # Secondary maintainer @ppedrot @@ -113,8 +117,8 @@ /plugins/extraction/ @letouzey # Secondary maintainer @maximedenes -# I don't know Pierre Corbineau's GitHub nickname -/plugins/firstorder/ @herbelin +/plugins/firstorder/ @PierreCorbineau +# Secondary maintainer @herbelin /plugins/fourier/ @herbelin # Secondary maintainer @gares @@ -149,8 +153,8 @@ /plugins/quote/ @herbelin -# Should be Pierre Corbineau too -/plugins/rtauto/ @herbelin +/plugins/rtauto/ @PierreCorbineau +# Secondary maintainer @herbelin ########## Pretyper ########## @@ -294,6 +298,9 @@ /META.coq @ejgallego # Secondary maintainer @letouzey +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## Developer tools ########## @@ -124,7 +124,7 @@ Tools - Coq can now be run with the option -mangle-names to change the auto-generated name scheme. This is intended to function as a linter for developments that want to be robust to changes in auto-generated names. This feature is experimental, - and may change or dissapear without warning. + and may change or disappear without warning. - GeoProof support was removed. Checker diff --git a/dev/base_include b/dev/base_include index 1fb80dc074..e76044f415 100644 --- a/dev/base_include +++ b/dev/base_include @@ -232,7 +232,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc) +let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc) let _ = print_string diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8c8c0d8be9..8e0d2341d0 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -854,7 +854,7 @@ function make_ocaml_libs { function make_findlib { make_ocaml - if build_prep http://download.camlcity.org/download findlib-1.5.6 tar.gz 1 ; then + if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index f1dddbd0ef..71fc396088 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -30,8 +30,8 @@ When maintainers receive a review request, they are expected to: * If they are the assignee, check if all reviewers approved the PR. If not, regularly ping the author (if changes should be implemented) or the reviewers (if reviews are missing). The assignee ensures that any requests for more - discussion have been granted. When the discussion has converged and all - reviewers have approved the PR, the assignee is expected to follow the merging + discussion have been granted. When the discussion has converged and ALL + REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. In all cases, maintainers can delegate reviews to the other maintainer of the @@ -41,6 +41,11 @@ patch. A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. +(*) In case a component is touched in a trivial way (adding/removing one file in +a `Makefile`, etc), or by applying a systematic process (global renaming, +deprecationg propagation, etc) that has been reviewed globally, the assignee can +say in a comment they think a review is not required and proceed with the merge. + ## Merging Once all reviewers approved the PR, the assignee is expected to check that CI @@ -49,6 +54,17 @@ documentation and test cases. If not, they should leave a comment on the PR and put the approriate label. Otherwise, they are expected to merge the PR using the [merge script](/dev/tools/merge-pr.sh). +When the PR has conflicts, the assignee can either: +- ask the author to rebase the branch, fixing the conflicts +- warn the author that they are going to rebase the branch, and push to the + branch directly + +In both cases, CI should be run again. + +In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix +the conflicts in the merge commit (following the same steps as below), and push +to `master` directly. Don't use the GitHub interface to fix these conflicts. + The command to be used is: ``` $ dev/tools/merge-pr XXXX @@ -56,3 +72,7 @@ $ dev/tools/merge-pr XXXX where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. Maintainers MUST NOT merge their own patches. + +DON'T USE the GitHub interface for merging, since it will prevent the automated +backport script from operating properly, generates bad commit messages, and a +messy history when there are conflicts. diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 9f24960fff..2f6f1af541 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -1,50 +1,157 @@ #!/usr/bin/env bash set -e +set -o pipefail + +API=https://api.github.com/repos/coq/coq +OFFICIAL_REMOTE_URL="git@github.com:coq/coq" # This script depends (at least) on git and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ -#TODO: check arguments and show usage if relevant +RED="\033[31m" +RESET="\033[0m" +GREEN="\033[32m" +BLUE="\033[34m" +YELLOW="\033[33m" +info() { + echo -e "${GREEN}info:${RESET} $1 ${RESET}" +} +error() { + echo -e "${RED}error:${RESET} $1 ${RESET}" +} +warning() { + echo -e "${YELLOW}warning:${RESET} $1 ${RESET}" +} -PR=$1 +check_util() { +if ! command -v "$1" > /dev/null 2>&1; then + error "this script requires the $1 command line utility" + exit 1 +fi +} -CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) -REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") -git fetch "$REMOTE" "refs/pull/$PR/head" +ask_confirmation() { + read -p "Continue anyway? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]] + then + exit 1 + fi +} -API=https://api.github.com/repos/coq/coq +check_util jq +check_util curl +check_util git +check_util gpg + +# command line parsing + +if [ $# != 1 ]; then + error "usage: $0 PR-number" + exit 1 +fi + +if [[ "$1" =~ ^[1-9][0-9]*$ ]]; then + PR=$1 +else + error "$1 is not a number" + exit 1 +fi + +# Fetching PR metadata + +TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title') +info "title for PR $PR is ${BLUE}$TITLE" BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') +info "PR $PR targets branch ${BLUE}$BASE_BRANCH" + +CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) +info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" +REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") +if [ -z "$REMOTE" ]; then + error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote" + error "don't know where to fetch the PR from" + error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH" + exit 1 +fi +REMOTE_URL=$(git remote get-url "$REMOTE" --push) +if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \ + "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then + error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" + error "that is ${BLUE}$OFFICIAL_REMOTE_URL" + error "it points to ${BLUE}$REMOTE_URL${RESET} instead" + ask_confirmation +fi +info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE" + +info "fetching from $REMOTE the PR" +git remote update "$REMOTE" +if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then + error "remote $REMOTE is not configured to fetch pull requests" + error "run: git config remote.$REMOTE.fetch +refs/pull/*/head:refs/remotes/$REMOTE/pr/*" + exit 1 +fi +git fetch "$REMOTE" "refs/pull/$PR/head" COMMIT=$(git rev-parse FETCH_HEAD) -STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') +info "commit for PR $PR is ${BLUE}$COMMIT" + +# Sanity check: merge to a different branch if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then - echo "Wrong base branch" - read -p "Bypass? [y/N] " -n 1 -r - echo - if [[ ! $REPLY =~ ^[Yy]$ ]] - then - exit 1 - fi + error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" + ask_confirmation fi; +# Sanity check: CI failed + +STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') + if [ "$STATUS" != "success" ]; then - echo "CI status is \"$STATUS\"" - read -p "Bypass? [y/N] " -n 1 -r - echo - if [[ ! $REPLY =~ ^[Yy]$ ]] - then - exit 1 - fi + error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" | + jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" + ask_confirmation fi; -git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e +# Sanity check: has labels named "needs:" + +NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') +if [ "$NEEDS_LABELS" != "[]" ]; then + error "needs:something labels still present: ${BLUE}$NEEDS_LABELS" + ask_confirmation +fi + +# Sanity check: has milestone + +MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title') +if [ "$MILESTONE" = "null" ]; then + error "no milestone set, please set one" + ask_confirmation +fi + +# Sanity check: has kind + +KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)') +if [ "$KIND" = "[]" ]; then + error "no kind:something label set, please set one" + ask_confirmation +fi + +# Sanity check: user.signingkey +if [ -z "$(git config user.signingkey)" ]; then + warning "git config user.signingkey is empty" + warning "gpg will guess a key out of your git config user.* data" +fi + +info "merging" +git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e # TODO: improve this check -if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then - echo "******************************************" - echo "** WARNING: does this PR have overlays? **" - echo "******************************************" +if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then + warning "this PR may have overlays (sorry the check is not perfect)" + warning "if it has overlays please check the following:" + warning "- each overlay has a corresponding open PR on the upstream repo" + warning "- after merging please notify the upstream they can merge the PR" fi diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 9cf81eccea..45760c6b4b 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -807,11 +807,11 @@ let judge_of_new_Type evd = let (evd', s) = new_univ_variable univ_rigid evd in (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) -let subterm_source evk (loc,k) = +let subterm_source evk ?where (loc,k) = let evk = match k with - | Evar_kinds.SubEvar (evk) -> evk + | Evar_kinds.SubEvar (None,evk) when where = None -> evk | _ -> evk in - (loc,Evar_kinds.SubEvar evk) + (loc,Evar_kinds.SubEvar (where,evk)) (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e289ca1692..972b0b9e1c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -254,7 +254,7 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a -val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> +val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located val meta_counter_summary_tag : int Summary.Dyn.tag diff --git a/engine/termops.ml b/engine/termops.ml index 3dfb0c34fd..b7531f6fc9 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -206,8 +206,12 @@ let pr_evar_source = function | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id - | Evar_kinds.SubEvar evk -> - str "subterm of " ++ Evar.print evk + | Evar_kinds.SubEvar (where,evk) -> + (match where with + | None -> str "subterm of " + | Some Evar_kinds.Body -> str "body of " + | Some Evar_kinds.Domain -> str "domain of " + | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk let pr_evar_info evi = let open Evd in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 6b7efc839e..2e552b60bb 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -359,8 +359,6 @@ let handle_exn (e, info) = | _ -> None in let mk_msg () = CErrors.print ~info e in match e with - | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!" - | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index c5de383b21..c964ecf1f5 100644 --- a/intf/evar_kinds.ml +++ b/intf/evar_kinds.ml @@ -21,6 +21,8 @@ type obligation_definition_status = Define of bool | Expand type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar +type subevar_kind = Domain | Codomain | Body + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) @@ -34,4 +36,4 @@ type t = | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Id.t - | SubEvar of Evar.t + | SubEvar of subevar_kind option * Evar.t diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index df061bfb72..dc1110ad86 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -457,8 +457,6 @@ type nonrec vernac_expr = | VernacCheckGuard | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string - (* Toplevel control *) - | VernacToplevelControl of exn (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 9750221143..811fcf4063 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -47,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *) let alreadydeclared pps = raise (AlreadyDeclared(pps)) exception Timeout -exception Drop -exception Quit let handle_stack = ref [] @@ -126,7 +124,7 @@ end let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ - | Timeout | Drop | Quit -> false + | Timeout -> false | Invalid_argument "equal: functional value" -> false | _ -> true [@@@ocaml.warning "+52"] diff --git a/lib/cErrors.mli b/lib/cErrors.mli index ec34dd62c5..4e2fe7621d 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -53,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a val todo : string -> unit exception Timeout -exception Drop -exception Quit (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 72c3cc14a1..8543d2b849 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -845,10 +845,6 @@ GEXTEND Gram | IDENT "Cd" -> VernacChdir None | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) - (* Toplevel control *) - | IDENT "Drop" -> VernacToplevelControl Drop - | IDENT "Quit" -> VernacToplevelControl Quit - | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 31f55ae9c3..458844e1b9 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -211,7 +211,7 @@ Set Implicit Arguments. (* BC *) simpl. case_eq (deduce t t) ; auto. - intros until 0. + intros *. case_eq (unsat t0) ; auto. unfold eval_clause. rewrite make_conj_cons. @@ -263,7 +263,7 @@ Set Implicit Arguments. Proof. induction cl. simpl. tauto. - intros until 0. + intros *. simpl. assert (HH := add_term_correct env a cl'). case_eq (add_term a cl'). diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a5b7a9e6f0..73be9d6b78 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1662,7 +1662,7 @@ let rec list_assoc_in_triple x = function let abstract_tycon ?loc env evdref subst tycon extenv t = let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with - | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk)) | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 03f40ad92e..4cffbbb837 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -19,6 +19,7 @@ open Vars open Namegen open Evd open Evarutil +open Evar_kinds open Pretype_errors module RelDecl = Context.Rel.Declaration @@ -78,12 +79,14 @@ let define_pure_evar_as_product evd evk = let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in let s = destSort evd concl in + let evksrc = evar_source evk evd in + let src = subterm_source evk ~where:Domain evksrc in let evd1,(dom,u1) = - new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) + new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (LocalAssum (id, dom)) evenv in - let src = evar_source evk evd1 in + let src = subterm_source evk ~where:Codomain evksrc in let filter = Filter.extend 1 (evar_filter evi) in if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) @@ -135,7 +138,7 @@ let define_pure_evar_as_lambda env evd evk = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in - let src = evar_source evk evd1 in + let src = subterm_source evk ~where:Body (evar_source evk evd1) in let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5c5b7206a5..7df0a0c94a 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -181,8 +181,6 @@ open Decl_kinds | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b - let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" - let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z @@ -1188,10 +1186,6 @@ open Decl_kinds ++ prlist_with_sep sep (pr_comment pr_constr) l) ) - (* Toplevel control *) - | VernacToplevelControl exn -> - return (pr_topcmd exn) - (* For extension *) | VernacExtend (s,c) -> return (pr_extend s c) diff --git a/stm/stm.ml b/stm/stm.ml index dbecbdae54..e970a02eed 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2734,7 +2734,6 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - if e = CErrors.Drop then Exninfo.iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2885,23 +2884,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - (* Side effect on all branches *) - | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); - `Ok - + (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; - VCS.commit id (mkTransCmd x l in_proof `MainQueue); - (* We can't replay a Definition since universes may be differently - * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with - | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv - | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); + | `Proof _ -> + VCS.checkout VCS.Branch.master; + VCS.commit id (mkTransCmd x l true `MainQueue); + (* We can't replay a Definition since universes may be differently + * inferred. This holds in Coq >= 8.5 *) + let action = match Vernacprop.under_control x.expr with + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; + end; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2930,9 +2928,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; end else begin - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Proof _ -> + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + (* We hope it can be replayed, but we can't really know *) + VCS.propagate_sideff ~action:(ReplayCommand x); + end; VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f68c8b326b..9a8af3a58c 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,7 +185,6 @@ let classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) - | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index df3cca1447..834d73bdda 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1102,7 +1102,13 @@ let msg_quantified_hypothesis = function pr_nth n ++ str " non dependent hypothesis" +let warn_deprecated_intros_until_0 = + CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics" + (fun () -> + strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"") + let depth_of_quantified_hypothesis red h gl = + if h = AnonHyp 0 then warn_deprecated_intros_until_0 (); match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake new file mode 100644 index 0000000000..e2a2aa52a0 --- /dev/null +++ b/test-suite/ide/bug7088.fake @@ -0,0 +1,13 @@ +ADD { Arguments id T x : rename. } +ADD { Lemma foo : True. } +ADD here { Proof. } +ADD { exact 3. } +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Arguments id FOO BAR : rename. } +ADD { exact I. } +ADD { Qed. } +ADD { Arguments id T x : assert. } +JOIN + diff --git a/test-suite/ide/load.fake b/test-suite/ide/load.fake new file mode 100644 index 0000000000..f6a7ef4dcb --- /dev/null +++ b/test-suite/ide/load.fake @@ -0,0 +1,11 @@ +ADD revert { Load "output/load/Load_noproof.v". } +ADD { Load "output/load/Load_proof.v". } +ADD { Fail Load "output/load/Load_openproof.v". } +WAIT +QUERY { Check f. } +QUERY { Check u. } +EDIT_AT revert +QUERY { Check f. } +QUERY { Fail Check u. } +JOIN + diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 38d055b28e..24180c4553 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -8,3 +8,11 @@ Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. +The command has indeed failed with message: +Cannot infer the domain of the type of f. +The command has indeed failed with message: +Cannot infer the domain of the implicit parameter A of id whose type is +"Type". +The command has indeed failed with message: +Cannot infer the codomain of the type of f in environment: +x : nat diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 424d24801c..c9b5091347 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -25,3 +25,9 @@ eexists ?[x]. destruct H1 as [x1 H1]. Fail instantiate (x:=projT1 x1). Abort. + +(* Test some messages for non solvable evars *) + +Fail Goal forall a f, f a = 0. +Fail Goal forall f x, id f x = 0. +Fail Goal forall f P, P (f 0). diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 96a0bd5ec5..3e7a830856 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -23,12 +23,12 @@ let set_debug () = let rcdefaultname = "coqrc" -let load_rcfile ~rcfile ~time ~state = +let load_rcfile ~rcfile ~state = try match rcfile with | Some rcfile -> if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) | None -> try @@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc with Not_found -> state (* Flags.if_verbose diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 71b5523cde..c891e736b4 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -12,12 +12,12 @@ val set_debug : unit -> unit -val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t +val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Mltop.coq_path list +val toplevel_init_load_path : unit -> Mltop.coq_path list (* LoadPath for Coq user libraries *) val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index a103cfe7f3..64d839f18b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -261,8 +261,8 @@ let rec discard_to_dot () = | e when CErrors.noncritical e -> () let read_sentence ~state input = - let open Vernac.State in - try Stm.parse_sentence ~doc:state.doc state.sid input + (* XXX: careful with ignoring the state Eugene!*) + try G_toplevel.parse_toplevel input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -293,40 +293,6 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer -(** [do_vernac] reads and executes a toplevel phrase, and print error - messages when an exception is raised, except for the following: - - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists. - Otherwise, exit. - - End_of_input: Ctrl-D was typed in, we will quit. - - In particular, this is normally the only place where a Sys.Break - is caught and handled (i.e. not re-raised). -*) - -let do_vernac ~time ~state = - let open Vernac.State in - top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); - resynch_buffer top_buffer; - try - let input = (top_buffer.tokens, None) in - Vernac.process_expr ~time ~state (read_sentence ~state (fst input)) - with - | Stm.End_of_input | CErrors.Quit -> - top_stderr (fnl ()); raise CErrors.Quit - | CErrors.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_warning (str "There is no ML toplevel."); state) - (* Exception printing should be done by the feedback listener, - however this is not yet ready so we rely on the exception for - now. *) - | any -> - let (e, info) = CErrors.push any in - let loc = Loc.get_loc info in - let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; - state - (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. Normally, the only exceptions that can come out of [do_vernac] and @@ -359,37 +325,55 @@ let cproof p1 p2 = let drop_last_doc = ref None -let rec loop ~time ~state = +(* Careful to keep this loop tail-rec *) +let rec vernac_loop ~state = + let open CAst in let open Vernac.State in - Sys.catch_break true; + let open G_toplevel in + loop_flush_all (); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); + resynch_buffer top_buffer; + (* execute one command *) try - reset_input_buffer state.doc stdin top_buffer; - (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop ~state = - let nstate = do_vernac ~time ~state in + let input = top_buffer.tokens in + match read_sentence ~state input with + | {v=VernacQuit} -> + exit 0 + | {v=VernacDrop} -> + if Mltop.is_ocaml_top() + then (drop_last_doc := Some state; state) + else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) + | {v=VernacControl c; loc} -> + let nstate = Vernac.process_expr ~state (make ?loc c) in let proof_changed = not (Option.equal cproof nstate.proof state.proof) in let print_goals = not !Flags.quiet && proof_changed && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - loop_flush_all (); vernac_loop ~state:nstate - (* We recover the current stateid, threading from the caller is - not possible due exceptions. *) - in vernac_loop ~state with - | CErrors.Drop -> - (* Due to using exceptions as a form of control, state here goes - out of sync as [do_vernac] will never return. We must thus do - this hack until we make `Drop` a toplevel-only command. See - bug #6872. *) - let state = { state with sid = Stm.get_current_state ~doc:state.doc } in - drop_last_doc := Some state; - state - | CErrors.Quit -> exit 0 + | Stm.End_of_input -> + top_stderr (fnl ()); exit 0 + (* Exception printing should be done by the feedback listener, + however this is not yet ready so we rely on the exception for + now. *) + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + vernac_loop ~state + +let rec loop ~state = + let open Vernac.State in + Sys.catch_break true; + try + reset_input_buffer state.doc stdin top_buffer; + vernac_loop ~state + with | any -> - top_stderr (str "Anomaly: main loop exited with exception: " ++ - str (Printexc.to_string any) ++ - fnl() ++ - str"Please report" ++ - strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop ~time ~state + top_stderr + (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++ + str (Printexc.to_string any)) ++ spc () ++ + hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); + loop ~state diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index bbb9b1383a..39a9de4f83 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -32,11 +32,8 @@ val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) val coqloop_feed : Feedback.feedback -> unit -(** Parse and execute one vernac command. *) -val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t - (** Main entry point of Coq: read and execute vernac commands. *) -val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t +val loop : state:Vernac.State.t -> Vernac.State.t (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cd831c05ca..a08cfa9f48 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -45,7 +45,7 @@ let console_toploop_run opts ~state = Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let _ = Coqloop.loop ~time:opts.time ~state in + let _ = Coqloop.loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); @@ -95,7 +95,7 @@ let load_vernacular opts ~state = (fun state (f_in, echo) -> let s = Loadpath.locate_file f_in in (* Should make the beautify logic clearer *) - let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in + let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s @@ -103,7 +103,7 @@ let load_vernacular opts ~state = let load_init_vernaculars opts ~state = let state = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -223,7 +223,7 @@ let compile opts ~echo ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file @@ -232,7 +232,7 @@ let compile opts ~echo ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -270,10 +270,10 @@ let compile opts ~echo ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -476,7 +476,7 @@ let init_toplevel arglist = { doc_type = Interactive opts.toplevel_name; iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in Some (load_init_vernaculars opts ~state), opts with any -> flush_all(); fatal_error_exn any (* Non interactive: we perform a sequence of compilation steps *) diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4 new file mode 100644 index 0000000000..7526f3071a --- /dev/null +++ b/toplevel/g_toplevel.ml4 @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pcoq +open Vernacexpr + +(* Vernaculars specific to the toplevel *) +type vernac_toplevel = + | VernacDrop + | VernacQuit + | VernacControl of vernac_control + +module Toplevel_ : sig + val vernac_toplevel : vernac_toplevel CAst.t Gram.entry +end = struct + let gec_vernac s = Gram.entry_create ("toplevel:" ^ s) + let vernac_toplevel = gec_vernac "vernac_toplevel" +end + +open Toplevel_ + +GEXTEND Gram + GLOBAL: vernac_toplevel; + vernac_toplevel: FIRST + [ [ IDENT "Drop"; "." -> CAst.make VernacDrop + | IDENT "Quit"; "." -> CAst.make VernacQuit + | cmd = main_entry -> + match cmd with + | None -> raise Stm.End_of_input + | Some (loc,c) -> CAst.make ~loc (VernacControl c) + ] + ] + ; +END + +let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 9fb2e33d74..78b96e5e27 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,5 +1,6 @@ Vernac Usage +G_toplevel Coqloop Coqinit Coqargs diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fdd0d4ed37..c1bbb20d5e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -28,10 +28,6 @@ let checknav_deep {CAst.loc;v=ast} = if is_deep_navigation_vernac ast then CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.") -let disable_drop = function - | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") - | e -> e - (* Echo from a buffer based on position. XXX: Should move to utility file. *) let vernac_echo ?loc in_chan = let open Loc in @@ -80,17 +76,21 @@ module State = struct doc : Stm.doc; sid : Stateid.t; proof : Proof.t option; + time : bool; } end -let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = +let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let open State in try (* The -time option is only supported from console-based clients due to the way it prints. *) - if time then print_cmd_header com; - let com = if time then CAst.make ?loc @@ VernacTime(time,com) else com in + let com = if state.time + then begin + print_cmd_header com; + CAst.make ?loc @@ VernacTime(state.time,com) + end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in (* Main STM interaction *) @@ -102,7 +102,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = (* Stm.observe nsid; *) let ndoc = if check then Stm.finish ~doc else doc in let new_proof = Proof_global.give_me_the_proof_opt () in - { doc = ndoc; sid = nsid; proof = new_proof } + { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) @@ -115,7 +115,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -let load_vernac_core ~time ~echo ~check ~interactive ~state file = +let load_vernac_core ~echo ~check ~interactive ~state file = (* Keep in sync *) let in_chan = open_utf8_file_in file in let in_echo = if echo then Some (open_utf8_file_in file) else None in @@ -154,7 +154,7 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple ast; - let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) ast in + let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in rids := state.sid :: !rids; rstate := state; done; @@ -165,11 +165,11 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = input_cleanup (); match e with | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa - | reraise -> iraise (disable_drop e, info) + | reraise -> iraise (e, info) -let process_expr ~time ~state loc_ast = +let process_expr ~state loc_ast = checknav_deep loc_ast; - interp_vernac ~time ~interactive:true ~check:true ~state loc_ast + interp_vernac ~interactive:true ~check:true ~state loc_ast (******************************************************************************) (* Beautify-specific code *) @@ -220,8 +220,8 @@ let beautify_pass ~doc ~comments ~ids ~filename = (* Main driver for file loading. For now, we only do one beautify pass. *) -let load_vernac ~time ~echo ~check ~interactive ~state filename = - let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in +let load_vernac ~echo ~check ~interactive ~state filename = + let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in (* Pass for beautify *) if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename; (* End pass *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 51758642e7..1269540235 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -15,6 +15,7 @@ module State : sig doc : Stm.doc; sid : Stateid.t; proof : Proof.t option; + time : bool; } end @@ -23,10 +24,10 @@ end expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t +val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool -> +val load_vernac : echo:bool -> check:bool -> interactive:bool -> state:State.t -> string -> State.t diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 249e7893c2..698ee4703a 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -559,15 +559,21 @@ let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.VarInstance id -> strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id - | Evar_kinds.SubEvar evk' -> + | Evar_kinds.SubEvar (where,evk') -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c) | Evar_empty -> assert false in let ty' = EConstr.of_constr evi.evar_concl in + (match where with + | Some Evar_kinds.Body -> str "the body of " + | Some Evar_kinds.Domain -> str "the domain of " + | Some Evar_kinds.Codomain -> str "the codomain of " + | None -> pr_existential_key sigma evk ++ str " of type " ++ ty ++ str " in the partial instance " ++ pc ++ - str " found for " ++ explain_evar_kind env sigma evk' + str " found for ") ++ + explain_evar_kind env sigma evk' (pr_leconstr_env env sigma ty') (snd evi.evar_source) let explain_typeclass_resolution env sigma evi k = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3dbe8b0c09..9ff4e33020 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2010,9 +2010,6 @@ let interp ?proof ~atts ~st c = | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") - (* Toplevel control *) - | VernacToplevelControl e -> raise e - (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1f2d2e4b42..d4f2a753ff 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -79,7 +79,6 @@ let call opn converted_args ~atts ~st = phase := "Executing command"; hunk ~atts ~st with - | Drop -> raise Drop | reraise -> let reraise = CErrors.push reraise in if !Flags.debug then |