From 4944b5e72c0f4bfcf1ae140f810d8666dac3cf60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 May 2015 14:26:35 +0200 Subject: Make Coercion.inh_app_fun respect its specification. It enhances bug #3527, as instead of raising an anomaly "Uncaught exception Coercion.NoCoercion(_)", it now fails with a typing error. --- pretyping/coercion.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f5135f5c60..6765ca130b 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -378,7 +378,8 @@ let inh_app_fun env evd j = try let t,p = lookup_path_to_fun_from env evd j.uj_type in apply_coercion env evd p j t - with Not_found | NoCoercion when Flags.is_program_mode () -> + with Not_found | NoCoercion -> + if Flags.is_program_mode () then try let evdref = ref evd in let coercef, t = mu env evdref t in @@ -386,6 +387,7 @@ let inh_app_fun env evd j = (!evdref, res) with NoSubtacCoercion | NoCoercion -> (evd,j) + else (evd, j) let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j -- cgit v1.2.3 From 15dc0ff339e01341e11c5dec63689ddc3e500e96 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 May 2015 15:00:59 +0200 Subject: Granting wish #4048: Locate Ltac prints the source of redefined Ltac. --- tactics/tacenv.ml | 36 +++++++++++++++++++++++++----------- tactics/tacenv.mli | 13 +++++++++++++ tactics/tacintern.ml | 17 +++++++++++++++-- 3 files changed, 53 insertions(+), 13 deletions(-) diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 08e8bc0112..09a98bc8cc 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -75,34 +75,48 @@ let interp_ml_tactic s = open Nametab open Libobject +type ltac_entry = { + tac_for_ml : bool; + tac_body : glob_tactic_expr; + tac_redef : ModPath.t list; +} + let mactab = - Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t) + Summary.ref (KNmap.empty : ltac_entry KNmap.t) ~name:"tactic-definition" -let interp_ltac r = snd (KNmap.find r !mactab) +let ltac_entries () = !mactab + +let interp_ltac r = (KNmap.find r !mactab).tac_body + +let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) +let add kn b t = + let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in + mactab := KNmap.add kn entry !mactab -(* Declaration of the TAC-DEFINITION object *) -let add (kn,td) = mactab := KNmap.add kn td !mactab +let replace kn path t = + let (path, _, _) = KerName.repr path in + let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in + mactab := KNmap.modify kn entry !mactab let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Until i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Exactly i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> let () = Nametab.push_tactic (Until 1) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 9410ccb389..2df6bb04a2 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -44,6 +44,19 @@ val interp_ltac : KerName.t -> glob_tactic_expr (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *) val is_ltac_for_ml_tactic : KerName.t -> bool +(** Whether the tactic is defined from ML-side *) + +type ltac_entry = { + tac_for_ml : bool; + (** Whether the tactic is defined from ML-side *) + tac_body : glob_tactic_expr; + (** The current body of the tactic *) + tac_redef : ModPath.t list; + (** List of modules redefining the tactic in reverse chronological order *) +} + +val ltac_entries : unit -> ltac_entry KNmap.t +(** Low-level access to all Ltac entries currently defined. *) (** {5 ML tactic extensions} *) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 5cc4c835bc..d4c67b90fb 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -809,11 +809,24 @@ let pr_ltac_fun_arg = function let print_ltac id = try let kn = Nametab.locate_tactic id in - let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + let filter mp = + try Some (Nametab.shortest_qualid_of_module mp) + with Not_found -> None + in + let mods = List.map_filter filter tac.Tacenv.tac_redef in + let redefined = match mods with + | [] -> mt () + | mods -> + let redef = prlist_with_sep fnl pr_qualid mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in + let l,t = split_ltac_fun tac.Tacenv.tac_body in hv 2 ( hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) + ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> errorlabstrm "print_ltac" -- cgit v1.2.3 From 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 15 May 2015 17:42:16 +0200 Subject: On MacOS X, ensuring that files found in the file system have the expected lowercase/uppercase spelling (based on a patch by Pierre B.). This should fix #2554 (and see also discussion on coq-club, May 2015). --- lib/system.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc9..6364035e16 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,6 +53,19 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l +let file_really_exists f = + if Coq_config.arch = "Darwin" then + (* ensure that the file exists with expected case on the + case-insensitive but case-preserving default MacOS file system *) + let rec aux f = + Printf.eprintf ".%!"; + let bf = Filename.basename f in + let df = Filename.dirname f in + String.equal df "." || String.equal df "/" || + aux df && Array.exists (String.equal bf) (Sys.readdir df) + in aux f + else Sys.file_exists f + let rec search paths test = match paths with | [] -> [] -- cgit v1.2.3 From cd6e8689abff88f03872840d12f177d06fccda05 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 15 May 2015 22:35:51 +0200 Subject: Removing option -no-native-compiler from test #3539 since this option is now negated into -native-compiler. --- test-suite/bugs/closed/3539.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v index c862965d4d..d258bb31f8 100644 --- a/test-suite/bugs/closed/3539.v +++ b/test-suite/bugs/closed/3539.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-no-native-compiler") -*- *) +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *) (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0 coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *) @@ -63,4 +63,4 @@ x' : forall (_ : T1) (_ : T), T2 m : T3 (x' fst1 x2) (x' fst0 x2) Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with "?25 ?27". - *) \ No newline at end of file + *) -- cgit v1.2.3 From b14d88c8cd17ad524898b31c1772a0e8f70f19f8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 16 May 2015 12:33:32 +0200 Subject: Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone". --- tactics/tactics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2791d7c484..402a9e88a1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3597,8 +3597,11 @@ let find_induction_type isrec elim hyp0 gl = if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in - scheme, ElimUsing (elim,indsign) in - (Option.get scheme.indref,scheme.nparams, elim) + scheme, ElimUsing (elim,indsign) + in + match scheme.indref with + | None -> error_ind_scheme "" + | Some ref -> ref, scheme.nparams, elim let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 -- cgit v1.2.3 From b07c8f1224d63de6172567b04b9e008c4f18de1a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 May 2015 16:44:19 +0200 Subject: Fixing bug #4201: The native compiler is not race-free. Instead of checking if the native compiler directory exists before creating it, we simply create it by default and catch the potential exception due to its presence. --- kernel/nativelib.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 605c1225c7..29b6bf6de7 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -94,7 +94,10 @@ let compile_library dir code fn = let basename = Filename.basename fn in let dirname = Filename.dirname fn in let dirname = dirname / output_dir in - if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755; + let () = + try Unix.mkdir dirname 0o755 + with Unix.Unix_error (Unix.EEXIST, _, _) -> () + in let fn = dirname / basename in write_ml_code fn ~header code; let r = fst (call_compiler fn) in -- cgit v1.2.3 From 41f0f4a53fd462cd7e0bb190ebd547409a0873de Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 18 May 2015 14:50:28 +0200 Subject: Adding the -color option to coqc. coqc by default uses colors, this allows to disable it. Moreover, colors are not yet correctly disabled when compiling from emacs (emacs bugs?), making this option even more useful. --- tools/coqc.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/coqc.ml b/tools/coqc.ml index aed229abc8..5710b97f2a 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,18 +111,18 @@ let parse_args () = |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-indices-matter"|"-quick"|"-color"|"-type-in-type" + |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem (* Options for coqtop : b) options with 1 argument *) - | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" as o) :: rem -> begin match rem with -- cgit v1.2.3 From 22eb2d34f0a9249720a30c6cb2973993e97834ea Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 18 May 2015 15:39:55 +0200 Subject: Fix usage about -color. --- toplevel/usage.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 50fb019f47..36ecc9fa5f 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -58,7 +58,7 @@ let print_usage_channel co command = \n\ \n -quiet unset display of extra information (implies -w none)\ \n -w (all|none) configure display of warnings\ -\n -color (on|off|auto) configure color output (only active through coqtop)\ +\n -color (on|off|auto) configure color output\ \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -- cgit v1.2.3 From 5b66cfdae503a10b724c111f35ceb001a705a95d Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 18 May 2015 15:45:07 +0200 Subject: Disabling colors when tERM variable is "dumb". This disables colors in emacs compilation buffer, which does not support ansi colors by default. --- toplevel/coqtop.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index af7169ad6c..7ba0c55a15 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -58,7 +58,10 @@ let init_color () = | `ON -> true | `AUTO -> Terminal.has_style Unix.stdout && - Terminal.has_style Unix.stderr + Terminal.has_style Unix.stderr && + (* emacs compilation buffer does not support colors by default, + its TERM variable is set to "dumb". *) + Unix.getenv "TERM" <> "dumb" in if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in -- cgit v1.2.3 From c3a62d51d13788a650fc13e89a1b6f000ba1f378 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 18 May 2015 15:47:57 +0200 Subject: Fixed CHANGES to reflect -color option. --- CHANGES | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index d2890f7402..b6793e426f 100644 --- a/CHANGES +++ b/CHANGES @@ -418,7 +418,7 @@ Interfaces - Many CoqIDE windows, including the query one, are now detachable to improve usability on multi screen work stations. -- Coqtop outputs highlighted syntax. Colors can be configured thanks +- Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks to the COQ_COLORS environment variable, and their current state can be displayed with the -list-tags command line option. -- cgit v1.2.3 From 923ce36ed6789718746369847f622b17bb37df2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 May 2015 15:29:55 +0200 Subject: Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeError. Instad of trying to print the exception, we raise it in the tactic monad. --- proofs/clenvtac.ml | 4 +--- test-suite/bugs/closed/3461.v | 5 +++++ test-suite/bugs/opened/3461.v | 5 ----- 3 files changed, 6 insertions(+), 8 deletions(-) create mode 100644 test-suite/bugs/closed/3461.v delete mode 100644 test-suite/bugs/opened/3461.v diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 18883df247..aaa49f1169 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -125,7 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m = try let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' - with e when Errors.noncritical e -> - (** This is Tacticals.tclFAIL *) - Proofview.tclZERO (FailError (0, lazy (Errors.print e))) + with e when Errors.noncritical e -> Proofview.tclZERO e end diff --git a/test-suite/bugs/closed/3461.v b/test-suite/bugs/closed/3461.v new file mode 100644 index 0000000000..1b625e6a15 --- /dev/null +++ b/test-suite/bugs/closed/3461.v @@ -0,0 +1,5 @@ +Lemma foo (b : bool) : + exists x : nat, x = x. +Proof. +eexists. +Fail eexact (eq_refl b). diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v deleted file mode 100644 index 1b625e6a15..0000000000 --- a/test-suite/bugs/opened/3461.v +++ /dev/null @@ -1,5 +0,0 @@ -Lemma foo (b : bool) : - exists x : nat, x = x. -Proof. -eexists. -Fail eexact (eq_refl b). -- cgit v1.2.3 From b994685d85d30f0db8ee0ec10f802f6bf3797e4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 May 2015 16:59:50 +0200 Subject: Removing test for opened bugs that were already present in the closed test-suite. --- test-suite/bugs/opened/3045.v | 30 ------------------------------ test-suite/bugs/opened/3326.v | 18 ------------------ test-suite/bugs/opened/3562.v | 2 -- test-suite/bugs/opened/3657.v | 33 --------------------------------- test-suite/bugs/opened/3670.v | 19 ------------------- test-suite/bugs/opened/3675.v | 20 -------------------- test-suite/bugs/opened/3788.v | 5 ----- test-suite/bugs/opened/3808.v | 2 -- 8 files changed, 129 deletions(-) delete mode 100644 test-suite/bugs/opened/3045.v delete mode 100644 test-suite/bugs/opened/3326.v delete mode 100644 test-suite/bugs/opened/3562.v delete mode 100644 test-suite/bugs/opened/3657.v delete mode 100644 test-suite/bugs/opened/3670.v delete mode 100644 test-suite/bugs/opened/3675.v delete mode 100644 test-suite/bugs/opened/3788.v delete mode 100644 test-suite/bugs/opened/3808.v diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v deleted file mode 100644 index b7f40b4ad7..0000000000 --- a/test-suite/bugs/opened/3045.v +++ /dev/null @@ -1,30 +0,0 @@ -Set Asymmetric Patterns. -Generalizable All Variables. -Set Implicit Arguments. -Set Universe Polymorphism. - -Record SpecializedCategory (obj : Type) := - { - Object :> _ := obj; - Morphism : obj -> obj -> Type; - - Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' - }. - -Arguments Compose {obj} [C s d d'] m1 m2 : rename. - -Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := -| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. - -Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d := - match m in @ReifiedMorphism objC C s d return Morphism C s d with - | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1) - (@ReifiedMorphismDenote _ _ _ _ m2) - end. - -Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d) -: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }. -refine match m with - | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _ - end; clear m. -Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ]. diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v deleted file mode 100644 index f73117a2ee..0000000000 --- a/test-suite/bugs/opened/3326.v +++ /dev/null @@ -1,18 +0,0 @@ -Class ORDER A := Order { - LEQ : A -> A -> bool; - leqRefl: forall x, true = LEQ x x -}. - -Section XXX. - -Variable A:Type. -Variable (O:ORDER A). -Definition aLeqRefl := @leqRefl _ O. - -Lemma OK : forall x, true = LEQ x x. - intros. - unfold LEQ. - destruct O. - clear. - Fail apply aLeqRefl. (* Toplevel input, characters 15-30: -Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v deleted file mode 100644 index 04a1223b6e..0000000000 --- a/test-suite/bugs/opened/3562.v +++ /dev/null @@ -1,2 +0,0 @@ -Theorem t: True. -Fail destruct 0 as x. diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v deleted file mode 100644 index 6faec0765e..0000000000 --- a/test-suite/bugs/opened/3657.v +++ /dev/null @@ -1,33 +0,0 @@ -(* Set Primitive Projections. *) -Class foo {A} {a : A} := { bar := a; baz : bar = bar }. -Arguments bar {_} _ {_}. -Instance: forall A a, @foo A a. -intros; constructor. -abstract reflexivity. -Defined. -Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat. -Proof. - Check (bar Set). - Check (bar (fun _ : Set => Set)). - Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *) - -Abort. - - -Module A. -Universes i j. -Constraint i < j. -Variable foo : Type@{i}. -Goal Type@{i}. - Fail let t := constr:(Type@{j}) in - change Type with t. -Abort. - -Goal Type@{j}. - Fail let t := constr:(Type@{i}) in - change Type with t. - let t := constr:(Type@{i}) in - change t. exact foo. -Defined. - -End A. diff --git a/test-suite/bugs/opened/3670.v b/test-suite/bugs/opened/3670.v deleted file mode 100644 index cf5e9b090b..0000000000 --- a/test-suite/bugs/opened/3670.v +++ /dev/null @@ -1,19 +0,0 @@ -Module Type FOO. - Parameters P Q : Type -> Type. -End FOO. - -Module Type BAR. - Declare Module Export foo : FOO. - Parameter f : forall A, P A -> Q A -> A. -End BAR. - -Module Type BAZ. - Declare Module Export foo : FOO. - Parameter g : forall A, P A -> Q A -> A. -End BAZ. - -Module BAR_FROM_BAZ (baz : BAZ) : BAR. - Import baz. - Module foo <: FOO := foo. - Definition f : forall A, P A -> Q A -> A := g. -End BAR_FROM_BAZ. diff --git a/test-suite/bugs/opened/3675.v b/test-suite/bugs/opened/3675.v deleted file mode 100644 index 93227ab852..0000000000 --- a/test-suite/bugs/opened/3675.v +++ /dev/null @@ -1,20 +0,0 @@ -Set Primitive Projections. -Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end. -Notation "p @ q" := (concat p q) (at level 20) : path_scope. -Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y. -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope path_scope. -Local Open Scope equiv_scope. -Generalizable Variables A B C f g. -Lemma isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} -: IsEquiv (compose g f). -Proof. - refine (Build_IsEquiv A C - (compose g f) - (compose f^-1 g^-1) _). - exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)). diff --git a/test-suite/bugs/opened/3788.v b/test-suite/bugs/opened/3788.v deleted file mode 100644 index 8e605a00f6..0000000000 --- a/test-suite/bugs/opened/3788.v +++ /dev/null @@ -1,5 +0,0 @@ -Set Implicit Arguments. -Global Set Primitive Projections. -Record Functor (C D : Type) := { object_of :> forall _ : C, D }. -Axiom path_functor_uncurried : forall C D (F G : Functor C D) (_ : sigT (fun HO : object_of F = object_of G => Set)), F = G. -Fail Lemma path_functor_uncurried_snd C D F G HO HM : (@path_functor_uncurried C D F G (existT _ HO HM)) = HM. diff --git a/test-suite/bugs/opened/3808.v b/test-suite/bugs/opened/3808.v deleted file mode 100644 index df40ca1910..0000000000 --- a/test-suite/bugs/opened/3808.v +++ /dev/null @@ -1,2 +0,0 @@ -Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) - := foo : Foo. -- cgit v1.2.3 From ea3909466eaaf86ff212c0a002e5df11e4a979f5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 May 2015 17:47:58 +0200 Subject: The Fail command does not catch uncaught exception anomalies anymore. --- lib/errors.ml | 9 +++++++++ lib/errors.mli | 4 ++++ toplevel/cerrors.ml | 9 ++++++++- toplevel/cerrors.mli | 2 +- toplevel/vernacentries.ml | 2 +- 5 files changed, 23 insertions(+), 3 deletions(-) diff --git a/lib/errors.ml b/lib/errors.ml index 999d99ee08..c60442654a 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -120,3 +120,12 @@ let noncritical = function | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true + +(** Check whether an exception is handled *) + +exception Bottom + +let handled e = + let bottom _ = raise Bottom in + try let _ = print_gen bottom !handle_stack e in true + with Bottom -> false diff --git a/lib/errors.mli b/lib/errors.mli index 5bd5724746..8320ce409f 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -88,3 +88,7 @@ val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... *) val noncritical : exn -> bool + +(** Check whether an exception is handled by some toplevel printer. The + [Anomaly] exception is never handled. *) +val handled : exn -> bool diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index a0892bed9a..accba3121b 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error ?(with_header=true) (exc, info) = +let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error with_header (exc, info) in + let () = + if not allow_uncaught && not (Errors.handled (fst e)) then + let (e, info) = e in + let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in + let err = Errors.make_anomaly msg in + Util.iraise (err, info) + in let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 100b3772cc..729686f32d 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9d5edc80a0..849b1d47d6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2106,7 +2106,7 @@ let with_fail b f = | e -> let e = Errors.push e in raise (HasFailed (Errors.iprint - (Cerrors.process_vernac_interp_error ~with_header:false e)))) + (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) () with e when Errors.noncritical e -> let (e, _) = Errors.push e in -- cgit v1.2.3 From 9dc2f675224b67ee3a35c2eb50d6a048a329a68a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 May 2015 19:10:52 +0200 Subject: Uncaught exception termination exits coqtop with the anomaly errno. --- toplevel/coqtop.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7ba0c55a15..826381028d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -618,7 +618,8 @@ let init arglist = if !batch_mode then mt () else str "Error during initialization:" ++ fnl () in - fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any)) + let is_anomaly e = Errors.is_anomaly e || not (Errors.handled e) in + fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any)) end; if !batch_mode then begin flush_all(); -- cgit v1.2.3 From d5c1f2133a80304ce8a1890e3568b14fafd8f283 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 May 2015 18:42:47 +0200 Subject: Test for bug #4116. --- test-suite/bugs/closed/4116.v | 383 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 383 insertions(+) create mode 100644 test-suite/bugs/closed/4116.v diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v new file mode 100644 index 0000000000..f808cb45e9 --- /dev/null +++ b/test-suite/bugs/closed/4116.v @@ -0,0 +1,383 @@ +(* File reduced by coq-bug-finder from original input, then from 13191 lines to 1315 lines, then from 1601 lines to 595 lines, then from 585 lines to 379 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 3 2015 3:50:31 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ac62cda8a4f488b94033b108c37556877232137a) *) + +Axiom admit : False. +Ltac admit := exfalso; exact admit. + +Global Set Primitive Projections. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +Definition relation (A : Type) := A -> A -> Type. + +Class Reflexive {A} (R : relation A) := + reflexivity : forall x : A, R x x. + +Class Symmetric {A} (R : relation A) := + symmetry : forall x y, R x y -> R y x. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope path_scope. +Open Scope fibration_scope. +Open Scope function_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Global Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) +: f == g + := fun x => match h with idpath => 1 end. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) + }. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) + }. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. +Notation "0" := (-1.+1) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" := + refine (let __transparent_assert_hypothesis := (_ : type) in _); + [ + | ( + let H := match goal with H := _ |- _ => constr:(H) end in + rename H into name) ]. + +Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x) +: transport P p u = transport idmap (ap P p) u + := match p with idpath => idpath end. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). + admit. + Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type + }. +Arguments trunctype_type {_} _. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hSet := 0-Type. + +Module Export Category. + Module Export Core. + Set Implicit Arguments. + + Delimit Scope morphism_scope with morphism. + Delimit Scope category_scope with category. + Delimit Scope object_scope with object. + + Record PreCategory := + Build_PreCategory' { + object :> Type; + morphism : object -> object -> Type; + + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1); + + associativity_sym : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + m3 o (m2 o m1) = (m3 o m2) o m1; + + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f; + + identity_identity : forall x, identity x o identity x = identity x + }. + Arguments identity {!C%category} / x%object : rename. + Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename. + + Definition Build_PreCategory + object morphism compose identity + associativity left_identity right_identity + := @Build_PreCategory' + object + morphism + compose + identity + associativity + (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _)) + left_identity + right_identity + (fun _ => left_identity _ _ _). + + Module Export CategoryCoreNotations. + Infix "o" := compose : morphism_scope. + Notation "1" := (identity _) : morphism_scope. + End CategoryCoreNotations. + + End Core. + +End Category. +Module Export Core. + Set Implicit Arguments. + + Delimit Scope functor_scope with functor. + + Local Open Scope morphism_scope. + + Section Functor. + Variables C D : PreCategory. + + Record Functor := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d); + composition_of : forall s d d' + (m1 : morphism C s d) (m2: morphism C d d'), + morphism_of _ _ (m2 o m1) + = (morphism_of _ _ m2) o (morphism_of _ _ m1); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. + End Functor. + Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +End Core. +Module Export Morphisms. + Set Implicit Arguments. + + Local Open Scope category_scope. + Local Open Scope morphism_scope. + + Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := + { + morphism_inverse : morphism C d s; + left_inverse : morphism_inverse o m = identity _; + right_inverse : m o morphism_inverse = identity _ + }. + + Class Isomorphic {C : PreCategory} s d := + { + morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic + }. + + Coercion morphism_isomorphic : Isomorphic >-> morphism. + + Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope. + + Section iso_equiv_relation. + Variable C : PreCategory. + + Global Instance isisomorphism_identity (x : C) : IsIsomorphism (identity x) + := {| morphism_inverse := identity x; + left_inverse := left_identity C x x (identity x); + right_inverse := right_identity C x x (identity x) |}. + + Global Instance isomorphic_refl : Reflexive (@Isomorphic C) + := fun x : C => {| morphism_isomorphic := identity x |}. + + Definition idtoiso (x y : C) (H : x = y) : Isomorphic x y + := match H in (_ = y0) return (x <~=~> y0) with + | 1%path => reflexivity x + end. + End iso_equiv_relation. + +End Morphisms. + +Notation IsCategory C := (forall s d : object C, IsEquiv (@idtoiso C s d)). + +Notation isotoid C s d := (@equiv_inv _ _ (@idtoiso C s d) _). + +Notation cat_of obj := + (@Build_PreCategory obj + (fun x y => x -> y) + (fun _ x => x) + (fun _ _ _ f g => f o g)%core + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ _ _ => idpath) + ). +Definition set_cat : PreCategory := cat_of hSet. +Set Implicit Arguments. + +Local Open Scope morphism_scope. + +Section Grothendieck. + Variable C : PreCategory. + Variable F : Functor C set_cat. + + Record Pair := + { + c : C; + x : F c + }. + + Local Notation Gmorphism s d := + { f : morphism C s.(c) d.(c) + | morphism_of F f s.(x) = d.(x) }. + + Definition identity_H s + := apD10 (identity_of F s.(c)) s.(x). + + Definition Gidentity s : Gmorphism s s. + Proof. + exists 1. + apply identity_H. + Defined. + + Definition Gcategory : PreCategory. + Proof. + refine (@Build_PreCategory + Pair + (fun s d => Gmorphism s d) + Gidentity + _ + _ + _ + _); admit. + Defined. +End Grothendieck. + +Lemma isotoid_1 {C} `{IsCategory C} {x : C} {H : IsIsomorphism (identity x)} +: isotoid C x x {| morphism_isomorphic := (identity x) ; isisomorphism_isomorphic := H |} + = idpath. + admit. +Defined. +Generalizable All Variables. + +Section Grothendieck2. + Context `{IsCategory C}. + Variable F : Functor C set_cat. + + Instance iscategory_grothendieck_toset : IsCategory (Gcategory F). + Proof. + intros s d. + refine (isequiv_adjointify _ _ _ _). + { + intro m. + transparent assert (H' : (s.(c) = d.(c))). + { + apply (idtoiso C (x := s.(c)) (y := d.(c)))^-1%function. + exists (m : morphism _ _ _).1. + admit. + + } + { + transitivity {| x := transport (fun x => F x) H' s.(x) |}. + admit. + + { + change d with {| c := d.(c) ; x := d.(x) |}; simpl. + apply ap. + subst H'. + simpl. + refine (transport_idmap_ap _ (fun x => F x : Type) _ _ _ _ @ _ @ (m : morphism _ _ _).2). + change (fun x => F x : Type) with (trunctype_type o object_of F)%function. + admit. + } + } + } + { + admit. + } + + { + intro x. + hnf in s, d. + destruct x. + simpl. + erewrite @isotoid_1. -- cgit v1.2.3 From 5a52a74592496353d562d9f3e958fb59ab585531 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 May 2015 19:36:31 +0200 Subject: Adding an extensible global state to evarmaps. Evars already had their own extensible state, but adding it globally allows to write out extensible state-passing code in e.g. plugins. The additional data is hopefully transparently preserved by the code out there. Trespassers ought to be prosecuted. --- pretyping/evd.ml | 9 +++++++++ pretyping/evd.mli | 13 +++++++++++++ 2 files changed, 22 insertions(+) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index f414d71dc1..18e668d288 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -564,6 +564,7 @@ type evar_map = { name) of the evar which will be instantiated with a term containing [e]. *) + extras : Store.t; } (*** Lifting primitive from Evar.Map. ***) @@ -745,6 +746,7 @@ let empty = { evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; + extras = Store.empty; } let from_env ?ctx e = @@ -1320,6 +1322,7 @@ let set_metas evd metas = { evar_names = evd.evar_names; future_goals = evd.future_goals; principal_future_goal = evd.principal_future_goal; + extras = Store.empty; } let meta_list evd = metamap_to_list evd.metas @@ -1468,6 +1471,12 @@ let dependent_evar_ident ev evd = | (_,Evar_kinds.VarInstance id) -> id | _ -> anomaly (str "Not an evar resulting of a dependent binding") +(**********************************************************) +(* Extra data *) + +let get_extra_data evd = evd.extras +let set_extra_data extras evd = { evd with extras } + (*******************************************************************) type pending = (* before: *) evar_map * (* after: *) evar_map diff --git a/pretyping/evd.mli b/pretyping/evd.mli index eca6d60ad5..15ce979d0c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -310,6 +310,19 @@ val add_universe_constraints : evar_map -> Universes.universe_constraints -> eva @raises UniversesDiffer in case a first-order unification fails. @raises UniverseInconsistency *) + +(** {5 Extra data} + + Evar maps can contain arbitrary data, allowing to use an extensible state. + As evar maps are theoretically used in a strict state-passing style, such + additional data should be passed along transparently. Some old and bug-prone + code tends to drop them nonetheless, so you should keep cautious. + +*) + +val get_extra_data : evar_map -> Store.t +val set_extra_data : Store.t -> evar_map -> evar_map + (** {5 Enriching with evar maps} *) type 'a sigma = { -- cgit v1.2.3 From 69941d4e195650bf59285b897c14d6287defea0f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 20 May 2015 14:36:41 +0200 Subject: Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files found in the file system have the expected lowercase/uppercase spelling) --- lib/envars.ml | 19 ++++++++++++++++--- lib/system.ml | 7 +++---- lib/system.mli | 2 ++ 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index b0eed8386b..ac0b6f722e 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,12 +39,25 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) + (* Duplicated from system.ml to minimize dependencies *) +let file_exists_respecting_case f = + if Coq_config.arch = "Darwin" then + (* ensure that the file exists with expected case on the + case-insensitive but case-preserving default MacOS file system *) + let rec aux f = + let bf = Filename.basename f in + let df = Filename.dirname f in + String.equal df "." || String.equal df "/" || + aux df && Array.exists (String.equal bf) (Sys.readdir df) + in aux f + else Sys.file_exists f + let rec which l f = match l with | [] -> raise Not_found | p :: tl -> - if Sys.file_exists (p / f) then + if file_exists_respecting_case (p / f) then p else which tl f @@ -102,7 +115,7 @@ let _ = If the check fails, then [oth ()] is evaluated. *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in - if Sys.file_exists (path / file) then path else oth () + if file_exists_respecting_case (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in @@ -134,7 +147,7 @@ let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = let paths = path_to_list path in - let valid_paths = List.filter Sys.file_exists paths in + let valid_paths = List.filter file_exists_respecting_case paths in List.rev valid_paths in make_search_path coqpath diff --git a/lib/system.ml b/lib/system.ml index 6364035e16..1a67120b60 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,12 +53,11 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l -let file_really_exists f = +let file_exists_respecting_case f = if Coq_config.arch = "Darwin" then (* ensure that the file exists with expected case on the case-insensitive but case-preserving default MacOS file system *) let rec aux f = - Printf.eprintf ".%!"; let bf = Filename.basename f in let df = Filename.dirname f in String.equal df "." || String.equal df "/" || @@ -90,7 +89,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if Sys.file_exists f then [lpe,f] else [])) + if file_exists_respecting_case f then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -106,7 +105,7 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - if Sys.file_exists filename then + if file_exists_respecting_case filename then let root = Filename.dirname filename in root, filename else diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..051e92f166 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -29,6 +29,8 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val file_exists_respecting_case : string -> bool + (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] -- cgit v1.2.3 From 8241460f5a729b577b0d7da544fe8f8fcda18d14 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 20 May 2015 14:47:24 +0200 Subject: Answering report #4241 (formatting of boxes not behaving regularly when printing width extend). --- lib/pp_control.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 0d224c0351..7fe4e0f52d 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -20,7 +20,7 @@ let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; - ellipsis = ".." } + ellipsis = "..." } (* A deeper pretty-printer to print proof scripts *) @@ -84,5 +84,8 @@ let set_margin v = let v = match v with None -> default_margin | Some v -> v in Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v - + Format.pp_set_margin !deep_ft v; + let m = 64 * v / 100 in (* Heuristic, based on usage *) + Format.pp_set_max_indent Format.str_formatter m; + Format.pp_set_max_indent !std_ft m; + Format.pp_set_max_indent !deep_ft m -- cgit v1.2.3 From 2eb7d2e20a2fc58ae91a5110f26e2f9a3699db46 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 21 May 2015 18:14:56 +0200 Subject: Changing the heuristic fixing bug #4241. Fixed #4241 correlates Printing Width and max_indent, this patch changes the correlation to the following one: max_indent = max ((wdth*80)/100) (wdth-30) i.e. the right column defined by max_indent is 20% of the global width, but capped to 30 characters. --- lib/pp_control.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 7fe4e0f52d..969c1550ec 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -85,7 +85,9 @@ let set_margin v = Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; Format.pp_set_margin !deep_ft v; - let m = 64 * v / 100 in (* Heuristic, based on usage *) + (* Heuristic, based on usage: the column on the right of max_indent + column is 20% of width, capped to 30 characters *) + let m = max (64 * v / 100) (v-30) in Format.pp_set_max_indent Format.str_formatter m; Format.pp_set_max_indent !std_ft m; Format.pp_set_max_indent !deep_ft m -- cgit v1.2.3 From e7043eec55085f4101bfb126d8829de6f6086c5a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 22 May 2015 08:50:36 +0200 Subject: Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X. Thanks to Vadim Zaliva for testing. --- lib/system.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/system.ml b/lib/system.ml index 1a67120b60..27e21204cc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -60,8 +60,8 @@ let file_exists_respecting_case f = let rec aux f = let bf = Filename.basename f in let df = Filename.dirname f in - String.equal df "." || String.equal df "/" || - aux df && Array.exists (String.equal bf) (Sys.readdir df) + (String.equal df "." || String.equal df "/" || aux df) + && Array.exists (String.equal bf) (Sys.readdir df) in aux f else Sys.file_exists f -- cgit v1.2.3 From c4ffe2b6725a3f8f60763228b77668aa3444f79c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 25 May 2015 14:15:53 +0200 Subject: CoqIDE columns in error and job panels can be sorted. This grants wish #4194. --- ide/session.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index 12b7796633..cfcc592ef1 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -239,7 +239,7 @@ let find_int_col s l = let find_string_col s l = match List.assoc s l with `StringC c -> c | _ -> assert false -let make_table_widget cd cb = +let make_table_widget ?sort cd cb = let frame = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in let columns, store = let cols = new GTree.column_list in @@ -253,6 +253,7 @@ let make_table_widget cd cb = ~rules_hint:true ~headers_visible:false ~model:store ~packing:frame#add () in let () = data#set_headers_visible true in + let () = data#set_headers_clickable true in let refresh () = let clr = Tags.color_of_string current.background_color in data#misc#modify_base [`NORMAL, `COLOR clr] @@ -268,15 +269,27 @@ let make_table_widget cd cb = c#set_sizing `AUTOSIZE; c) columns cd in + let make_sorting i (_, c) = + let sort (store : GTree.model) it1 it2 = match c with + | `IntC c -> + Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + | `StringC c -> + Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + in + store#set_sort_func i sort + in + List.iteri make_sorting columns; + List.iteri (fun i c -> c#set_sort_column_id i) cols; List.iter (fun c -> ignore(data#append_column c)) cols; ignore( data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc) ); + let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in frame, (fun f -> f columns store), refresh let create_errpage (script : Wg_ScriptView.script_view) : errpage = let table, access, refresh = - make_table_widget + make_table_widget ~sort:(0, `ASCENDING) [`Int,"Line",true; `String,"Error message",true] (fun columns store tp vc -> let row = store#get_iter tp in @@ -311,7 +324,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = let create_jobpage coqtop coqops : jobpage = let table, access, refresh = - make_table_widget + make_table_widget ~sort:(0, `ASCENDING) [`String,"Worker",true; `String,"Job name",true] (fun columns store tp vc -> let row = store#get_iter tp in -- cgit v1.2.3 From ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 26 May 2015 15:04:21 +0200 Subject: Jump to error line in CoqIDE grabs focus of the textview. --- ide/session.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/ide/session.ml b/ide/session.ml index cfcc592ef1..fd8f806909 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -296,6 +296,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = let lno = store#get ~row ~column:(find_int_col "Line" columns) in let where = script#buffer#get_iter (`LINE (lno-1)) in script#buffer#place_cursor ~where; + script#misc#grab_focus (); ignore (script#scroll_to_iter ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in let tip = GMisc.label ~text:"Double click to jump to error line" () in -- cgit v1.2.3 From 866c41b9720413e00194ba7addb9c4277e114890 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 27 May 2015 11:43:11 +0200 Subject: Fix bug #4159 Some asynchronous constraints between initial universes and the ones at the end of a proof were forgotten. Also add a message to print universes indicating if all the constraints are processed already or not. --- interp/modintern.ml | 2 +- kernel/safe_typing.ml | 2 ++ kernel/safe_typing.mli | 1 + library/global.ml | 5 +++++ library/global.mli | 1 + library/universes.ml | 2 +- pretyping/evd.ml | 16 +++++++++++++++- pretyping/evd.mli | 2 +- proofs/proof_global.ml | 4 ++-- stm/lemmas.ml | 2 +- tactics/extratactics.ml4 | 2 +- toplevel/command.ml | 4 ++-- toplevel/vernacentries.ml | 12 ++++++++---- 13 files changed, 41 insertions(+), 14 deletions(-) diff --git a/interp/modintern.ml b/interp/modintern.ml index bf0b2f9800..35e731137f 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,7 +62,7 @@ let transl_with_decl env = function WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> let c, ectx = interp_constr env (Evd.from_env env) c in - let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in + let ctx = Evd.evar_context_universe_context ectx in WithDef (fqid,(c,ctx)) let loc_of_module = function diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d6bd754783..d9adca0c91 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -246,6 +246,8 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e = else add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst +let is_joined_environment e = List.is_empty e.future_cst + (** {6 Various checks } *) let exists_modlabel l senv = Label.Set.mem l senv.modlabels diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index abd5cd7ae1..a57fb108c4 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -51,6 +51,7 @@ val is_curmod_library : safe_environment -> bool val join_safe_environment : ?except:Future.UUIDSet.t -> safe_environment -> safe_environment +val is_joined_environment : safe_environment -> bool (** {6 Enriching a safe environment } *) (** Insertion of local declarations (Local or Variables) *) diff --git a/library/global.ml b/library/global.ml index 875097e48c..49fa2ef28f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -19,6 +19,7 @@ module GlobalSafeEnv : sig val safe_env : unit -> Safe_typing.safe_environment val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit + val is_joined_environment : unit -> bool end = struct @@ -27,6 +28,9 @@ let global_env = ref Safe_typing.empty_environment let join_safe_environment ?except () = global_env := Safe_typing.join_safe_environment ?except !global_env +let is_joined_environment () = + Safe_typing.is_joined_environment !global_env + let () = Summary.declare_summary global_env_summary_name { Summary.freeze_function = (function @@ -50,6 +54,7 @@ end let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () +let is_joined_environment = GlobalSafeEnv.is_joined_environment let env () = Safe_typing.env_of_safe_env (safe_env ()) diff --git a/library/global.mli b/library/global.mli index 62d7ea3210..248e1f86dd 100644 --- a/library/global.mli +++ b/library/global.mli @@ -112,6 +112,7 @@ val import : val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit +val is_joined_environment : unit -> bool val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool diff --git a/library/universes.ml b/library/universes.ml index 3a8ee26254..3a7a769075 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -845,7 +845,7 @@ let normalize_context_set ctx us algs = Constraint.add (canon, Univ.Eq, g) cst) global cstrs in - let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in + let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) (ctx, LMap.empty, Constraint.empty) partition diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 18e668d288..fe96aa347d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -330,9 +330,23 @@ let union_evar_universe_context ctx ctx' = type 'a in_evar_universe_context = 'a * evar_universe_context -let evar_universe_context_set ctx = ctx.uctx_local +let evar_universe_context_set diff ctx = + let initctx = ctx.uctx_local in + let cstrs = + Univ.LSet.fold + (fun l cstrs -> + try + match Univ.LMap.find l ctx.uctx_univ_variables with + | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs + | None -> cstrs + with Not_found -> cstrs) + (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty + in + Univ.ContextSet.add_constraints cstrs initctx + let evar_universe_context_constraints ctx = snd ctx.uctx_local let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local + let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } let evar_universe_context_subst ctx = ctx.uctx_univ_variables diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 15ce979d0c..f2d8a83350 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -475,7 +475,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * evar_universe_context -val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set +val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set val evar_universe_context_constraints : evar_universe_context -> Univ.constraints val evar_context_universe_context : evar_universe_context -> Univ.universe_context val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5bff3c8131..8be96285f9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -292,7 +292,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let body = c and typ = nf t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - let ctx = Evd.evar_universe_context_set universes in + let ctx = Evd.evar_universe_context_set Univ.UContext.empty universes in if keep_body_ucst_sepatate then (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of @@ -317,7 +317,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context universes in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt, Evd.evar_universe_context_set (Future.force univs)), eff) + (pt, Evd.evar_universe_context_set initunivs (Future.force univs)), eff) in let entries = Future.map2 (fun p (_, t) -> diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6cece32e0a..5eebd0d9d3 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -436,7 +436,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.evar_universe_context_set ctx in + let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 177be2c205..e4240cb5cc 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -268,7 +268,7 @@ let add_rewrite_hint bases ort t lcsr = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = if poly then - Evd.evar_universe_context_set ctx + Evd.evar_universe_context_set Univ.UContext.empty ctx else let cstrs = Evd.evar_universe_context_constraints ctx in (Global.add_constraints cstrs; Univ.ContextSet.empty) diff --git a/toplevel/command.ml b/toplevel/command.ml index 7cf0477f9f..1b396d57ba 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1064,7 +1064,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let ctx = Evd.evar_universe_context_set ctx in + let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in let ctx = Universes.restrict_universe_context ctx vars in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let ctx = Univ.ContextSet.to_context ctx in @@ -1097,7 +1097,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - let ctx = Evd.evar_universe_context_set ctx in + let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in let ctx = Univ.ContextSet.to_context ctx in ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) fixnames fixdecls fixtypes fiximps); diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 849b1d47d6..61ebc9bbe6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1563,7 +1563,7 @@ let vernac_global_check c = let sigma = Evd.from_env env in let c,ctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (Evd.evar_universe_context_set ctx) in + let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in @@ -1628,9 +1628,13 @@ let vernac_print = function msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) | PrintUniverses (b, None) -> - let univ = Global.universes () in - let univ = if b then Univ.sort_universes univ else univ in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ) + let univ = Global.universes () in + let univ = if b then Univ.sort_universes univ else univ in + let pr_remaining = + if Global.is_joined_environment () then mt () + else str"There may remain asynchronous universe constraints" + in + msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) -- cgit v1.2.3 From c6714db203f60413523ebeaac86242a6e4cc05e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 May 2015 11:43:10 +0200 Subject: Test for 4159 --- test-suite/ide/univ.fake | 14 ++++++++++++++ tools/fake_ide.ml | 4 ++++ 2 files changed, 18 insertions(+) create mode 100644 test-suite/ide/univ.fake diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake new file mode 100644 index 0000000000..90af8785ad --- /dev/null +++ b/test-suite/ide/univ.fake @@ -0,0 +1,14 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + interp error while fixing. +# the error should note make the GUI unfocus the currently focused proof. + +# first proof +ADD { Set Implicit Arguments. } +ADD { Record dynamic := dyn { dyn_type : Type; dyn_value : dyn_type }. } +ADD { Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2), dyn x1 = dyn x2 -> A1 = A2. } +ADD { Proof. } +ADD { now intros A1 A2 x1 x2 [= e1 e2]. } +ADD { Qed. } +JOIN diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index c2b126687f..d7a292f4cf 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -257,6 +257,9 @@ let eval_print l coq = | [ Tok(_,"WAIT") ] -> let phrase = "Stm Wait." in eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"JOIN") ] -> + let phrase = "Stm JoinDocument." in + eval_call (query (phrase,tip_id())) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" @@ -273,6 +276,7 @@ let grammar = ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] ; Seq [Item (eat_rex "WAIT")] + ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] ; Seq [Item (eat_rex "FAILGOALS")] ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] -- cgit v1.2.3 From 5c437ab917bd24de66986e95dcf58c3f31e17a34 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 May 2015 11:50:11 +0200 Subject: STM: preserve branch name on edit (Close: #4245, #4246) --- stm/stm.ml | 46 +++++++++++++++++++++++++++------------------- test-suite/ide/reopen.fake | 21 +++++++++++++++++++++ 2 files changed, 48 insertions(+), 19 deletions(-) create mode 100644 test-suite/ide/reopen.fake diff --git a/stm/stm.ml b/stm/stm.ml index 97903e721b..fa3ffc7c6e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -131,7 +131,8 @@ type cancel_switch = bool ref type branch_type = [ `Master | `Proof of proof_mode * depth - | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type ] + | `Edit of + proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] type cmd_t = { ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) cast : ast; @@ -449,7 +450,7 @@ end = struct (* {{{ *) if List.mem edit_branch (Vcs_.branches !vcs) then begin checkout edit_branch; match get_branch edit_branch with - | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode + | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode | _ -> assert false end else let pl = proof_nesting () in @@ -1788,7 +1789,7 @@ let known_state ?(redefine_qed=false) ~cache id = VCS.create_cluster nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false - | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) -> + | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then msg_error(strbrk("The command closing the proof changed. " @@ -1922,7 +1923,7 @@ let finish ?(print_goals=false) () = VCS.print (); (* Some commands may by side effect change the proof mode *) match VCS.get_branch head with - | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode + | { VCS.kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode | _ -> () @@ -1990,7 +1991,7 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.delete_branch brname; if keep <> VtDrop then VCS.propagate_sideff None; `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id, _) } -> + | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = match VCS.visit qed_id with | { step = `Qed ({ fproof }, _) } -> fproof @@ -2144,9 +2145,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | { VCS.root; kind = `Proof(_,d); pos } -> VCS.delete_branch bn; VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q,k); pos } -> + | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } -> VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q,k))) + VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob))) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); @@ -2298,20 +2299,23 @@ let edit_at id = | { step = `Fork _ } -> tip | { step = `Sideff (`Ast(_,id)|`Id id) } -> id | { next } -> master_for_br root next in - let reopen_branch start at_id mode qed_id tip = + let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = (* Hum, this should be the real start_id in the clusted and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep | _ -> anomaly (str "Cluster not ending with Qed") in VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id, keep)); + VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); VCS.delete_cluster_of id; cancel_switch := true; Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in - let backto id = + let no_edit = function + | `Edit (pm, _,_,_,_) -> `Proof(pm,1) + | x -> x in + let backto id bn = List.iter VCS.delete_branch (VCS.branches ()); let ancestors = VCS.reachable id in let { mine = brname, brinfo; others } = Backtrack.branches_of id in @@ -2321,7 +2325,10 @@ let edit_at id = VCS.branch ~root ~pos name k) others; VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); - VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind; + VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos + (Option.default brname bn) + (no_edit brinfo.VCS.kind); + VCS.print (); VCS.delete_cluster_of id; VCS.gc (); Reach.known_state ~cache:(interactive ()) id; @@ -2332,20 +2339,21 @@ let edit_at id = let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in let branch_info = match snd (VCS.get_info id).vcs_backup with - | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m + | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) + | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) | _ -> None in match focused, VCS.cluster_of id, branch_info with | _, Some _, None -> assert false - | false, Some (qed_id,start), Some mode -> + | false, Some (qed_id,start), Some(mode,bn) -> let tip = VCS.cur_tip () in if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch - then reopen_branch start id mode qed_id tip - else backto id - | true, Some (qed_id,_), Some mode -> + then reopen_branch start id mode qed_id tip bn + else backto id (Some bn) + | true, Some (qed_id,_), Some(mode,bn) -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin - backto id + backto id (Some bn) end else begin anomaly(str"Cannot leave an `Edit branch open") end @@ -2356,11 +2364,11 @@ let edit_at id = VCS.checkout_shallowest_proof_branch (); `NewTip end else if is_ancestor_of_cur_branch id then begin - backto id + backto id None end else begin anomaly(str"Cannot leave an `Edit branch open") end - | false, None, _ -> backto id + | false, None, _ -> backto id None in VCS.print (); rc diff --git a/test-suite/ide/reopen.fake b/test-suite/ide/reopen.fake new file mode 100644 index 0000000000..8166d0137e --- /dev/null +++ b/test-suite/ide/reopen.fake @@ -0,0 +1,21 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + interp error while fixing. +# the error should note make the GUI unfocus the currently focused proof. + +# first proof +ADD { Lemma a : True. } +ADD here { Proof using. } +ADD { fail. } +ADD { trivial. } # first error +ADD { Qed. } +WAIT +EDIT_AT here +# Fixing the proof +ADD fix { trivial. } +ADD { Qed. } +WAIT +EDIT_AT fix +ADD { Qed. } +JOIN -- cgit v1.2.3 From 83188dacc43df02245d13810d08cc63b7a5633ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 May 2015 14:13:12 +0200 Subject: Fixup for 866c41b --- pretyping/evd.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fe96aa347d..60b1da7049 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -339,7 +339,7 @@ let evar_universe_context_set diff ctx = match Univ.LMap.find l ctx.uctx_univ_variables with | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs | None -> cstrs - with Not_found -> cstrs) + with Not_found | Option.IsNone -> cstrs) (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty in Univ.ContextSet.add_constraints cstrs initctx -- cgit v1.2.3 From 5e873be3cdbdff6b9bad782ce88d2206b9053e14 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 May 2015 13:30:06 +0200 Subject: coqide: don't require ocaml >= 4 --- ide/session.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ide/session.ml b/ide/session.ml index fd8f806909..a795f6331a 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -278,8 +278,8 @@ let make_table_widget ?sort cd cb = in store#set_sort_func i sort in - List.iteri make_sorting columns; - List.iteri (fun i c -> c#set_sort_column_id i) cols; + CList.iteri make_sorting columns; + CList.iteri (fun i c -> c#set_sort_column_id i) cols; List.iter (fun c -> ignore(data#append_column c)) cols; ignore( data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc) -- cgit v1.2.3 From c47916933025a4853ed0b397d7476b844bb894a4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 May 2015 14:44:10 +0200 Subject: STM/Univ: save initial univs (the ones in the statement) in Proof.proof This makes the treatment of universe constraints/normalization more understandable in the Sync/Async case: - if one has to keep the constraints of the body and the type of a lemma separate, then equations coming from the body are kept (see: 866c41 ) - if they can be merge then the equations (substituted on both the body and type) can be removed (one of the sides occurs nowhere) The result is that, semantically, the constraints of a lemma do not depend on weather it was produced asynchronously (v->vio->vo, or in a CoqIDE session) or synchronously (v->vo). Still the internal representation of the constraints changes to accommodate an optimization (to reduce the size of the constraint set): - in the synchronous case (some) equations are substituted (in both the type and body), hence they can be completely dropped from the constraint set - in the asynchronous case (some) equations are substituted in the body only (the type is fixed once and for all before the equations are discovered/generated), hence these equations are necessary to relate the type and the (optimized) body and are hence kept in the constraint set --- proofs/proof.ml | 11 +++++++++-- proofs/proof.mli | 1 + proofs/proof_global.ml | 33 +++++++++++++++------------------ 3 files changed, 25 insertions(+), 20 deletions(-) diff --git a/proofs/proof.ml b/proofs/proof.ml index 828f9fa717..a7077d9110 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -111,6 +111,8 @@ type proof = { shelf : Goal.goal list; (* List of goals that have been given up *) given_up : Goal.goal list; + (* The initial universe context (for the statement) *) + initial_euctx : Evd.evar_universe_context } (*** General proof functions ***) @@ -271,7 +273,9 @@ let start sigma goals = entry; focus_stack = [] ; shelf = [] ; - given_up = [] } in + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr let dependent_start goals = let entry, proofview = Proofview.dependent_init goals in @@ -280,7 +284,9 @@ let dependent_start goals = entry; focus_stack = [] ; shelf = [] ; - given_up = [] } in + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -311,6 +317,7 @@ let return p = Proofview.return p.proofview let initial_goals p = Proofview.initial_goals p.entry +let initial_euctx p = p.initial_euctx let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in diff --git a/proofs/proof.mli b/proofs/proof.mli index 2b85ec8724..a2e10d8133 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -69,6 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof val dependent_start : Proofview.telescope -> proof val initial_goals : proof -> (Term.constr * Term.types) list +val initial_euctx : proof -> Evd.evar_universe_context (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8be96285f9..3e2c813e38 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -273,12 +273,10 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in + let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in - let universes = - if poly || now then Future.force univs - else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) - in - (* Because of dependent subgoals at the begining of proofs, we could + let universes = if poly || now then Future.force univs else initial_euctx in + (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = @@ -289,11 +287,12 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = if poly || now then let make_body t (c, eff) = let open Universes in - let body = c and typ = nf t in + let body = c and typ = nf t in let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in - let ctx = Evd.evar_universe_context_set Univ.UContext.empty universes in + let used_univs_typ = Universes.universes_of_constr typ in if keep_body_ucst_sepatate then + let initunivs = Evd.evar_context_universe_context initial_euctx in + let ctx = Evd.evar_universe_context_set initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -302,6 +301,8 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let univs_typ = Univ.ContextSet.to_context ctx_typ in (univs_typ, typ), ((body, ctx_body), eff) else + let initunivs = Univ.UContext.empty in + let ctx = Evd.evar_universe_context_set initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -310,14 +311,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let univs = Univ.ContextSet.to_context ctx 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 ~pure:true p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context universes in - Future.from_val (initunivs, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> - (pt, Evd.evar_universe_context_set initunivs (Future.force univs)), eff) + let initunivs = Evd.evar_context_universe_context initial_euctx in + Future.from_val (initunivs, nf t), + Future.chain ~pure:true p (fun (pt,eff) -> + (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -370,10 +370,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = - if poly || !Flags.compilation_mode = Flags.BuildVo - then Evd.nf_constraints evd - else evd in + let evd = Evd.nf_constraints evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) -- cgit v1.2.3 From f63c0cdd3c7da642e505569e83199784bbfdc367 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 May 2015 19:00:07 +0200 Subject: make Unset Silent work in coqc Trying to untangle the flags: coqc -verbose coqtop -compile-verbose are used just to print the commands run; -quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag. Flags.verbose controls many prints that are expected to be made in interactive mode. E.g. "Proof" or "tac" prints goals if such flag is true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc mode. It is still messy, but the confusion between -verbose and Flags.verbose has gone (I must have identified the two things with my initial STM patch) --- toplevel/vernac.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5418c60e94..a06702e0d6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -215,7 +215,7 @@ let display_cmd_header loc com = str " [" ++ str cmd ++ str "] "); Pp.flush_all () -let rec vernac_com verbosely checknav (loc,com) = +let rec vernac_com checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in @@ -241,7 +241,7 @@ let rec vernac_com verbosely checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp verbosely (loc,v) + | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; @@ -268,7 +268,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in - vernac_com verbosely checknav loc_ast; + vernac_com checknav loc_ast; pp_flush () done with any -> (* whatever the exception *) @@ -292,14 +292,14 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast +let eval_expr loc_ast = vernac_com checknav loc_ast (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try - read_vernac_file verb file; + Flags.silently (read_vernac_file verb) file; if !Flags.beautify_file then close_out !chan_beautify; with any -> let (e, info) = Errors.push any in -- cgit v1.2.3 From e47c30bf431f3c8160b41384eedb538ba16578d0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 May 2015 15:41:15 +0200 Subject: Flag -test-mode intended to be used for ad-hoc prints in test-suite Of course there is an exception to the previous commit. Fail used to print even if silenced but loading a vernac file. This behavior is useful only in tests, hence this flag. --- lib/flags.ml | 2 ++ lib/flags.mli | 2 ++ test-suite/Makefile | 2 +- toplevel/coqtop.ml | 1 + toplevel/vernacentries.ml | 2 +- 5 files changed, 7 insertions(+), 2 deletions(-) diff --git a/lib/flags.ml b/lib/flags.ml index 313da0c5bd..009caa9dee 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -48,6 +48,8 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let test_mode = ref false + type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff type cache = Force diff --git a/lib/flags.mli b/lib/flags.mli index 1f68a88f3a..544e2a72ae 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -15,6 +15,8 @@ val batch_mode : bool ref type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref +val test_mode : bool ref + type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref type cache = Force diff --git a/test-suite/Makefile b/test-suite/Makefile index cffbe48196..476d850ac9 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -30,7 +30,7 @@ BIN := ../bin/ LIB := .. -coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite +coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 826381028d..81e04525c8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -499,6 +499,7 @@ let parse_args arglist = |"-async-proofs-never-reopen-branch" -> Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () + |"-test-mode" -> test_mode := true |"-beautify" -> make_beautify true |"-boot" -> boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 61ebc9bbe6..188d2d098f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2118,7 +2118,7 @@ let with_fail b f = | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed!") | HasFailed msg -> - if is_verbose () || !Flags.ide_slave then msg_info + if is_verbose () || !test_mode || !ide_slave then msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end -- cgit v1.2.3 From 43aa642ad4f2d30029c1c1f272ba162b6801a40b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 May 2015 15:41:51 +0200 Subject: coqtop: reset the current file name after a load-vernac-source --- toplevel/vernac.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a06702e0d6..7d84ecf6ca 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -277,6 +277,7 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> + cur_file := None; if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None | _ -> raise_with_file fname (disable_drop e, info) -- cgit v1.2.3