diff options
34 files changed, 490 insertions, 317 deletions
diff --git a/API/API.mli b/API/API.mli index 04c69b025f..879323a37d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4914,7 +4914,6 @@ module G_proofs : sig val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option end diff --git a/Makefile.ide b/Makefile.ide index 542d8c252d..7593a9f2ea 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -153,10 +153,12 @@ install-ide-bin: install-ide-toploop: ifeq ($(BEST),opt) + $(MKDIR) $(FULLCOQLIB)/toploop/ $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif install-ide-toploop-byte: ifneq ($(BEST),opt) + $(MKDIR) $(FULLCOQLIB)/toploop/ $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ endif diff --git a/Makefile.install b/Makefile.install index 4800f8f3fa..55229deb96 100644 --- a/Makefile.install +++ b/Makefile.install @@ -77,6 +77,7 @@ endif install-byte: install-coqide-byte $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS) ifndef CUSTOM diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 4a471d4a2b..bc7146884c 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -236,6 +236,7 @@ type scheme = type section_subset_expr = | SsEmpty + | SsType | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0c0b910e1d..22e109b01c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -367,7 +367,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry cook_context = None; } -let record_aux env s_ty s_bo suggested_expr = +let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = String.concat " " @@ -376,10 +376,7 @@ let record_aux env s_ty s_bo suggested_expr = if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None else Some (Id.to_string id)) (keep_hyps env s_bo)) in - Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) - -let suggest_proof_using = ref (fun _ _ _ _ _ -> "") -let set_suggest_proof_using f = suggest_proof_using := f + Aux_file.record_in_aux "context_used" v let build_constant_declaration kn env result = let open Cooking in @@ -425,16 +422,13 @@ let build_constant_declaration kn env result = (Opaqueproof.force_proof (opaque_tables env) lc) in (* we force so that cst are added to the env immediately after *) ignore(Opaqueproof.force_constraints (opaque_tables env) lc); - let expr = - !suggest_proof_using (Constant.to_string kn) - env vars ids_typ context_ids in - if !Flags.record_aux_file then record_aux env ids_typ vars expr; + if !Flags.record_aux_file then record_aux env ids_typ vars; vars in keep_hyps env (Idset.union ids_typ ids_def), def | None -> if !Flags.record_aux_file then - record_aux env Id.Set.empty Id.Set.empty ""; + record_aux env Id.Set.empty Id.Set.empty; [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) @@ -618,14 +612,10 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let context_ids = List.map NamedDecl.get_id (named_context env) in let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Opaqueproof.force_proof (opaque_tables env) lc) in - let expr = - !suggest_proof_using (Id.to_string id) - env ids_def ids_typ context_ids in - record_aux env ids_typ ids_def expr + record_aux env ids_typ ids_def end; let univs = match decl.cook_universes with | Monomorphic_const ctx -> ctx diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 24153343e7..b16f81c5a6 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -77,6 +77,3 @@ val infer_declaration : trust:'a trust -> env -> constant option -> val build_constant_declaration : constant -> env -> Cooking.result -> constant_body - -val set_suggest_proof_using : - (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit diff --git a/lib/flags.ml b/lib/flags.ml index a178eb7552..a53a866aba 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -42,7 +42,6 @@ let with_extra_values o l f x = Exninfo.iraise reraise let boot = ref false -let load_init = ref true let record_aux_file = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 8ec2a80730..5233e72a25 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -11,7 +11,6 @@ (** Command-line flags *) val boot : bool ref -val load_init : bool ref (** Set by coqtop to tell the kernel to output to the aux file; will be eventually removed by cleanups such as PR#1103 *) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e2c87bbbf6..f10d746770 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -17,12 +17,6 @@ open Pcoq.Vernac_ let thm_token = G_vernac.thm_token -let hint_proof_using e = function - | Some _ as x -> x - | None -> match Proof_using.get_default_proof_using () with - | None -> None - | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) - let hint = Gram.entry_create "hint" (* Proof commands *) @@ -35,8 +29,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3e0b85b54a..a5b58b8553 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -580,8 +580,8 @@ GEXTEND Gram starredidentref: [ [ i = identref -> SsSingl i | i = identref; "*" -> SsFwdClose(SsSingl i) - | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type") - | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]] + | "Type" -> SsType + | "Type"; "*" -> SsFwdClose SsType ]] ; ssexpr: [ "35" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d639dd0e1c..c577cb2198 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -340,7 +340,7 @@ GEXTEND Gram command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l) + Vernacexpr.VernacProof (Some (in_tac ta), l) | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> Vernacexpr.VernacProof (ta,Some l) ] ] diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 88e2cb1da5..462ffde313 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1612,7 +1612,11 @@ Section Complete. Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x). Notation "x == y" := (req x y) (at level 70, no associativity). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid3. Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. Proof. exact (Radd_ext Reqe). Qed. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index bd4e94687d..8aa0b1c91f 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -48,7 +48,11 @@ Section ZMORPHISM. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid3. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. @@ -260,7 +264,11 @@ Section NMORPHISM. Notation "0" := rO. Notation "1" := rI. Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid4. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid4. Ltac rrefl := gen_reflexivity Rsth. Variable SReqe : sring_eq_ext radd rmul req. Variable SRth : semi_ring_theory 0 1 radd rmul req. @@ -381,7 +389,11 @@ Section NWORDMORPHISM. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid5. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid5. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd with signature (req ==> req ==> req) as radd_ext5. @@ -566,7 +578,11 @@ Section GEN_DIV. Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. (* Useful tactics *) - Add Setoid R req Rsth as R_set1. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_set1. Ltac rrefl := gen_reflexivity Rsth. Add Morphism radd with signature (req ==> req ==> req) as radd_ext. Proof. exact (Radd_ext Reqe). Qed. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 335a68d70f..776ebd808d 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -404,7 +404,11 @@ Section ALMOST_RING. Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. - Add Setoid C ceq Csth as C_setoid. + Add Parametric Relation : C ceq + reflexivity proved by Csth.(@Equivalence_Reflexive _ _) + symmetry proved by Csth.(@Equivalence_Symmetric _ _) + transitivity proved by Csth.(@Equivalence_Transitive _ _) + as C_setoid. Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. Proof. exact (Radd_ext Ceqe). Qed. diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a1cdfdbaa2..d1158b3d6f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -524,7 +524,16 @@ open Decl_kinds | PrintStrategy (Some qid) -> keyword "Print Strategy" ++ pr_smart_global qid - let pr_using e = str (Proof_using.to_string e) + let pr_using e = + let rec aux = function + | SsEmpty -> "()" + | SsType -> "(Type)" + | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsCompl e -> "-" ^ aux e^"" + | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" + | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" + | SsFwdClose e -> "("^aux e^")*" + in Pp.str (aux e) let rec pr_vernac_body v = let return = tag_vernac v in diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index b88eed4843..cf27b413c0 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -15,5 +15,8 @@ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation lis (** Prints a vernac expression *) val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t +(** Prints a "proof using X" clause. *) +val pr_using : Vernacexpr.section_subset_expr -> Pp.t + (** Prints a vernac expression and closes it with a dot. *) val pr_vernac : Vernacexpr.vernac_expr -> Pp.t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index eaf0c693e1..058e839b47 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_using Proof_type Logic Refine diff --git a/stm/stm.ml b/stm/stm.ml index 220ed9be4e..d1693519dc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -250,8 +250,8 @@ end (* }}} *) (* The main document type associated to a VCS *) type stm_doc_type = - | VoDoc of Names.DirPath.t - | VioDoc of Names.DirPath.t + | VoDoc of string + | VioDoc of string | Interactive of Names.DirPath.t (* Dummy until we land the functional interp patch + fixed start_library *) @@ -276,6 +276,9 @@ module VCS : sig val init : stm_doc_type -> id -> doc (* val get_type : unit -> stm_doc_type *) + val set_ldir : Names.DirPath.t -> unit + val get_ldir : unit -> Names.DirPath.t + val is_interactive : unit -> [`Yes | `No | `Shallow] val is_vio_doc : unit -> bool @@ -460,6 +463,7 @@ end = struct (* {{{ *) let vcs : vcs ref = ref (empty Stateid.dummy) let doc_type = ref (Interactive (Names.DirPath.make [])) + let ldir = ref Names.DirPath.empty let init dt id = doc_type := dt; @@ -467,6 +471,10 @@ end = struct (* {{{ *) vcs := set_info !vcs id (default_info ()); dummy_doc + let set_ldir ld = + ldir := ld + + let get_ldir () = !ldir (* let get_type () = !doc_type *) let is_interactive () = @@ -697,7 +705,7 @@ let state_of_id ~doc id = (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig - + (** The function is from unit, so it uses the current state to define a new one. I.e. one may been to install the right state before defining a new one. @@ -713,7 +721,6 @@ module State : sig val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool - val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) type frozen_state @@ -727,9 +734,15 @@ module State : sig val proof_part_of_frozen : frozen_state -> proof_part val assign : Stateid.t -> partial_state -> unit + (* Handlers for initial state, prior to document creation. *) + val register_root_state : unit -> unit + val restore_root_state : unit -> unit + (* Only for internal use to catch problems in parse_sentence, should be removed in the state handling refactoring. *) val cur_id : Stateid.t ref + + end = struct (* {{{ *) (* cur_id holds Stateid.dummy in case the last attempt to define a state @@ -879,6 +892,15 @@ end = struct (* {{{ *) Hooks.(call unreachable_state id ie); Exninfo.iraise ie + let init_state = ref None + + let register_root_state () = + init_state := Some (freeze_global_state `No) + + let restore_root_state () = + cur_id := Stateid.dummy; + unfreeze_global_state Option.(get !init_state) + end (* }}} *) (* indentation code for Show Script, initially contributed @@ -1145,16 +1167,12 @@ let set_compilation_hints file = let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in - match Str.split (Str.regexp ";") s with - | ids :: _ -> - let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in - let ids = List.map (fun id -> Loc.tag id) ids in - begin match ids with - | [] -> SsEmpty - | x :: xs -> - List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs - end - | _ -> raise Not_found + let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in + let ids = List.map (fun id -> Loc.tag id) ids in + match ids with + | [] -> SsEmpty + | x :: xs -> + List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs let get_hint_bp_time proof_name = try float_of_string (Aux_file.get !hints proof_name) @@ -2365,19 +2383,55 @@ end (* }}} *) type stm_init_options = { doc_type : stm_doc_type; + require_libs : (string * string option * bool option) list; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; - require_libs : (Names.DirPath.t * string * bool option) list; implicit_std : bool; *) } -let init { doc_type } = +(* +let doc_type_module_name (std : stm_doc_type) = + match std with + | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn + | Interactive mn -> Names.DirPath.to_string mn +*) + +let init_core () = + State.register_root_state () + +let new_doc { doc_type ; require_libs } = + let load_objs libs = + let rq_file (dir, from, exp) = + let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in + let mfrom = Option.map (fun fr -> Libnames.(Qualid (Loc.tag @@ qualid_of_string fr))) from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in + List.(iter rq_file (rev libs)) + in + + (* We must reset the whole state before creating a document! *) + State.restore_root_state (); + let doc = VCS.init doc_type Stateid.initial in set_undo_classifier Backtrack.undo_vernac_classifier; - (* we declare the library here XXX: *) - State.define ~cache:`Yes (fun () -> ()) Stateid.initial; + + begin match doc_type with + | Interactive ln -> + Declaremods.start_library ln + | VoDoc ln -> + let ldir = Flags.verbosely Library.start_library ln in + VCS.set_ldir ldir; + set_compilation_hints ln + | VioDoc ln -> + let ldir = Flags.verbosely Library.start_library ln in + VCS.set_ldir ldir; + set_compilation_hints ln + end; + load_objs require_libs; + + (* We record the state here! *) + State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin @@ -2393,7 +2447,7 @@ let init { doc_type } = (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env)) with Not_found -> () end; end; - doc + doc, VCS.cur_tip () let observe ~doc id = let vcs = VCS.backup () in @@ -2456,6 +2510,7 @@ let check_task name (tasks,rcbackup) i = rc with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks + let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = @@ -2953,6 +3008,7 @@ let edit_at ~doc id = Exninfo.iraise (e, info) let get_current_state ~doc = VCS.cur_tip () +let get_ldir ~doc = VCS.get_ldir () let get_doc did = dummy_doc diff --git a/stm/stm.mli b/stm/stm.mli index 47963e5d81..c65cf6a9af 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,17 +13,17 @@ open Names (** The STM doc type determines some properties such as what uncompleted proofs are allowed and recording of aux files. *) type stm_doc_type = - | VoDoc of DirPath.t - | VioDoc of DirPath.t + | VoDoc of string + | VioDoc of string | Interactive of DirPath.t (* Main initalization routine *) type stm_init_options = { doc_type : stm_doc_type; + require_libs : (string * string option * bool option) list; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; - require_libs : (Names.DirPath.t * string * bool option) list; implicit_std : bool; *) } @@ -31,7 +31,10 @@ type stm_init_options = { (** The type of a STM document *) type doc -val init : stm_init_options -> doc +val init_core : unit -> unit + +(* Starts a new document *) +val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) @@ -105,6 +108,7 @@ val finish_tasks : string -> (* Id of the tip of the current branch *) val get_current_state : doc:doc -> Stateid.t +val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option diff --git a/test-suite/bugs/closed/1322.v b/test-suite/bugs/closed/1322.v index 1ec7d452a6..6941ade44c 100644 --- a/test-suite/bugs/closed/1322.v +++ b/test-suite/bugs/closed/1322.v @@ -12,7 +12,11 @@ Variable I_eq_equiv : Setoid_Theory I I_eq. transitivity proved by I_eq_equiv.(Seq_trans I I_eq) as I_eq_relation. *) -Add Setoid I I_eq I_eq_equiv as I_with_eq. +Add Parametric Relation : I I_eq + reflexivity proved by I_eq_equiv.(@Equivalence_Reflexive _ _) + symmetry proved by I_eq_equiv.(@Equivalence_Symmetric _ _) + transitivity proved by I_eq_equiv.(@Equivalence_Transitive _ _) + as I_with_eq. Variable F : I -> Type. Variable F_morphism : forall i j, I_eq i j -> F i = F j. diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out new file mode 100644 index 0000000000..8d67a4a4b7 --- /dev/null +++ b/test-suite/output/SuggestProofUsing.out @@ -0,0 +1,7 @@ +The proof of nat should start with one of the following commands: +Proof using . +Proof using Type*. +Proof using Type. +The proof of foo should start with one of the following commands: +Proof using A B. +Proof using All. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v new file mode 100644 index 0000000000..00b6f8e183 --- /dev/null +++ b/test-suite/output/SuggestProofUsing.v @@ -0,0 +1,31 @@ +Set Suggest Proof Using. + +Section Sec. + Variables A B : Type. + + (* Some normal lemma. *) + Lemma nat : Set. + Proof. + exact nat. + Qed. + + (* Make sure All is suggested even though we add an unused variable + to the context. *) + Let foo : Type. + Proof. + exact (A -> B). + Qed. + + (* Having a [Proof using] disables the suggestion message. *) + Definition bar : Type. + Proof using A. + exact A. + Qed. + + (* Transparent definitions don't get a suggestion message. *) + Definition baz : Type. + Proof. + exact A. + Defined. + +End Sec. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index cfa5526025..8f79f8a669 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -179,8 +179,6 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) - # FIXME This should be generated by Coq GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) @@ -189,7 +187,12 @@ else CAMLP4EXTEND= endif +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") +else PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +endif ifneq (,$(TIMING)) TIMING_ARG=-time diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index bf22c16cd3..c808992887 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,9 +59,9 @@ let load_rcfile doc sid = doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) -let add_stdlib_path ~unix_path ~coq_root ~with_ml = +let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml = let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in - Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init) + Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init let add_userlib_path ~unix_path = Mltop.add_rec_path Mltop.AddRecML ~unix_path @@ -75,7 +75,7 @@ let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes (* Initializes the LoadPath *) -let init_load_path () = +let init_load_path ~load_init = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in @@ -93,9 +93,9 @@ let init_load_path () = if System.exists_dir (coqlib/"toploop") then Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) - add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; + add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) - add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; + add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; (* then user-contrib *) if Sys.file_exists user_contrib then add_userlib_path ~unix_path:user_contrib; diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 2c275a00d3..60ed698b87 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -20,6 +20,6 @@ val push_include : string -> Names.DirPath.t -> bool -> unit val push_ml_include : string -> unit -val init_load_path : unit -> unit +val init_load_path : load_init:bool -> unit val init_ocaml_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9b58c9a654..e9fdaac5bf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -188,11 +188,9 @@ let load_vernacular doc sid = Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s) (doc, sid) (List.rev !load_vernacular_list) -let load_vernacular_obj = ref ([] : string list) -let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj -let load_vernac_obj () = - let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in - Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) +let load_init_vernaculars doc sid = + let doc, sid = Coqinit.load_rcfile doc sid in + load_vernacular doc sid (******************************************************************************) (* Required Modules *) @@ -201,26 +199,23 @@ let set_include d p implicit = let p = dirpath_of_string p in Coqinit.push_include d p implicit -let require_prelude () = - let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in - let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in - let m = - if Sys.file_exists vo then vo else - if Sys.file_exists vio then vio else vo in - Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true) - -let require_list = ref ([] : string list) +(* None = No Import; Some false = Import; Some true = Export *) +let require_list = ref ([] : (string * string option * bool option) list) let add_require s = require_list := s :: !require_list -let require () = - let () = if !Flags.load_init then Flags.silently require_prelude () in - let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in - Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) + +let load_init = ref true + +(* From Coq Require Import Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true + +let require_libs () = + if !load_init then prelude_data :: !require_list else !require_list let add_compat_require v = match v with - | Flags.V8_5 -> add_require "Coq.Compat.Coq85" - | Flags.V8_6 -> add_require "Coq.Compat.Coq86" - | Flags.V8_7 -> add_require "Coq.Compat.Coq87" + | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false) + | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false) + | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false) | Flags.VOld | Flags.Current -> () (******************************************************************************) @@ -230,9 +225,9 @@ let add_compat_require v = let glob_opt = ref false let compile_list = ref ([] : (bool * string) list) -let _compilation_list : Stm.stm_doc_type list ref = ref [] -let compilation_mode = ref Vernac.BuildVo +type compilation_mode = BuildVo | BuildVio | Vio2Vo +let compilation_mode = ref BuildVo let compilation_output_name = ref None let batch_mode = ref false @@ -253,21 +248,140 @@ let add_compile verbose s = in compile_list := (verbose,s) :: !compile_list -let compile_file mode doc (verbosely,f_in) = +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + +let ensure_ext ext f = + if Filename.check_suffix f ext then f + else begin + warn_file_no_extension (f,ext); + f ^ ext + end + +let chop_extension f = + try Filename.chop_extension f with _ -> f + +let compile_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let ensure_bname src tgt = + let src, tgt = Filename.basename src, Filename.basename tgt in + let src, tgt = chop_extension src, chop_extension tgt in + if src <> tgt then + compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) + +let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt + +let ensure_v v = ensure ".v" v v +let ensure_vo v vo = ensure ".vo" v vo +let ensure_vio v vio = ensure ".vio" v vio + +let ensure_exists f = + if not (Sys.file_exists f) then + compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) + +(* Compile a vernac file *) +let compile ~verbosely ~f_in ~f_out = + let check_pending_proofs () = + let pfs = Proof_global.get_all_proof_names () in + if not (CList.is_empty pfs) then + compile_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") + in + match !compilation_mode with + | BuildVo -> + Flags.record_aux_file := true; + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + let long_f_dot_vo = + match f_out with + | None -> long_f_dot_v ^ "o" + | Some f -> ensure_vo long_f_dot_v f in + + let doc, sid = Stm.(new_doc + { doc_type = VoDoc long_f_dot_vo; + require_libs = require_libs () + }) in + + let doc, sid = load_init_vernaculars doc sid in + let ldir = Stm.get_ldir ~doc in + Aux_file.(start_aux_file + ~aux_file:(aux_file_name_for long_f_dot_vo) + ~v_file:long_f_dot_v); + Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; + Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); + let wall_clock1 = Unix.gettimeofday () in + let doc, _ = Vernac.load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let _doc = Stm.join ~doc in + let wall_clock2 = Unix.gettimeofday () in + check_pending_proofs (); + Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + Aux_file.record_in_aux_at "vo_compile_time" + (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); + Aux_file.stop_aux_file (); + Dumpglob.end_dump_glob () + | BuildVio -> + + Flags.record_aux_file := false; + Dumpglob.noglob (); + + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + + let long_f_dot_vio = + match f_out with + | None -> long_f_dot_v ^ "io" + | Some f -> ensure_vio long_f_dot_v f in + + let doc, sid = Stm.(new_doc + { doc_type = VioDoc long_f_dot_vio; + require_libs = require_libs () + }) in + + let doc, sid = load_init_vernaculars doc sid in + + let ldir = Stm.get_ldir ~doc in + let doc, _ = Vernac.load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc = Stm.finish ~doc in + check_pending_proofs (); + let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + Stm.reset_task_queue () + + | Vio2Vo -> + let open Filename in + Flags.record_aux_file := false; + Dumpglob.noglob (); + let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in + let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in + let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in + Library.save_library_raw lfdv sum lib univs proofs + +let compile ~verbosely ~f_in ~f_out = + ignore(CoqworkmgrApi.get 1); + compile ~verbosely ~f_in ~f_out; + CoqworkmgrApi.giveback 1 + +let compile_file (verbosely,f_in) = if !Flags.beautify then - Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None) f_in + Flags.with_option Flags.beautify_file + (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in else - Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None + compile ~verbosely ~f_in ~f_out:None let compile_files doc = if !compile_list == [] then () - else - let init_state = States.freeze ~marshallable:`No in - let mode = !compilation_mode in - List.iter (fun vf -> - States.unfreeze init_state; - compile_file mode doc vf) - (List.rev !compile_list) + else List.iter compile_file (List.rev !compile_list) (******************************************************************************) (* VIO Dispatching *) @@ -279,7 +393,7 @@ let add_vio_task f = Flags.quiet := true; vio_tasks := f :: !vio_tasks -let check_vio_tasks doc = +let check_vio_tasks () = let rc = List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) true (List.rev !vio_tasks) in @@ -303,7 +417,7 @@ let set_vio_checking_j opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 -let schedule_vio_checking doc = +let schedule_vio_checking () = if !vio_files <> [] && !vio_checking then Vio_checking.schedule_vio_checking !vio_files_j !vio_files @@ -374,7 +488,7 @@ let usage batch = begin try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); - Coqinit.init_load_path (); + Coqinit.init_load_path ~load_init:!load_init; with NoCoqLib -> usage_no_coqlib () end; if batch then Usage.print_usage_coqc () @@ -563,20 +677,20 @@ let parse_args arglist = |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) |"-load-ml-source" -> Mltop.dir_ml_use (next ()) - |"-load-vernac-object" -> add_vernac_obj (next ()) + |"-load-vernac-object" -> add_require (next (), None, None) |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next ()) + |"-require" -> add_require (next (), None, Some false) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); - compilation_mode := Vernac.Vio2Vo + compilation_mode := Vio2Vo |"-toploop" -> set_toploop (next ()) |"-w" | "-W" -> let w = next () in @@ -609,7 +723,7 @@ let parse_args arglist = |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> Flags.load_init := false + |"-noinit"|"-nois" -> load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then @@ -621,11 +735,11 @@ let parse_args arglist = |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false |"-quick" -> Safe_typing.allow_delayed_constants := true; - compilation_mode := Vernac.BuildVio + compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require "Utf8_core" + |"-unicode" -> add_require ("Utf8_core", None, Some false) |"-v"|"--version" -> Usage.version (exitcode ()) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true @@ -640,12 +754,18 @@ let parse_args arglist = with any -> fatal_error any let init_toplevel arglist = + (* Coq's init process, phase 1: + - OCaml parameters, and basic structures and IO + *) Profile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); - let doc = begin + (* Coq's init process, phase 2: + - Basic Coq environment, load-path, plugins. + *) + let res = begin try let extras = parse_args arglist in (* If we have been spawned by the Spawn module, this has to be done @@ -656,7 +776,7 @@ let init_toplevel arglist = if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - Coqinit.init_load_path (); + Coqinit.init_load_path ~load_init:!load_init; Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin @@ -665,52 +785,67 @@ let init_toplevel arglist = exit 1 end; Flags.if_verbose print_header (); - inputstate (); Mltop.init_known_plugins (); engage (); + + (* Allow the user to load an arbitrary state here *) + inputstate (); + + (* This state will be shared by all the documents *) + Stm.init_core (); + + (* Coq init process, phase 3: Stm initialization, backtracking state. + + It is essential that the module system is in a consistent + state before we take the first snapshot. This was not + guaranteed in the past. In particular, we want to be sure we + have called start_library before loading the prelude and rest + of required files. + + We split the codepath here depending whether coqtop is called + in interactive mode or not. *) + if (not !batch_mode || CList.is_empty !compile_list) - && Global.env_is_initial () - then Declaremods.start_library !toplevel_name; - load_vernac_obj (); - require (); - let doc = Stm.(init { doc_type = Interactive Names.DirPath.empty }) in - let doc, sid = Coqinit.load_rcfile doc (Stm.get_current_state ~doc) in - (* XXX: We ignore this for now, but should be threaded to the toplevels *) - let doc, _sid = load_vernacular doc sid in - compile_files doc; - (* All these tasks use coqtop as a driver to invoke more coqtop, - * they should be really orthogonal to coqtop. - *) - schedule_vio_checking doc; - schedule_vio_compilation (); - check_vio_tasks doc; - outputstate (); - doc + (* Interactive *) + then begin + try + let doc, sid = Stm.(new_doc + { doc_type = Interactive !toplevel_name; + require_libs = require_libs () + }) in + Some (load_init_vernaculars doc sid) + with any -> flush_all(); fatal_error any + (* Non interactive *) + end else begin + try + compile_files (); + schedule_vio_checking (); + schedule_vio_compilation (); + check_vio_tasks (); + (* Allow the user to output an arbitrary state *) + outputstate (); + None + with any -> flush_all(); fatal_error any + end; with any -> flush_all(); - let extra = None - (* XXX: Must refine once Stm.init takes care of the start_library & friends *) - (* if !batch_mode && not Stateid.(equal (Stm.get_current_state ~doc) dummy) *) - (* then None *) - (* else Some (str "Error during initialization: ") *) - in + let extra = Some (str "Error during initialization: ") in fatal_error ?extra any end in - if !batch_mode then begin + Feedback.del_feeder init_feeder; + res + +let start () = + match init_toplevel (List.tl (Array.to_list Sys.argv)) with + (* Batch mode *) + | Some (doc, sid) when not !batch_mode -> + !toploop_run doc; + exit 1 + | _ -> flush_all(); if !output_context then Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 - end; - Feedback.del_feeder init_feeder; - doc - -let start () = - let doc = init_toplevel (List.tl (Array.to_list Sys.argv)) in - (* In batch mode, Coqtop has already exited at this point. In interactive one, - dump glob is nothing but garbage ... *) - !toploop_run doc; - exit 1 (* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 4c26a6ebcc..1c7c3f944a 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,7 +11,7 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> Stm.doc +val init_toplevel : string list -> (Stm.doc * Stateid.t) option val start : unit -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1e09a1c0d2..d736975d32 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -103,11 +103,6 @@ let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () with Proof_global.NoCurrentProof -> Pp.str "" -let vernac_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -247,105 +242,3 @@ and load_vernac ~verbosely ~check ~interactive doc sid file = let process_expr doc sid loc_ast = checknav_deep loc_ast; interp_vernac ~interactive:true ~check:true doc sid loc_ast - -let warn_file_no_extension = - CWarnings.create ~name:"file-no-extension" ~category:"filesystem" - (fun (f,ext) -> - str "File \"" ++ str f ++ - strbrk "\" has been implicitly expanded to \"" ++ - str f ++ str ext ++ str "\"") - -let ensure_ext ext f = - if Filename.check_suffix f ext then f - else begin - warn_file_no_extension (f,ext); - f ^ ext - end - -let chop_extension f = - try Filename.chop_extension f with _ -> f - -let ensure_bname src tgt = - let src, tgt = Filename.basename src, Filename.basename tgt in - let src, tgt = chop_extension src, chop_extension tgt in - if src <> tgt then - vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ - str "Source: " ++ str src ++ fnl () ++ - str "Target: " ++ str tgt) - -let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt - -let ensure_v v = ensure ".v" v v -let ensure_vo v vo = ensure ".vo" v vo -let ensure_vio v vio = ensure ".vio" v vio - -let ensure_exists f = - if not (Sys.file_exists f) then - vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -type compilation_mode = BuildVo | BuildVio | Vio2Vo - -(* Compile a vernac file *) -let compile ~verbosely ~mode ~doc ~f_in ~f_out= - let check_pending_proofs () = - let pfs = Proof_global.get_all_proof_names () in - if not (List.is_empty pfs) then - vernac_error (str "There are pending proofs: " - ++ (pfs - |> List.rev - |> prlist_with_sep pr_comma Names.Id.print) - ++ str ".") - in - match mode with - | BuildVo -> - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - let long_f_dot_vo = - match f_out with - | None -> long_f_dot_v ^ "o" - | Some f -> ensure_vo long_f_dot_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_vo in - Stm.set_compilation_hints long_f_dot_vo; - Aux_file.(start_aux_file - ~aux_file:(aux_file_name_for long_f_dot_vo) - ~v_file:long_f_dot_v); - Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; - Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); - let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let _doc = Stm.join ~doc in - let wall_clock2 = Unix.gettimeofday () in - check_pending_proofs (); - Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); - Aux_file.record_in_aux_at "vo_compile_time" - (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - Aux_file.stop_aux_file (); - Dumpglob.end_dump_glob () - | BuildVio -> - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - let long_f_dot_vio = - match f_out with - | None -> long_f_dot_v ^ "io" - | Some f -> ensure_vio long_f_dot_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_vio in - Dumpglob.noglob (); - Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let doc = Stm.finish ~doc in - check_pending_proofs (); - let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in - Stm.reset_task_queue () - | Vio2Vo -> - let open Filename in - Dumpglob.noglob (); - let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in - let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in - Stm.set_compilation_hints lfdv; - let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in - Library.save_library_raw lfdv sum lib univs proofs - -let compile ~verbosely ~mode ~doc ~f_in ~f_out = - ignore(CoqworkmgrApi.get 1); - compile ~verbosely ~mode ~doc ~f_in ~f_out; - CoqworkmgrApi.giveback 1 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d3a45ce9de..f9a4300267 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -18,8 +18,3 @@ val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t - -type compilation_mode = BuildVo | BuildVio | Vio2Vo - -(** Compile a vernac file, (f is assumed without .v suffix) *) -val compile : verbosely:bool -> mode:compilation_mode -> doc:Stm.doc -> f_in:string -> f_out:string option -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2c8f6ec9d6..d45665dd4c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -180,10 +180,14 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = try let const = adjust_guardness_conditions const do_guard in let k = Kindops.logical_kind_of_goal_kind kind in + let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in + let () = if should_suggest + then Proof_using.suggest_variable (Global.env ()) id + in (Local, VarRef id) | Local | Global | Discharge -> let local = match locality with @@ -192,7 +196,11 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = in let kn = declare_constant ?export_seff id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) in + let () = if should_suggest + then Proof_using.suggest_constant (Global.env ()) kn + in + (locality, ConstRef kn) + in definition_message id; Option.iter (Universes.register_universe_binders r) pl; call_hook (fun exn -> exn) hook l r diff --git a/proofs/proof_using.ml b/vernac/proof_using.ml index 1a321120c6..ffe99cfd81 100644 --- a/proofs/proof_using.ml +++ b/vernac/proof_using.ml @@ -14,16 +14,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -let to_string e = - let rec aux = function - | SsEmpty -> "()" - | SsSingl (_,id) -> "("^Id.to_string id^")" - | SsCompl e -> "-" ^ aux e^"" - | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" - | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" - | SsFwdClose e -> "("^aux e^")*" - in aux e - let known_names = Summary.ref [] ~name:"proofusing-nameset" let in_nameset = @@ -48,12 +38,20 @@ let rec close_fwd e s = s (named_context e) in if Id.Set.equal s s' then s else close_fwd e s' -;; + +let set_of_type env ty = + List.fold_left (fun acc ty -> + Id.Set.union (global_vars_set env ty) acc) + Id.Set.empty ty + +let full_set env = + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty let rec process_expr env e ty = let rec aux = function | SsEmpty -> Id.Set.empty - | SsSingl (_,id) -> set_of_id env ty id + | SsType -> set_of_type env ty + | SsSingl (_,id) -> set_of_id env id | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) | SsCompl e -> Id.Set.diff (full_set env) (aux e) @@ -61,23 +59,15 @@ let rec process_expr env e ty = in aux e -and set_of_id env ty id = - if Id.to_string id = "Type" then - List.fold_left (fun acc ty -> - Id.Set.union (global_vars_set env ty) acc) - Id.Set.empty ty - else if Id.to_string id = "All" then +and set_of_id env id = + if Id.to_string id = "All" then List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id -and full_set env = - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - let process_expr env e ty = - let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in - let v_ty = process_expr env ty_expr ty in + let v_ty = set_of_type env ty in let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s @@ -105,7 +95,13 @@ let remove_ids_and_lets env s ids = (no_body id || Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s) -let suggest_Proof_using name env vars ids_typ context_ids = +let record_proof_using expr = + Aux_file.record_in_aux "suggest_proof_using" expr + +(* Variables in [skip] come from after the definition, so don't count + for "All". Used in the variable case since the env contains the + variable itself. *) +let suggest_common env ppid used ids_typ skip = let module S = Id.Set in let open Pp in let print x = Feedback.msg_debug x in @@ -114,10 +110,13 @@ let suggest_Proof_using name env vars ids_typ context_ids = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" else ppcmds in wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in - let used = S.union vars ids_typ in + let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in let all_needed = really_needed env needed in - let all = List.fold_right S.add context_ids S.empty in + let all = List.fold_left (fun all d -> S.add (NamedDecl.get_id d) all) + S.empty (named_context env) + in + let all = S.diff all skip in let fwd_typ = close_fwd env ids_typ in if !Flags.debug then begin print (str "All " ++ pr_set false all); @@ -133,36 +132,59 @@ let suggest_Proof_using name env vars ids_typ context_ids = if S.equal all all_needed then valid(str "All"); valid (pr_set false needed); Feedback.msg_info ( - str"The proof of "++ str name ++ spc() ++ + str"The proof of "++ ppid ++ spc() ++ str "should start with one of the following commands:"++spc()++ v 0 ( prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) -;; + if !Flags.record_aux_file + then + let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in + record_proof_using s -let value = ref false +let suggest_proof_using = ref false let _ = Goptions.declare_bool_option { Goptions.optdepr = false; Goptions.optname = "suggest Proof using"; Goptions.optkey = ["Suggest";"Proof";"Using"]; - Goptions.optread = (fun () -> !value); - Goptions.optwrite = (fun b -> - value := b; - if b then Term_typing.set_suggest_proof_using suggest_Proof_using - else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "") - ) } + Goptions.optread = (fun () -> !suggest_proof_using); + Goptions.optwrite = ((:=) suggest_proof_using) } + +let suggest_constant env kn = + if !suggest_proof_using + then begin + let open Declarations in + let body = lookup_constant kn env in + let used = Id.Set.of_list @@ List.map NamedDecl.get_id body.const_hyps in + let ids_typ = global_vars_set env body.const_type in + suggest_common env (Printer.pr_constant env kn) used ids_typ Id.Set.empty + end + +let suggest_variable env id = + if !suggest_proof_using + then begin + match lookup_named id env with + | LocalDef (_,body,typ) -> + let ids_typ = global_vars_set env typ in + let ids_body = global_vars_set env body in + let used = Id.Set.union ids_body ids_typ in + suggest_common env (Id.print id) used ids_typ (Id.Set.singleton id) + | LocalAssum _ -> assert false + end let value = ref None +let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) +let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us))) + let _ = Goptions.declare_stringopt_option { Goptions.optdepr = false; Goptions.optname = "default value for Proof using"; Goptions.optkey = ["Default";"Proof";"Using"]; - Goptions.optread = (fun () -> !value); - Goptions.optwrite = (fun b -> value := b;) } - + Goptions.optread = (fun () -> Option.map using_to_string !value); + Goptions.optwrite = (fun b -> value := Option.map using_from_string b); + } let get_default_proof_using () = !value diff --git a/proofs/proof_using.mli b/vernac/proof_using.mli index c882b1827a..f63c8e2424 100644 --- a/proofs/proof_using.mli +++ b/vernac/proof_using.mli @@ -14,6 +14,8 @@ val process_expr : val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit -val to_string : Vernacexpr.section_subset_expr -> string +val suggest_constant : Environ.env -> Names.Constant.t -> unit -val get_default_proof_using : unit -> string option +val suggest_variable : Environ.env -> Names.Id.t -> unit + +val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index f74073e1f7..850902d6ba 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,4 +1,5 @@ Vernacprop +Proof_using Lemmas Himsg ExplainErr diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 203d913db8..66427b7093 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2060,17 +2060,13 @@ let interp ?proof ?loc locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no" - | VernacProof (Some tac, None) -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no"; - vernac_set_end_tac tac - | VernacProof (None, Some l) -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes"; - vernac_set_used_variables l - | VernacProof (Some tac, Some l) -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes"; - vernac_set_end_tac tac; vernac_set_used_variables l + | VernacProof (tac, using) -> + let using = Option.append using (Proof_using.get_default_proof_using ()) in + let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in + let usings = if Option.is_empty using then "using:no" else "using:yes" in + Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings); + Option.iter vernac_set_end_tac tac; + Option.iter vernac_set_used_variables using | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) |