diff options
53 files changed, 705 insertions, 228 deletions
@@ -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. diff --git a/engine/evd.ml b/engine/evd.ml index f414d71dc..60b1da704 100644 --- a/engine/evd.ml +++ b/engine/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 | Option.IsNone -> 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 @@ -564,6 +578,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 +760,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 +1336,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 +1485,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/engine/evd.mli b/engine/evd.mli index eca6d60ad..f2d8a8335 100644 --- a/engine/evd.mli +++ b/engine/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 = { @@ -462,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/ide/session.ml b/ide/session.ml index 12b779663..a795f6331 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,21 +269,34 @@ 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 + 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) ); + 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 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 @@ -311,7 +325,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 diff --git a/interp/modintern.ml b/interp/modintern.ml index bf0b2f980..35e731137 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/nativelib.ml b/kernel/nativelib.ml index 605c1225c..29b6bf6de 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 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d6bd75478..d9adca0c9 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 abd5cd7ae..a57fb108c 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/lib/envars.ml b/lib/envars.ml index b0eed8386..ac0b6f722 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/errors.ml b/lib/errors.ml index 999d99ee0..c60442654 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 5bd572474..8320ce409 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/lib/flags.ml b/lib/flags.ml index 313da0c5b..009caa9de 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 1f68a88f3..544e2a72a 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/lib/pp_control.ml b/lib/pp_control.ml index 0d224c035..969c1550e 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,10 @@ 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; + (* 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 diff --git a/lib/system.ml b/lib/system.ml index e4a60eccb..26bf78010 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -94,6 +94,18 @@ let all_subdirs ~unix_path:root = else msg_warning (str ("Cannot open " ^ root)); List.rev !l +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 search paths test = match paths with | [] -> [] @@ -118,7 +130,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 -> @@ -134,7 +146,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 6ed450326..eb29b6970 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -59,6 +59,8 @@ val where_in_path_rex : 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] diff --git a/library/global.ml b/library/global.ml index 875097e48..49fa2ef28 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 62d7ea321..248e1f86d 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 3a8ee2625..3a7a76907 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/coercion.ml b/pretyping/coercion.ml index f5135f5c6..6765ca130 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 diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 18883df24..aaa49f116 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/proofs/proof.ml b/proofs/proof.ml index 828f9fa71..a7077d911 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 2b85ec872..a2e10d813 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 5bff3c813..3e2c813e3 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 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 (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... *) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6cece32e0..5eebd0d9d 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/stm/stm.ml b/stm/stm.ml index 97903e721..fa3ffc7c6 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/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 177be2c20..e4240cb5c 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/tactics/tacenv.ml b/tactics/tacenv.ml index 492b51f1a..c1e4d72e3 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -77,34 +77,48 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = 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 7ee591cca..47d9efda5 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 5cc4c835b..d4c67b90f 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" diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2791d7c48..402a9e88a 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 diff --git a/test-suite/Makefile b/test-suite/Makefile index cffbe4819..476d850ac 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/test-suite/bugs/opened/3461.v b/test-suite/bugs/closed/3461.v index 1b625e6a1..1b625e6a1 100644 --- a/test-suite/bugs/opened/3461.v +++ b/test-suite/bugs/closed/3461.v diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v new file mode 100644 index 000000000..f808cb45e --- /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. diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v deleted file mode 100644 index b7f40b4ad..000000000 --- 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 f73117a2e..000000000 --- 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 04a1223b6..000000000 --- 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 6faec0765..000000000 --- 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 cf5e9b090..000000000 --- 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 93227ab85..000000000 --- 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 8e605a00f..000000000 --- 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 df40ca191..000000000 --- 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. diff --git a/test-suite/ide/reopen.fake b/test-suite/ide/reopen.fake new file mode 100644 index 000000000..8166d0137 --- /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 diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake new file mode 100644 index 000000000..90af8785a --- /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/coqc.ml b/tools/coqc.ml index aed229abc..5710b97f2 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 diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index c2b126687..d7a292f4c 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 ] diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index a0892bed9..accba3121 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 100b3772c..729686f32 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/command.ml b/toplevel/command.ml index 7cf0477f9..1b396d57b 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/coqtop.ml b/toplevel/coqtop.ml index 56b544292..934e73aae 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 @@ -496,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 @@ -615,7 +619,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(); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 50fb019f4..36ecc9fa5 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\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5418c60e9..7d84ecf6c 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 *) @@ -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) @@ -292,14 +293,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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9d5edc80a..188d2d098 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 ()) @@ -2106,7 +2110,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 @@ -2114,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 |