From 1fd4c22d493715f154f6b79dc7f6e4efd44ff185 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Nov 2020 18:52:30 +0100 Subject: [ltac] break dependency on the STM --- lib/stateid.ml | 3 +++ lib/stateid.mli | 7 +++++++ plugins/ltac/profile_ltac.ml | 6 +----- stm/stm.ml | 3 +++ 4 files changed, 14 insertions(+), 5 deletions(-) diff --git a/lib/stateid.ml b/lib/stateid.ml index a1328f156c..2a41cb7866 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -45,3 +45,6 @@ type ('a,'b) request = { name : string } +let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true) +let is_valid ~doc id = !is_valid_ref ~doc id +let set_is_valid f = is_valid_ref := f diff --git a/lib/stateid.mli b/lib/stateid.mli index 9b2de9c894..4563710f84 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -42,3 +42,10 @@ type ('a,'b) request = { name : string } +(* Asks the document manager is the given state is valid (or belongs to an + old version of the document) *) +val is_valid : doc:int -> t -> bool + +(* By default [is_valid] always answers true, but a document manager supporting + undo operations like the STM can override this. *) +val set_is_valid : (doc:int -> t -> bool) -> unit diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index aa2449d962..937d579012 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -436,11 +436,7 @@ let finish_timing ~prefix name = (* ******************** *) let print_results_filter ~cutoff ~filter = - (* The STM doesn't provide yet a proper document query and traversal - API, thus we need to re-check if some states are current anymore - (due to backtracking) using the `state_of_id` API. *) - let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in - data := SM.filter valid !data; + data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data; let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in diff --git a/stm/stm.ml b/stm/stm.ml index 0b00524bd5..27f2b6fc5c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -801,6 +801,9 @@ let state_of_id ~doc id = | EmptyState | ParsingState _ -> `Valid None with VCS.Expired -> `Expired +let () = + Stateid.set_is_valid (fun ~doc id -> state_of_id ~doc id <> `Expired) + (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig -- cgit v1.2.3 From 4390b6907b3d07793c2e8f9e7ad3cc38d9488711 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Sep 2020 14:04:53 +0200 Subject: [vernac] move vernac_classifier to vernac --- stm/stm.mllib | 1 - stm/vernac_classifier.ml | 215 ------------------------------------------- stm/vernac_classifier.mli | 19 ---- vernac/vernac.mllib | 1 + vernac/vernac_classifier.ml | 215 +++++++++++++++++++++++++++++++++++++++++++ vernac/vernac_classifier.mli | 19 ++++ 6 files changed, 235 insertions(+), 235 deletions(-) delete mode 100644 stm/vernac_classifier.ml delete mode 100644 stm/vernac_classifier.mli create mode 100644 vernac/vernac_classifier.ml create mode 100644 vernac/vernac_classifier.mli diff --git a/stm/stm.mllib b/stm/stm.mllib index 831369625f..49e7195e27 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -3,7 +3,6 @@ Dag Vcs TQueue WorkerPool -Vernac_classifier CoqworkmgrApi AsyncTaskQueue Partac diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml deleted file mode 100644 index ffae2866c0..0000000000 --- a/stm/vernac_classifier.ml +++ /dev/null @@ -1,215 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* "Later" - | VtNow -> "Now" - -let string_of_vernac_classification = function - | VtStartProof _ -> "StartProof" - | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w) - | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" - | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" - | VtQed VtDrop -> "Qed(drop)" - | VtProofStep { proof_block_detection } -> - "ProofStep " ^ Option.default "" proof_block_detection - | VtQuery -> "Query" - | VtMeta -> "Meta " - | VtProofMode _ -> "Proof Mode" - -let vtkeep_of_opaque = function - | Opaque -> VtKeepOpaque - | Transparent -> VtKeepDefined - -let idents_of_name : Names.Name.t -> Names.Id.t list = - function - | Names.Anonymous -> [] - | Names.Name n -> [n] - -let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] - -let options_affecting_stm_scheduling = - [ Attributes.universe_polymorphism_option_name; - stm_allow_nested_proofs_option_name; - Vernacinterp.proof_mode_opt_name; - Attributes.program_mode_option_name; - Proof_using.proof_using_opt_name; - ] - -let classify_vernac e = - let static_classifier ~atts e = match e with - (* Univ poly compatibility: we run it now, so that we can just - * look at Flags in stm.ml. Would be nicer to have the stm - * look at the entire dag to detect this option. *) - | VernacSetOption (_, l,_) - when CList.exists (CList.equal String.equal l) - options_affecting_stm_scheduling -> - VtSideff ([], VtNow) - (* Qed *) - | VernacAbort _ -> VtQed VtDrop - | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom) - | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)) - | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque) - (* Query *) - | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery - (* ProofStep *) - | VernacProof _ - | VernacFocus _ | VernacUnfocus - | VernacSubproof _ - | VernacCheckGuard - | VernacUnfocused - | VernacSolveExistential _ -> - VtProofStep { proof_block_detection = None } - | VernacBullet _ -> - VtProofStep { proof_block_detection = Some "bullet" } - | VernacEndSubproof -> - VtProofStep { proof_block_detection = Some "curly" } - (* StartProof *) - | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> - VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) - - | VernacDefinition (_,({v=i},_),ProveBody _) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i) - | VernacStartTheoremProof (_,l) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids) - | VernacFixpoint (discharge,l) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = - if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity - else GuaranteesOpacity - in - let ids, open_proof = - List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} -> - id::l, b || body_def = None) ([],false) l in - if open_proof - then VtStartProof (guarantee,ids) - else VtSideff (ids, VtLater) - | VernacCoFixpoint (discharge,l) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = - if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity - else GuaranteesOpacity - in - let ids, open_proof = - List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } -> - id::l, b || body_def = None) ([],false) l in - if open_proof - then VtStartProof (guarantee,ids) - else VtSideff (ids, VtLater) - (* Sideff: apply to all open branches. usually run on master only *) - | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in - VtSideff (ids, VtLater) - | VernacPrimitive ((id,_),_,_) -> - VtSideff ([id.CAst.v], VtLater) - | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) - | VernacInductive (_,l) -> - let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with - | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l - | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ - CList.map_filter (function - | AssumExpr({v=Names.Name n},_,_), _ -> Some n - | _ -> None) l) l in - VtSideff (List.flatten ids, VtLater) - | VernacScheme l -> - let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in - VtSideff (ids, VtLater) - | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater) - | VernacBeginSection {v=id} -> VtSideff ([id], VtLater) - | VernacUniverse _ | VernacConstraint _ - | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ - | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ - | VernacChdir _ - | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacArguments _ - | VernacReserve _ - | VernacGeneralizable _ - | VernacSetOpacity _ | VernacSetStrategy _ - | VernacSetOption _ - | VernacAddOption _ | VernacRemoveOption _ - | VernacMemOption _ | VernacPrintOption _ - | VernacGlobalCheck _ - | VernacDeclareReduction _ - | VernacExistingClass _ | VernacExistingInstance _ - | VernacRegister _ - | VernacNameSectionHypSet _ - | VernacComments _ - | VernacDeclareInstance _ -> VtSideff ([], VtLater) - (* Who knows *) - | VernacLoad _ -> VtSideff ([], VtNow) - (* (Local) Notations have to disappear *) - | VernacEndSegment _ -> VtSideff ([], VtNow) - (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (exp,{v=id},bl,_) - | VernacDefineModule (exp,{v=id},bl,_,_) -> - VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow) - | VernacDeclareModuleType ({v=id},bl,_,_) -> - VtSideff ([id], if bl = [] then VtLater else VtNow) - (* These commands alter the parser *) - | VernacDeclareCustomEntry _ - | VernacOpenCloseScope _ | VernacDeclareScope _ - | VernacDelimiters _ | VernacBindScope _ - | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ - | VernacSyntacticDefinition _ - | VernacRequire _ | VernacImport _ | VernacInclude _ - | VernacDeclareMLModule _ - | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow) - | VernacProofMode pm -> VtProofMode pm - | VernacInstance ((name,_),_,_,props,_) -> - let program, refine = - Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts) - in - if program || (props <> None && not refine) then - VtSideff (idents_of_name name.CAst.v, VtLater) - else - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee, idents_of_name name.CAst.v) - (* Stm will install a new classifier to handle these *) - | VernacBack _ | VernacAbortAll - | VernacUndoTo _ | VernacUndo _ - | VernacResetName _ | VernacResetInitial - | VernacRestart -> VtMeta - (* What are these? *) - | VernacRestoreState _ - | VernacWriteState _ -> VtSideff ([], VtNow) - (* Plugins should classify their commands *) - | VernacExtend (s,l) -> - try Vernacextend.get_vernac_classifier s l - with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") - in - let static_control_classifier ({ CAst.v ; _ } as cmd) = - (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (* XXX why is Fail not always Query? *) - if Vernacprop.has_Fail cmd then - (match static_classifier ~atts:v.attrs v.expr with - | VtQuery | VtProofStep _ | VtSideff _ - | VtMeta as x -> x - | VtQed _ -> VtProofStep { proof_block_detection = None } - | VtStartProof _ | VtProofMode _ -> VtQuery) - else - static_classifier ~atts:v.attrs v.expr - - in - static_control_classifier e diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli deleted file mode 100644 index 61bf3a503a..0000000000 --- a/stm/vernac_classifier.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* string - -(** What does a vernacular do *) -val classify_vernac : Vernacexpr.vernac_control -> vernac_classification - -(** *) -val stm_allow_nested_proofs_option_name : string list diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index cd0dd5e9a6..007a3b05fc 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -45,3 +45,4 @@ ComArguments Vernacentries ComTactic Vernacinterp +Vernac_classifier diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml new file mode 100644 index 0000000000..ffae2866c0 --- /dev/null +++ b/vernac/vernac_classifier.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* "Later" + | VtNow -> "Now" + +let string_of_vernac_classification = function + | VtStartProof _ -> "StartProof" + | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w) + | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" + | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" + | VtQed VtDrop -> "Qed(drop)" + | VtProofStep { proof_block_detection } -> + "ProofStep " ^ Option.default "" proof_block_detection + | VtQuery -> "Query" + | VtMeta -> "Meta " + | VtProofMode _ -> "Proof Mode" + +let vtkeep_of_opaque = function + | Opaque -> VtKeepOpaque + | Transparent -> VtKeepDefined + +let idents_of_name : Names.Name.t -> Names.Id.t list = + function + | Names.Anonymous -> [] + | Names.Name n -> [n] + +let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] + +let options_affecting_stm_scheduling = + [ Attributes.universe_polymorphism_option_name; + stm_allow_nested_proofs_option_name; + Vernacinterp.proof_mode_opt_name; + Attributes.program_mode_option_name; + Proof_using.proof_using_opt_name; + ] + +let classify_vernac e = + let static_classifier ~atts e = match e with + (* Univ poly compatibility: we run it now, so that we can just + * look at Flags in stm.ml. Would be nicer to have the stm + * look at the entire dag to detect this option. *) + | VernacSetOption (_, l,_) + when CList.exists (CList.equal String.equal l) + options_affecting_stm_scheduling -> + VtSideff ([], VtNow) + (* Qed *) + | VernacAbort _ -> VtQed VtDrop + | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom) + | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)) + | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque) + (* Query *) + | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ + | VernacCheckMayEval _ -> VtQuery + (* ProofStep *) + | VernacProof _ + | VernacFocus _ | VernacUnfocus + | VernacSubproof _ + | VernacCheckGuard + | VernacUnfocused + | VernacSolveExistential _ -> + VtProofStep { proof_block_detection = None } + | VernacBullet _ -> + VtProofStep { proof_block_detection = Some "bullet" } + | VernacEndSubproof -> + VtProofStep { proof_block_detection = Some "curly" } + (* StartProof *) + | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> + VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) + + | VernacDefinition (_,({v=i},_),ProveBody _) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i) + | VernacStartTheoremProof (_,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids) + | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + else GuaranteesOpacity + in + let ids, open_proof = + List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} -> + id::l, b || body_def = None) ([],false) l in + if open_proof + then VtStartProof (guarantee,ids) + else VtSideff (ids, VtLater) + | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + else GuaranteesOpacity + in + let ids, open_proof = + List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } -> + id::l, b || body_def = None) ([],false) l in + if open_proof + then VtStartProof (guarantee,ids) + else VtSideff (ids, VtLater) + (* Sideff: apply to all open branches. usually run on master only *) + | VernacAssumption (_,_,l) -> + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in + VtSideff (ids, VtLater) + | VernacPrimitive ((id,_),_,_) -> + VtSideff ([id.CAst.v], VtLater) + | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) + | VernacInductive (_,l) -> + let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with + | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l + | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ + CList.map_filter (function + | AssumExpr({v=Names.Name n},_,_), _ -> Some n + | _ -> None) l) l in + VtSideff (List.flatten ids, VtLater) + | VernacScheme l -> + let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in + VtSideff (ids, VtLater) + | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater) + | VernacBeginSection {v=id} -> VtSideff ([id], VtLater) + | VernacUniverse _ | VernacConstraint _ + | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ + | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ + | VernacChdir _ + | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ + | VernacArguments _ + | VernacReserve _ + | VernacGeneralizable _ + | VernacSetOpacity _ | VernacSetStrategy _ + | VernacSetOption _ + | VernacAddOption _ | VernacRemoveOption _ + | VernacMemOption _ | VernacPrintOption _ + | VernacGlobalCheck _ + | VernacDeclareReduction _ + | VernacExistingClass _ | VernacExistingInstance _ + | VernacRegister _ + | VernacNameSectionHypSet _ + | VernacComments _ + | VernacDeclareInstance _ -> VtSideff ([], VtLater) + (* Who knows *) + | VernacLoad _ -> VtSideff ([], VtNow) + (* (Local) Notations have to disappear *) + | VernacEndSegment _ -> VtSideff ([], VtNow) + (* Modules with parameters have to be executed: can import notations *) + | VernacDeclareModule (exp,{v=id},bl,_) + | VernacDefineModule (exp,{v=id},bl,_,_) -> + VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow) + | VernacDeclareModuleType ({v=id},bl,_,_) -> + VtSideff ([id], if bl = [] then VtLater else VtNow) + (* These commands alter the parser *) + | VernacDeclareCustomEntry _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ + | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ + | VernacSyntaxExtension _ + | VernacSyntacticDefinition _ + | VernacRequire _ | VernacImport _ | VernacInclude _ + | VernacDeclareMLModule _ + | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow) + | VernacProofMode pm -> VtProofMode pm + | VernacInstance ((name,_),_,_,props,_) -> + let program, refine = + Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts) + in + if program || (props <> None && not refine) then + VtSideff (idents_of_name name.CAst.v, VtLater) + else + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v) + (* Stm will install a new classifier to handle these *) + | VernacBack _ | VernacAbortAll + | VernacUndoTo _ | VernacUndo _ + | VernacResetName _ | VernacResetInitial + | VernacRestart -> VtMeta + (* What are these? *) + | VernacRestoreState _ + | VernacWriteState _ -> VtSideff ([], VtNow) + (* Plugins should classify their commands *) + | VernacExtend (s,l) -> + try Vernacextend.get_vernac_classifier s l + with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") + in + let static_control_classifier ({ CAst.v ; _ } as cmd) = + (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (* XXX why is Fail not always Query? *) + if Vernacprop.has_Fail cmd then + (match static_classifier ~atts:v.attrs v.expr with + | VtQuery | VtProofStep _ | VtSideff _ + | VtMeta as x -> x + | VtQed _ -> VtProofStep { proof_block_detection = None } + | VtStartProof _ | VtProofMode _ -> VtQuery) + else + static_classifier ~atts:v.attrs v.expr + + in + static_control_classifier e diff --git a/vernac/vernac_classifier.mli b/vernac/vernac_classifier.mli new file mode 100644 index 0000000000..61bf3a503a --- /dev/null +++ b/vernac/vernac_classifier.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* string + +(** What does a vernacular do *) +val classify_vernac : Vernacexpr.vernac_control -> vernac_classification + +(** *) +val stm_allow_nested_proofs_option_name : string list -- cgit v1.2.3 From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Jan 2021 11:34:35 +0100 Subject: [sysinit] new component for system initialization This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml --- META.coq.in | 17 +- Makefile.common | 4 +- Makefile.dev | 3 +- dev/base_include | 1 - dev/dune | 1 + dev/tools/update-compat.py | 2 +- ide/coqide/idetop.ml | 16 +- stm/dune | 2 +- stm/stm.ml | 71 +----- stm/stm.mli | 29 +-- stm/stm.mllib | 1 + stm/stmargs.ml | 140 +++++++++++ stm/stmargs.mli | 13 + sysinit/coqargs.ml | 515 ++++++++++++++++++++++++++++++++++++++++ sysinit/coqargs.mli | 107 +++++++++ sysinit/coqloadpath.ml | 73 ++++++ sysinit/coqloadpath.mli | 16 ++ sysinit/dune | 8 + sysinit/sysinit.mllib | 3 + sysinit/usage.ml | 112 +++++++++ sysinit/usage.mli | 28 +++ toplevel/ccompile.ml | 19 +- toplevel/ccompile.mli | 2 +- toplevel/coqargs.ml | 580 --------------------------------------------- toplevel/coqargs.mli | 81 ------- toplevel/coqc.ml | 11 +- toplevel/coqinit.ml | 111 --------- toplevel/coqinit.mli | 22 -- toplevel/coqrc.ml | 45 ++++ toplevel/coqrc.mli | 11 + toplevel/coqtop.ml | 21 +- toplevel/coqtop.mli | 6 +- toplevel/toplevel.mllib | 4 +- toplevel/usage.ml | 113 --------- toplevel/usage.mli | 29 --- toplevel/workerLoop.ml | 7 +- 36 files changed, 1151 insertions(+), 1073 deletions(-) create mode 100644 stm/stmargs.ml create mode 100644 stm/stmargs.mli create mode 100644 sysinit/coqargs.ml create mode 100644 sysinit/coqargs.mli create mode 100644 sysinit/coqloadpath.ml create mode 100644 sysinit/coqloadpath.mli create mode 100644 sysinit/dune create mode 100644 sysinit/sysinit.mllib create mode 100644 sysinit/usage.ml create mode 100644 sysinit/usage.mli delete mode 100644 toplevel/coqargs.ml delete mode 100644 toplevel/coqargs.mli delete mode 100644 toplevel/coqinit.ml delete mode 100644 toplevel/coqinit.mli create mode 100644 toplevel/coqrc.ml create mode 100644 toplevel/coqrc.mli delete mode 100644 toplevel/usage.ml delete mode 100644 toplevel/usage.mli diff --git a/META.coq.in b/META.coq.in index 68ab0733ee..7a9818da08 100644 --- a/META.coq.in +++ b/META.coq.in @@ -207,10 +207,10 @@ package "vernac" ( package "stm" ( - description = "Coq State Transactional Machine" + description = "Coq State Transaction Machine" version = "8.14" - requires = "coq.vernac" + requires = "coq.sysinit" directory = "stm" archive(byte) = "stm.cma" @@ -218,6 +218,19 @@ package "stm" ( ) +package "sysinit" ( + + description = "Coq initialization" + version = "8.14" + + requires = "coq.vernac" + directory = "sysinit" + + archive(byte) = "sysinit.cma" + archive(native) = "sysinit.cmxa" + +) + package "toplevel" ( description = "Coq Toplevel" diff --git a/Makefile.common b/Makefile.common index 82d9b89c4f..415454df79 100644 --- a/Makefile.common +++ b/Makefile.common @@ -99,7 +99,7 @@ CORESRCDIRS:=\ coqpp \ config clib lib kernel kernel/byterun library \ engine pretyping interp proofs gramlib/.pack parsing printing \ - tactics vernac stm toplevel + tactics vernac stm sysinit toplevel PLUGINDIRS:=\ omega micromega \ @@ -132,7 +132,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ gramlib/.pack/gramlib.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ - stm/stm.cma toplevel/toplevel.cma + sysinit/sysinit.cma stm/stm.cma toplevel/toplevel.cma ########################################################################### # plugins object files diff --git a/Makefile.dev b/Makefile.dev index 5825a884c2..cfb02b6d80 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -91,10 +91,11 @@ interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma stm: stm/stm.cma +sysinit: sysinit/sysinit.cma toplevel: toplevel/toplevel.cma .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine stm toplevel +.PHONY: engine stm sysinit toplevel ###################### ### 3) theories files diff --git a/dev/base_include b/dev/base_include index daee2d97c5..f375a867bc 100644 --- a/dev/base_include +++ b/dev/base_include @@ -134,7 +134,6 @@ open ComDefinition open Indschemes open Ind_tables open Auto_ind_decl -open Coqinit open Coqtop open Himsg open Metasyntax diff --git a/dev/dune b/dev/dune index a6d88c94d2..ae801f9e83 100644 --- a/dev/dune +++ b/dev/dune @@ -34,6 +34,7 @@ %{lib:coq.tactics:tactics.cma} %{lib:coq.vernac:vernac.cma} %{lib:coq.stm:stm.cma} + %{lib:coq.sysinit:sysinit.cma} %{lib:coq.toplevel:toplevel.cma} %{lib:coq.plugins.ltac:ltac_plugin.cma} %{lib:coq.top_printers:top_printers.cmi} diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 666fb6cc91..a14b98c73c 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -64,7 +64,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 RELEASE_NUMBER_OF_OLD_VERSIONS = 2 MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' -COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') +COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 528e2a756b..ed0eb8f34b 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -513,7 +513,7 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop run_mode ~opts:_ state = +let loop (run_mode,_) ~opts:_ state = match run_mode with | Coqtop.Batch -> exit 0 | Coqtop.Interactive -> @@ -582,23 +582,19 @@ coqidetop specific options:\n\ let islave_parse ~opts extra_args = let open Coqtop in - let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let (run_mode, stm_opts), extra_args = coqtop_toplevel.parse_extra ~opts extra_args in let extra_args = parse extra_args in (* One of the role of coqidetop is to find the name of buffers to open *) (* in the command line; Coqide is waiting these names on stdout *) (* (see filter_coq_opts in coq.ml), so we send them now *) print_string (String.concat "\n" extra_args); - run_mode, [] + (run_mode, stm_opts), [] -let islave_init run_mode ~opts = +let islave_init (run_mode, stm_opts) ~opts = if run_mode = Coqtop.Batch then Flags.quiet := true; - Coqtop.init_toploop opts + Coqtop.init_toploop opts stm_opts -let islave_default_opts = - Coqargs.{ default with - config = { default.config with - stm_flags = { default.config.stm_flags with - Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}} +let islave_default_opts = Coqargs.default let () = let open Coqtop in diff --git a/stm/dune b/stm/dune index c369bd00fb..27d561334e 100644 --- a/stm/dune +++ b/stm/dune @@ -3,4 +3,4 @@ (synopsis "Coq's Document Manager and Proof Checking Scheduler") (public_name coq.stm) (wrapped false) - (libraries vernac)) + (libraries sysinit)) diff --git a/stm/stm.ml b/stm/stm.ml index 27f2b6fc5c..f4e370e7bc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -297,13 +297,11 @@ end (* }}} *) (*************************** THE DOCUMENT *************************************) (******************************************************************************) -type interactive_top = TopLogical of DirPath.t | TopPhysical of string - (* The main document type associated to a VCS *) type stm_doc_type = | VoDoc of string | VioDoc of string - | Interactive of interactive_top + | Interactive of Coqargs.interactive_top (* Dummy until we land the functional interp patch + fixed start_library *) type doc = int @@ -517,7 +515,7 @@ end = struct (* {{{ *) type vcs = (branch_type, transaction, vcs state_info, box) t let vcs : vcs ref = ref (empty Stateid.dummy) - let doc_type = ref (Interactive (TopLogical (Names.DirPath.make []))) + let doc_type = ref (Interactive (Coqargs.TopLogical (Names.DirPath.make []))) let ldir = ref Names.DirPath.empty let init dt id ps = @@ -2308,23 +2306,6 @@ end (* }}} *) (** STM initialization options: *) -type option_command = - | OptionSet of string option - | OptionAppend of string - | OptionUnset - -type injection_command = - | OptionInjection of (Goptions.option_name * option_command) - (** Set flags or options before the initial state is ready. *) - | RequireInjection of (string * string option * bool option) - (** Require libraries before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) - (* -load-vernac-source interleaving is not supported yet *) - (* | LoadInjection of (string * bool) *) - type stm_init_options = { doc_type : stm_doc_type (** The STM does set some internal flags differently depending on @@ -2338,7 +2319,7 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; injections : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -2355,6 +2336,10 @@ let doc_type_module_name (std : stm_doc_type) = | Interactive mn -> Names.DirPath.to_string mn *) +let init_process stm_flags = + Spawned.init_channels (); + CoqworkmgrApi.(init stm_flags.AsyncOpts.async_proofs_worker_priority) + let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers; @@ -2379,44 +2364,10 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - let interp_set_option opt v old = - let open Goptions in - let err expect = - let opt = String.concat " " opt in - let got = v in (* avoid colliding with Pp.v *) - CErrors.user_err - Pp.(str "-set: " ++ str opt ++ - str" expects " ++ str expect ++ - str" but got " ++ str got) - in - match old with - | BoolValue _ -> - let v = match String.trim v with - | "true" -> true - | "false" | "" -> false - | _ -> err "a boolean" - in - BoolValue v - | IntValue _ -> - let v = String.trim v in - let v = match int_of_string_opt v with - | Some _ as v -> v - | None -> if v = "" then None else err "an int" - in - IntValue v - | StringValue _ -> StringValue v - | StringOptValue _ -> StringOptValue (Some v) in - - let set_option = let open Goptions in function - | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt - | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true - | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v - | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in - let handle_injection = function - | RequireInjection r -> require_file r + | Coqargs.RequireInjection r -> require_file r (* | LoadInjection l -> *) - | OptionInjection o -> set_option o in + | Coqargs.OptionInjection o -> Coqargs.set_option o in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2437,8 +2388,8 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = begin match doc_type with | Interactive ln -> let dp = match ln with - | TopLogical dp -> dp - | TopPhysical f -> dirpath_of_file f + | Coqargs.TopLogical dp -> dp + | Coqargs.TopPhysical f -> dirpath_of_file f in Declaremods.start_library dp diff --git a/stm/stm.mli b/stm/stm.mli index e0c33a309b..dddd63cb52 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -42,32 +42,13 @@ module AsyncOpts : sig end -type interactive_top = TopLogical of DirPath.t | TopPhysical of string - (** The STM document type [stm_doc_type] determines some properties such as what uncompleted proofs are allowed and what gets recorded to aux files. *) type stm_doc_type = | VoDoc of string (* file path *) | VioDoc of string (* file path *) - | Interactive of interactive_top (* module path *) - -type option_command = - | OptionSet of string option - | OptionAppend of string - | OptionUnset - -type injection_command = - | OptionInjection of (Goptions.option_name * option_command) - (** Set flags or options before the initial state is ready. *) - | RequireInjection of (string * string option * bool option) - (** Require libraries before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) - (* -load-vernac-source interleaving is not supported yet *) - (* | LoadInjection of (string * bool) *) + | Interactive of Coqargs.interactive_top (* module path *) (** STM initialization options: *) type stm_init_options = @@ -83,7 +64,7 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; injections : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -94,8 +75,10 @@ type stm_init_options = (** The type of a STM document *) type doc -(** [init_core] performs some low-level initialization; should go away - in future releases. *) +(** [init_process] performs some low-level initialization, call early *) +val init_process : AsyncOpts.stm_opt -> unit + +(** [init_core] snapshorts the initial system state *) val init_core : unit -> unit (** [new_doc opt] Creates a new document with options [opt] *) diff --git a/stm/stm.mllib b/stm/stm.mllib index 49e7195e27..a77e0c79e7 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -7,5 +7,6 @@ CoqworkmgrApi AsyncTaskQueue Partac Stm +Stmargs ProofBlockDelimiter Vio_checking diff --git a/stm/stmargs.ml b/stm/stmargs.ml new file mode 100644 index 0000000000..609d4f42e9 --- /dev/null +++ b/stm/stmargs.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* "master"); + Flags.async_proofs_worker_id := s + +let get_host_port opt s = + match String.split_on_char ':' s with + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) + +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (String.split_on_char ',' s) + +let get_priority opt s = + try CoqworkmgrApi.priority_of_string s + with Invalid_argument _ -> + Coqargs.error_wrong_arg ("Error: low/high expected after "^opt) + +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy + | _ -> + Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt) + +let get_cache opt = function + | "force" -> Some Stm.AsyncOpts.Force + | _ -> + Coqargs.error_wrong_arg ("Error: force expected after "^opt) + +let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> Coqargs.error_missing_arg opt + in + let noval = begin match opt with + + |"-async-proofs" -> + { oval with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + } + |"-async-proofs-j" -> + { oval with + Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ())) + } + |"-async-proofs-cache" -> + { oval with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + } + + |"-async-proofs-tac-j" -> + let j = Coqargs.get_int ~opt (next ()) in + if j <= 0 then begin + Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") + end; + { oval with + Stm.AsyncOpts.async_proofs_n_tacworkers = j + } + + |"-async-proofs-worker-priority" -> + { oval with + Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ()) + } + + |"-async-proofs-private-flags" -> + { oval with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + } + + |"-async-proofs-tactic-error-resilience" -> + { oval with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) + } + + |"-async-proofs-command-error-resilience" -> + { oval with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ()) + } + + |"-async-proofs-delegation-threshold" -> + { oval with + Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ()) + } + + |"-worker-id" -> set_worker_id opt (next ()); oval + + |"-main-channel" -> + Spawned.main_channel := get_host_port opt (next()); oval + + |"-control-channel" -> + Spawned.control_channel := get_host_port opt (next()); oval + + (* Options with zero arg *) + |"-async-queries-always-delegate" + |"-async-proofs-always-delegate" + |"-async-proofs-never-reopen-branch" -> + { oval with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true + } + |"-stm-debug" -> Stm.stm_debug := true; oval + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init + with any -> fatal_error any + +let usage = "\ +\n -stm-debug STM debug mode (will trace every transaction)\ +" \ No newline at end of file diff --git a/stm/stmargs.mli b/stm/stmargs.mli new file mode 100644 index 0000000000..f760afdc98 --- /dev/null +++ b/stm/stmargs.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* string list -> Stm.AsyncOpts.stm_opt * string list + +val usage : string diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml new file mode 100644 index 0000000000..930c3b135f --- /dev/null +++ b/sysinit/coqargs.ml @@ -0,0 +1,515 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* { opts with config = { opts.config with color = `ON }} + | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} + | "auto" -> { opts with config = { opts.config with color = `AUTO }} + | _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") + +let set_query opts q = + { opts with main = match opts.main with + | Run -> Queries (default_queries@[q]) + | Queries queries -> Queries (queries@[q]) + } + +let warn_deprecated_sprop_cumul = + CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" + (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") + +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") + +let set_inputstate opts s = + warn_deprecated_inputstate (); + { opts with pre = { opts.pre with inputstate = Some s }} + +(******************************************************************************) +(* Parsing helpers *) +(******************************************************************************) +let get_bool ~opt = function + | "yes" | "on" -> true + | "no" | "off" -> false + | _ -> + error_wrong_arg ("Error: yes/no expected after option "^opt) + +let get_int ~opt n = + try int_of_string n + with Failure _ -> + error_wrong_arg ("Error: integer expected after option "^opt) +let get_int_opt ~opt n = + if n = "" then None + else Some (get_int ~opt n) + +let get_float ~opt n = + try float_of_string n + with Failure _ -> + error_wrong_arg ("Error: float expected after option "^opt) + +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + Filename.(List.fold_left concat (dirname s) + [ !Nativelib.output_dir + ; Library.native_name_from_filename s + ]) + with _ -> "" + +let interp_set_option opt v old = + let open Goptions in + let opt = String.concat " " opt in + match old with + | BoolValue _ -> BoolValue (get_bool ~opt v) + | IntValue _ -> IntValue (get_int_opt ~opt v) + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) + +let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v + | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v + +let get_compat_file = function + | "8.14" -> "Coq.Compat.Coq814" + | "8.13" -> "Coq.Compat.Coq813" + | "8.12" -> "Coq.Compat.Coq812" + | "8.11" -> "Coq.Compat.Coq811" + | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + +let to_opt_key = Str.(split (regexp " +")) + +let parse_option_set opt = + match String.index_opt opt '=' with + | None -> to_opt_key opt, None + | Some eqi -> + let len = String.length opt in + let v = String.sub opt (eqi+1) (len - eqi - 1) in + to_opt_key (String.sub opt 0 eqi), Some v + +let warn_no_native_compiler = + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + Pp.(fun s -> strbrk "Native compiler is disabled," ++ + strbrk " -native-compiler " ++ strbrk s ++ + strbrk " option ignored.") + +let get_native_compiler s = + (* We use two boolean flags because the four states make sense, even if + only three are accessible to the user at the moment. The selection of the + produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by + a separate flag, and the "ondemand" value removed. Once this is done, use + [get_bool] here. *) + let n = match s with + | ("yes" | "on") -> NativeOn {ondemand=false} + | "ondemand" -> NativeOn {ondemand=true} + | ("no" | "off") -> NativeOff + | _ -> + error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in + if Coq_config.native_compiler = NativeOff && n <> NativeOff then + let () = warn_no_native_compiler s in + NativeOff + else + n + +(* Main parsing routine *) +(*s Parsing of the command line *) + +let parse_args ~help ~init arglist : t * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + let noval = begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: rem -> + args := rem; + add_ml_include oval d + | [] -> error_missing_arg opt + end + |"-Q" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p false + | _ -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p true + | _ -> error_missing_arg opt + end + + (* Options with one arg *) + |"-coqlib" -> + { oval with config = { oval.config with coqlib = Some (next ()) + }} + + |"-compat" -> + add_vo_require oval (get_compat_file (next ())) None (Some false) + + |"-exclude-dir" -> + System.exclude_directory (next ()); oval + + |"-init-file" -> + { oval with config = { oval.config with rcfile = Some (next ()); }} + + |"-inputstate"|"-is" -> + set_inputstate oval (next ()) + + |"-load-vernac-object" -> + add_vo_require oval (next ()) None None + + |"-load-vernac-source"|"-l" -> + add_load_vernacular oval false (next ()) + + |"-load-vernac-source-verbose"|"-lv" -> + add_load_vernacular oval true (next ()) + + |"-mangle-names" -> + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval + + |"-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 ()); + oval + + |"-rfrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) None + + |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) + + |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) + + |"-require-import-from" | "-rifrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some false) + + |"-require-export-from" | "-refrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some true) + + |"-top" -> + let topname = Libnames.dirpath_of_string (next ()) in + if Names.DirPath.is_empty topname then + CErrors.user_err Pp.(str "Need a non empty toplevel module name"); + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopLogical topname }}} + + |"-topfile" -> + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopPhysical (next()) }}} + + |"-w" | "-W" -> + let w = next () in + if w = "none" then add_set_option oval ["Warnings"] (OptionSet(Some w)) + else add_set_option oval ["Warnings"] (OptionAppend w) + + |"-bytecode-compiler" -> + { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} + + |"-native-compiler" -> + let native_compiler = get_native_compiler (next ()) in + { oval with config = { oval.config with native_compiler }} + + | "-set" -> + let opt, v = parse_option_set @@ next() in + add_set_option oval opt (OptionSet v) + + | "-unset" -> + add_set_option oval (to_opt_key @@ next ()) OptionUnset + + |"-native-output-dir" -> + let native_output_dir = next () in + { oval with config = { oval.config with native_output_dir } } + + |"-nI" -> + let include_dir = next () in + { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } } + + (* Options with zero arg *) + |"-test-mode" -> Vernacinterp.test_mode := true; oval + |"-beautify" -> Flags.beautify := true; oval + |"-bt" -> Exninfo.record_backtrace true; oval + |"-color" -> set_color oval (next ()) + |"-config"|"--config" -> set_query oval PrintConfig + |"-debug" -> set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval + |"-diffs" -> + add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) + |"-emacs" -> set_emacs oval + |"-impredicative-set" -> + set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval + |"-allow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) + |"-disallow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset + |"-sprop-cumulative" -> + warn_deprecated_sprop_cumul(); + add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) + |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval + |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} + |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} + |"-boot" -> { oval with pre = { oval.pre with boot = true }} + |"-output-context" -> { oval with post = { oval.post with output_context = true }} + |"-profile-ltac" -> Flags.profile_ltac := true; oval + |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} + |"-quiet"|"-silent" -> + Flags.quiet := true; + Flags.make_warn false; + oval + |"-list-tags" -> set_query oval PrintTags + |"-time" -> { oval with config = { oval.config with time = true }} + |"-type-in-type" -> set_type_in_type (); oval + |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) + |"-where" -> set_query oval PrintWhere + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) + |"-v"|"--version" -> set_query oval PrintVersion + |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion + + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init + with any -> fatal_error any + +(* We need to reverse a few lists *) +let parse_args ~help ~init args = + let opts, extra = parse_args ~help ~init args in + let opts = + { opts with + pre = { opts.pre with + ml_includes = List.rev opts.pre.ml_includes + ; vo_includes = List.rev opts.pre.vo_includes + ; load_vernacular_list = List.rev opts.pre.load_vernacular_list + ; injections = List.rev opts.pre.injections + } + } in + opts, extra + +(******************************************************************************) +(* Startup LoadPath and Modules *) +(******************************************************************************) +(* prelude_data == From Coq Require Import Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some false + +let injection_commands opts = + if opts.pre.load_init then RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections + +let build_load_path opts = + let ml_path, vo_path = + if opts.pre.boot then [],[] + else + let coqlib = Envars.coqlib () in + Coqloadpath.init_load_path ~coqlib in + ml_path @ opts.pre.ml_includes , + vo_path @ opts.pre.vo_includes diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli new file mode 100644 index 0000000000..894e0f2ef3 --- /dev/null +++ b/sysinit/coqargs.mli @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* init:t -> string list -> t * string list + +val injection_commands : t -> injection_command list +val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list + +(* Common utilities *) + +val get_int : opt:string -> string -> int +val get_int_opt : opt:string -> string -> int option +val get_bool : opt:string -> string -> bool +val get_float : opt:string -> string -> float +val error_missing_arg : string -> 'a +val error_wrong_arg : string -> 'a + +val set_option : Goptions.option_name * option_command -> unit \ No newline at end of file diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml new file mode 100644 index 0000000000..8635345e00 --- /dev/null +++ b/sysinit/coqloadpath.ml @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* List.map fst in + let vo_path = + { unix_path + ; coq_path = Libnames.default_root_prefix + ; has_ml = false + ; implicit = false + ; recursive = true + } in + ml_path, [vo_path] + else [], [] + +(* LoadPath for Coq user libraries *) +let init_load_path ~coqlib = + + let open Loadpath in + let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in + let coqpath = Envars.coqpath in + let coq_path = Names.DirPath.make [Libnames.coq_root] in + + (* ML includes *) + let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in + + let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in + + let misc_ml, misc_vo = + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in + + let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in + let vo_loadpath = + (* current directory (not recursively!) *) + [ { unix_path = "." + ; coq_path = Libnames.default_root_prefix + ; implicit = false + ; has_ml = true + ; recursive = false + } ] @ + + (* then standard library *) + [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ + + (* then user-contrib *) + contrib_vo @ + + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) + List.concat misc_vo + in + ml_loadpath, vo_loadpath diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli new file mode 100644 index 0000000000..d853e9ea54 --- /dev/null +++ b/sysinit/coqloadpath.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* CUnix.physical_path list * Loadpath.vo_path list diff --git a/sysinit/dune b/sysinit/dune new file mode 100644 index 0000000000..6146aa60d0 --- /dev/null +++ b/sysinit/dune @@ -0,0 +1,8 @@ +(library + (name sysinit) + (public_name coq.sysinit) + (synopsis "Coq's initialization") + (wrapped false) + (libraries coq.vernac) + (modules coqloadpath coqargs usage) + ) diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib new file mode 100644 index 0000000000..9d35a931bc --- /dev/null +++ b/sysinit/sysinit.mllib @@ -0,0 +1,3 @@ +Usage +Coqloadpath +Coqargs diff --git a/sysinit/usage.ml b/sysinit/usage.ml new file mode 100644 index 0000000000..1831a3f9b2 --- /dev/null +++ b/sysinit/usage.ml @@ -0,0 +1,112 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* set the output directory for native objects\ +\n -nI dir OCaml include directories for the native compiler (default if not set) \ +\n -h, -help, --help print this list of options\ +\n" + +(* print the usage *) + +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +let print_usage co { executable_name; extra_args; extra_options } = + print_usage_common co ("Usage: " ^ executable_name ^ " " ^ extra_args ^ "\n\n"); + output_string co extra_options diff --git a/sysinit/usage.mli b/sysinit/usage.mli new file mode 100644 index 0000000000..2d1a8e94cc --- /dev/null +++ b/sysinit/usage.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* unit +val machine_readable_version : unit -> unit + +(** {6 extra arguments or options to print when asking usage for a + given executable. } *) + +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +(** {6 Prints the generic part and specific part of usage for a + given executable. } *) + +val print_usage : out_channel -> specific_usage -> unit diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index b75a4199ea..4747abceb5 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -24,7 +24,7 @@ let fatal_error msg = let load_init_file opts ~state = if opts.pre.load_rcfile then Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) () + Coqrc.load_rcfile ~rcfile:opts.config.rcfile ~state) () else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -93,7 +93,7 @@ let create_empty_file filename = close_out f (* Compile a vernac file *) -let compile opts copts ~echo ~f_in ~f_out = +let compile opts stm_options copts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in @@ -106,7 +106,6 @@ let compile opts copts ~echo ~f_in ~f_out = in let ml_load_path, vo_load_path = build_load_path opts in let injections = injection_commands opts in - let stm_options = opts.config.stm_flags in let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand in @@ -209,22 +208,22 @@ let compile opts copts ~echo ~f_in ~f_out = dump_empty_vos(); create_empty_file (long_f_dot_out ^ "k") -let compile opts copts ~echo ~f_in ~f_out = +let compile opts stm_opts copts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts copts ~echo ~f_in ~f_out; + compile opts stm_opts copts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts copts (f_in, echo) = +let compile_file opts stm_opts copts (f_in, echo) = let f_out = copts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts copts ~echo ~f_in ~f_out) f_in + (fun f_in -> compile opts stm_opts copts ~echo ~f_in ~f_out) f_in else - compile opts copts ~echo ~f_in ~f_out + compile opts stm_opts copts ~echo ~f_in ~f_out -let compile_files opts copts = +let compile_files (opts, stm_opts) copts = let compile_list = copts.compile_list in - List.iter (compile_file opts copts) compile_list + List.iter (compile_file opts stm_opts copts) compile_list (******************************************************************************) (* VIO Dispatching *) diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 8c154488d0..1b670a8edc 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -13,7 +13,7 @@ val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t (** [compile_files opts] compile files specified in [opts] *) -val compile_files : Coqargs.t -> Coqcargs.t -> unit +val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml deleted file mode 100644 index c114c43e26..0000000000 --- a/toplevel/coqargs.ml +++ /dev/null @@ -1,580 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* "master"); - Flags.async_proofs_worker_id := s - -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } - -(******************************************************************************) - -type color = [`ON | `AUTO | `EMACS | `OFF] - -type native_compiler = Coq_config.native_compiler = - NativeOff | NativeOn of { ondemand : bool } - -type coqargs_logic_config = { - impredicative_set : Declarations.set_predicativity; - indices_matter : bool; - toplevel_name : Stm.interactive_top; -} - -type coqargs_config = { - logic : coqargs_logic_config; - rcfile : string option; - coqlib : string option; - color : color; - enable_VM : bool; - native_compiler : native_compiler; - native_output_dir : CUnix.physical_path; - native_include_dirs : CUnix.physical_path list; - stm_flags : Stm.AsyncOpts.stm_opt; - debug : bool; - time : bool; - print_emacs : bool; -} - -type coqargs_pre = { - boot : bool; - load_init : bool; - load_rcfile : bool; - - ml_includes : string list; - vo_includes : Loadpath.vo_path list; - - load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; - - inputstate : string option; -} - -type coqargs_query = - | PrintTags | PrintWhere | PrintConfig - | PrintVersion | PrintMachineReadableVersion - | PrintHelp of Usage.specific_usage - -type coqargs_main = - | Queries of coqargs_query list - | Run - -type coqargs_post = { - memory_stat : bool; - output_context : bool; -} - -type t = { - config : coqargs_config; - pre : coqargs_pre; - main : coqargs_main; - post : coqargs_post; -} - -let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) - -let default_native = Coq_config.native_compiler - -let default_logic_config = { - impredicative_set = Declarations.PredicativeSet; - indices_matter = false; - toplevel_name = Stm.TopLogical default_toplevel; -} - -let default_config = { - logic = default_logic_config; - rcfile = None; - coqlib = None; - color = `AUTO; - enable_VM = true; - native_compiler = default_native; - native_output_dir = ".coq-native"; - native_include_dirs = []; - stm_flags = Stm.AsyncOpts.default_opts; - debug = false; - time = false; - print_emacs = false; - - (* Quiet / verbosity options should be here *) -} - -let default_pre = { - boot = false; - load_init = true; - load_rcfile = true; - ml_includes = []; - vo_includes = []; - load_vernacular_list = []; - injections = []; - inputstate = None; -} - -let default_queries = [] - -let default_post = { - memory_stat = false; - output_context = false; -} - -let default = { - config = default_config; - pre = default_pre; - main = Run; - post = default_post; -} - -(******************************************************************************) -(* Functional arguments *) -(******************************************************************************) -let add_ml_include opts s = - { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }} - -let add_vo_include opts unix_path coq_path implicit = - let open Loadpath in - let coq_path = Libnames.dirpath_of_string coq_path in - { opts with pre = { opts.pre with vo_includes = { - unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }} - -let add_vo_require opts d p export = - { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }} - -let add_load_vernacular opts verb s = - { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} - -let add_set_option opts opt_name value = - { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }} - -(** Options for proof general *) -let set_emacs opts = - Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; - { opts with config = { opts.config with color = `EMACS; print_emacs = true }} - -let set_logic f oval = - { oval with config = { oval.config with logic = f oval.config.logic }} - -let set_color opts = function - | "yes" | "on" -> { opts with config = { opts.config with color = `ON }} - | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} - | "auto" -> { opts with config = { opts.config with color = `AUTO }} - | _ -> - error_wrong_arg ("Error: on/off/auto expected after option color") - -let set_query opts q = - { opts with main = match opts.main with - | Run -> Queries (default_queries@[q]) - | Queries queries -> Queries (queries@[q]) - } - -let warn_deprecated_sprop_cumul = - CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" - (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") - -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") - -let set_inputstate opts s = - warn_deprecated_inputstate (); - { opts with pre = { opts.pre with inputstate = Some s }} - -(******************************************************************************) -(* Parsing helpers *) -(******************************************************************************) -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> - error_wrong_arg ("Error: yes/no expected after option "^opt) - -let get_int opt n = - try int_of_string n - with Failure _ -> - error_wrong_arg ("Error: integer expected after option "^opt) - -let get_float opt n = - try float_of_string n - with Failure _ -> - error_wrong_arg ("Error: float expected after option "^opt) - -let get_host_port opt s = - match String.split_on_char ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (String.split_on_char ',' s) - -let get_priority opt s = - try CoqworkmgrApi.priority_of_string s - with Invalid_argument _ -> - error_wrong_arg ("Error: low/high expected after "^opt) - -let get_async_proofs_mode opt = let open Stm.AsyncOpts in function - | "no" | "off" -> APoff - | "yes" | "on" -> APon - | "lazy" -> APonLazy - | _ -> - error_wrong_arg ("Error: on/off/lazy expected after "^opt) - -let get_cache opt = function - | "force" -> Some Stm.AsyncOpts.Force - | _ -> - error_wrong_arg ("Error: force expected after "^opt) - - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - Filename.(List.fold_left concat (dirname s) - [ !Nativelib.output_dir - ; Library.native_name_from_filename s - ]) - with _ -> "" - -let get_compat_file = function - | "8.14" -> "Coq.Compat.Coq814" - | "8.13" -> "Coq.Compat.Coq813" - | "8.12" -> "Coq.Compat.Coq812" - | "8.11" -> "Coq.Compat.Coq811" - | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - CErrors.user_err ~hdr:"get_compat_file" - Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> - CErrors.user_err ~hdr:"get_compat_file" - Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") - -let to_opt_key = Str.(split (regexp " +")) - -let parse_option_set opt = - match String.index_opt opt '=' with - | None -> to_opt_key opt, None - | Some eqi -> - let len = String.length opt in - let v = String.sub opt (eqi+1) (len - eqi - 1) in - to_opt_key (String.sub opt 0 eqi), Some v - -let warn_no_native_compiler = - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - Pp.(fun s -> strbrk "Native compiler is disabled," ++ - strbrk " -native-compiler " ++ strbrk s ++ - strbrk " option ignored.") - -let get_native_compiler s = - (* We use two boolean flags because the four states make sense, even if - only three are accessible to the user at the moment. The selection of the - produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by - a separate flag, and the "ondemand" value removed. Once this is done, use - [get_bool] here. *) - let n = match s with - | ("yes" | "on") -> NativeOn {ondemand=false} - | "ondemand" -> NativeOn {ondemand=true} - | ("no" | "off") -> NativeOff - | _ -> - error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in - if Coq_config.native_compiler = NativeOff && n <> NativeOff then - let () = warn_no_native_compiler s in - NativeOff - else - n - -(* Main parsing routine *) -(*s Parsing of the command line *) - -let parse_args ~help ~init arglist : t * string list = - let args = ref arglist in - let extras = ref [] in - let rec parse oval = match !args with - | [] -> - (oval, List.rev !extras) - | opt :: rem -> - args := rem; - let next () = match !args with - | x::rem -> args := rem; x - | [] -> error_missing_arg opt - in - let noval = begin match opt with - - (* Complex options with many args *) - |"-I"|"-include" -> - begin match rem with - | d :: rem -> - args := rem; - add_ml_include oval d - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> - args := rem; - add_vo_include oval d p false - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> - args := rem; - add_vo_include oval d p true - | _ -> error_missing_arg opt - end - - (* Options with one arg *) - |"-coqlib" -> - { oval with config = { oval.config with coqlib = Some (next ()) - }} - - |"-async-proofs" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) - }}} - |"-async-proofs-j" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) - }}} - |"-async-proofs-cache" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) - }}} - - |"-async-proofs-tac-j" -> - let j = get_int opt (next ()) in - if j <= 0 then begin - error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") - end; - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_n_tacworkers = j - }}} - - |"-async-proofs-worker-priority" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ()) - }}} - - |"-async-proofs-private-flags" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - }}} - - |"-async-proofs-tactic-error-resilience" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) - }}} - - |"-async-proofs-command-error-resilience" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) - }}} - - |"-async-proofs-delegation-threshold" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) - }}} - - |"-worker-id" -> set_worker_id opt (next ()); oval - - |"-compat" -> - add_vo_require oval (get_compat_file (next ())) None (Some false) - - |"-exclude-dir" -> - System.exclude_directory (next ()); oval - - |"-init-file" -> - { oval with config = { oval.config with rcfile = Some (next ()); }} - - |"-inputstate"|"-is" -> - set_inputstate oval (next ()) - - |"-load-vernac-object" -> - add_vo_require oval (next ()) None None - - |"-load-vernac-source"|"-l" -> - add_load_vernacular oval false (next ()) - - |"-load-vernac-source-verbose"|"-lv" -> - add_load_vernacular oval true (next ()) - - |"-mangle-names" -> - Goptions.set_bool_option_value ["Mangle"; "Names"] true; - Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); - oval - - |"-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 ()); - oval - - |"-rfrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) None - - |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) - - |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) - - |"-require-import-from" | "-rifrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) (Some false) - - |"-require-export-from" | "-refrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) (Some true) - - |"-top" -> - let topname = Libnames.dirpath_of_string (next ()) in - if Names.DirPath.is_empty topname then - CErrors.user_err Pp.(str "Need a non empty toplevel module name"); - { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}} - - |"-topfile" -> - { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}} - - |"-main-channel" -> - Spawned.main_channel := get_host_port opt (next()); oval - - |"-control-channel" -> - Spawned.control_channel := get_host_port opt (next()); oval - - |"-w" | "-W" -> - let w = next () in - if w = "none" then add_set_option oval ["Warnings"] (Stm.OptionSet(Some w)) - else add_set_option oval ["Warnings"] (Stm.OptionAppend w) - - |"-bytecode-compiler" -> - { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }} - - |"-native-compiler" -> - let native_compiler = get_native_compiler (next ()) in - { oval with config = { oval.config with native_compiler }} - - | "-set" -> - let opt, v = parse_option_set @@ next() in - add_set_option oval opt (Stm.OptionSet v) - - | "-unset" -> - add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset - - |"-native-output-dir" -> - let native_output_dir = next () in - { oval with config = { oval.config with native_output_dir } } - - |"-nI" -> - let include_dir = next () in - { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } } - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-never-reopen-branch" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_never_reopen_branch = true - }}} - |"-test-mode" -> Vernacinterp.test_mode := true; oval - |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Exninfo.record_backtrace true; oval - |"-color" -> set_color oval (next ()) - |"-config"|"--config" -> set_query oval PrintConfig - |"-debug" -> Coqinit.set_debug (); oval - |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval - |"-diffs" -> - add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) - |"-stm-debug" -> Stm.stm_debug := true; oval - |"-emacs" -> set_emacs oval - |"-impredicative-set" -> - set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval - |"-allow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None) - |"-disallow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset - |"-sprop-cumulative" -> - warn_deprecated_sprop_cumul(); - add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None) - |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval - |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} - |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} - |"-boot" -> { oval with pre = { oval.pre with boot = true }} - |"-output-context" -> { oval with post = { oval.post with output_context = true }} - |"-profile-ltac" -> Flags.profile_ltac := true; oval - |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} - |"-quiet"|"-silent" -> - Flags.quiet := true; - Flags.make_warn false; - oval - |"-list-tags" -> set_query oval PrintTags - |"-time" -> { oval with config = { oval.config with time = true }} - |"-type-in-type" -> set_type_in_type (); oval - |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) - |"-where" -> set_query oval PrintWhere - |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) - |"-v"|"--version" -> set_query oval PrintVersion - |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion - - (* Unknown option *) - | s -> - extras := s :: !extras; - oval - end in - parse noval - in - try - parse init - with any -> fatal_error any - -(* We need to reverse a few lists *) -let parse_args ~help ~init args = - let opts, extra = parse_args ~help ~init args in - let opts = - { opts with - pre = { opts.pre with - ml_includes = List.rev opts.pre.ml_includes - ; vo_includes = List.rev opts.pre.vo_includes - ; load_vernacular_list = List.rev opts.pre.load_vernacular_list - ; injections = List.rev opts.pre.injections - } - } in - opts, extra - -(******************************************************************************) -(* Startup LoadPath and Modules *) -(******************************************************************************) -(* prelude_data == From Coq Require Import Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some false - -let injection_commands opts = - if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections - -let build_load_path opts = - let ml_path, vo_path = - if opts.pre.boot then [],[] - else - let coqlib = Envars.coqlib () in - Coqinit.libs_init_load_path ~coqlib in - ml_path @ opts.pre.ml_includes , - vo_path @ opts.pre.vo_includes diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli deleted file mode 100644 index f6222e4ec4..0000000000 --- a/toplevel/coqargs.mli +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* init:t -> string list -> t * string list -val error_wrong_arg : string -> unit - -val injection_commands : t -> Stm.injection_command list -val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 03c53d6991..0c23c9f4e9 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -41,9 +41,9 @@ coqc specific options:\ \n" } -let coqc_main copts ~opts = +let coqc_main (copts,stm_opts) ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files opts copts; + Ccompile.compile_files (opts,stm_opts) copts; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) @@ -73,8 +73,11 @@ let coqc_run copts ~opts () = let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in exit exit_code -let custom_coqc = Coqtop.{ - parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); +let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel + = Coqtop.{ + parse_extra = (fun ~opts extras -> + let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in + (Coqcargs.parse extras, stm_opts), []); help = coqc_specific_usage; init = coqc_init; run = coqc_run; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml deleted file mode 100644 index 501047c520..0000000000 --- a/toplevel/coqinit.ml +++ /dev/null @@ -1,111 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile - else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) - | None -> - try - let warn x = Feedback.msg_warning (str x) in - let inferedrc = List.find CUnix.file_readable_p [ - Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; - Envars.xdg_config_home warn / rcdefaultname; - Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; - Envars.home ~warn / "."^rcdefaultname - ] in - Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc - with Not_found -> state - (* - Flags.if_verbose - mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ - " found. Skipping rcfile loading.")) - *) - with reraise -> - let reraise = Exninfo.capture reraise in - let () = Feedback.msg_info (str"Load of rcfile failed.") in - Exninfo.iraise reraise - -(* Recursively puts `.v` files in the LoadPath *) -let build_stdlib_vo_path ~unix_path ~coq_path = - let open Loadpath in - { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true } - -(* Note we don't use has_ml=true due to #12771 , we need to see if we - should just remove that option *) -let build_userlib_path ~unix_path = - let open Loadpath in - if Sys.file_exists unix_path then - let ml_path = System.all_subdirs ~unix_path |> List.map fst in - let vo_path = - { unix_path - ; coq_path = Libnames.default_root_prefix - ; has_ml = false - ; implicit = false - ; recursive = true - } in - ml_path, [vo_path] - else [], [] - -(* LoadPath for Coq user libraries *) -let libs_init_load_path ~coqlib = - - let open Loadpath in - let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in - let coqpath = Envars.coqpath in - let coq_path = Names.DirPath.make [Libnames.coq_root] in - - (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in - - let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in - - let misc_ml, misc_vo = - List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in - - let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in - let vo_loadpath = - (* current directory (not recursively!) *) - [ { unix_path = "." - ; coq_path = Libnames.default_root_prefix - ; implicit = false - ; has_ml = true - ; recursive = false - } ] @ - - (* then standard library *) - [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ - - (* then user-contrib *) - contrib_vo @ - - (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.concat misc_vo - in - ml_loadpath, vo_loadpath diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli deleted file mode 100644 index b96a0ef162..0000000000 --- a/toplevel/coqinit.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unit - -val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t - -(** Standard LoadPath for Coq user libraries; in particular it - includes (in-order) Coq's standard library, Coq's [user-contrib] - folder, and directories specified in [COQPATH] and [XDG_DIRS] *) -val libs_init_load_path - : coqlib:CUnix.physical_path - -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqrc.ml b/toplevel/coqrc.ml new file mode 100644 index 0000000000..e074e621da --- /dev/null +++ b/toplevel/coqrc.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + if CUnix.file_readable_p rcfile then + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile + else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) + | None -> + try + let warn x = Feedback.msg_warning (Pp.str x) in + let inferedrc = List.find CUnix.file_readable_p [ + Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home warn / rcdefaultname; + Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; + Envars.home ~warn / "."^rcdefaultname + ] in + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc + with Not_found -> state + (* + Flags.if_verbose + mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ + " found. Skipping rcfile loading.")) + *) + with reraise -> + let reraise = Exninfo.capture reraise in + let () = Feedback.msg_info (Pp.str"Load of rcfile failed.") in + Exninfo.iraise reraise diff --git a/toplevel/coqrc.mli b/toplevel/coqrc.mli new file mode 100644 index 0000000000..3b8a31b2a5 --- /dev/null +++ b/toplevel/coqrc.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d0d50aee70..7596df788b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -198,11 +198,7 @@ let init_parse parse_extra help init_opts = (** Coq's init process, phase 2: Basic Coq environment, plugins. *) let init_execution opts custom_init = - (* If we have been spawned by the Spawn module, this has to be done - * early since the master waits us to connect back *) - Spawned.init_channels (); if opts.post.memory_stat then at_exit print_memory_stat; - CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority); Mltop.init_known_plugins (); (* Configuration *) Global.set_engagement opts.config.logic.impredicative_set; @@ -241,10 +237,11 @@ let init_toplevel custom = | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> let () = init_coqlib opts in + Stm.init_process (snd customopts); let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate -let init_document opts = +let init_document opts stm_options = (* Coq init process, phase 3: Stm initialization, backtracking state. It is essential that the module system is in a consistent @@ -255,7 +252,6 @@ let init_document opts = Flags.load_vos_libraries := true; let ml_load_path, vo_load_path = build_load_path opts in let injections = injection_commands opts in - let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc @@ -281,16 +277,16 @@ let start_coq custom = type run_mode = Interactive | Batch -let init_toploop opts = - let state = init_document opts in +let init_toploop opts stm_opts = + let state = init_document opts stm_opts in let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init run_mode ~opts = +let coqtop_init (run_mode,stm_opts) ~opts = if run_mode = Batch then Flags.quiet := true; init_color opts.config; Flags.if_verbose print_header (); - init_toploop opts + init_toploop opts stm_opts let coqtop_parse_extra ~opts extras = let rec parse_extra run_mode = function @@ -299,9 +295,10 @@ let coqtop_parse_extra ~opts extras = let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest | [] -> run_mode, [] in let run_mode, extras = parse_extra Interactive extras in - run_mode, extras + let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in + (run_mode, stm_opts), extras -let coqtop_run run_mode ~opts state = +let coqtop_run (run_mode,_) ~opts state = match run_mode with | Interactive -> Coqloop.loop ~opts ~state; | Batch -> exit 0 diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index e535c19252..9ae0d86cf1 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -28,7 +28,7 @@ type ('a,'b) custom_toplevel = load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [custom.run]. *) -val start_coq : ('a,'b) custom_toplevel -> unit +val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit (** Initializer color for output *) @@ -36,10 +36,10 @@ val init_color : Coqargs.coqargs_config -> unit (** Prepare state for interactive loop *) -val init_toploop : Coqargs.t -> Vernac.State.t +val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t (** The specific characterization of the coqtop_toplevel *) type run_mode = Interactive | Batch -val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel +val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index ddd11fd160..90f8fb9686 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,7 +1,5 @@ Vernac -Usage -Coqinit -Coqargs +Coqrc Coqcargs G_toplevel Coqloop diff --git a/toplevel/usage.ml b/toplevel/usage.ml deleted file mode 100644 index 6fb5f821ee..0000000000 --- a/toplevel/usage.ml +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* set the output directory for native objects\ -\n -nI dir OCaml include directories for the native compiler (default if not set) \ -\n -h, -help, --help print this list of options\ -\n" - -(* print the usage *) - -type specific_usage = { - executable_name : string; - extra_args : string; - extra_options : string; -} - -let print_usage co { executable_name; extra_args; extra_options } = - print_usage_common co ("Usage: " ^ executable_name ^ " " ^ extra_args ^ "\n\n"); - output_string co extra_options diff --git a/toplevel/usage.mli b/toplevel/usage.mli deleted file mode 100644 index cbc3b4f7e8..0000000000 --- a/toplevel/usage.mli +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unit -val machine_readable_version : unit -> unit - -(** {6 extra arguments or options to print when asking usage for a - given executable. } *) - -type specific_usage = { - executable_name : string; - extra_args : string; - extra_options : string; -} - -(** {6 Prints the generic part and specific part of usage for a - given executable. } *) - -val print_usage : out_channel -> specific_usage -> unit - diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 59e10b09a0..b0d7bb6f78 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -9,9 +9,10 @@ (************************************************************************) let worker_parse_extra ~opts extra_args = - (), extra_args + let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in + ((),stm_opts), extra_args -let worker_init init () ~opts = +let worker_init init ((),_) ~opts = Flags.quiet := true; init (); Coqtop.init_toploop opts @@ -30,6 +31,6 @@ let start ~init ~loop name = help = worker_specific_usage name; opts = Coqargs.default; init = worker_init init; - run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); + run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom -- cgit v1.2.3 From 4c4d6cfacf92b555546055a45edc19b68245b83c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 14:19:59 +0100 Subject: [sysinit] move initialization code from coqtop to here We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits. --- .github/CODEOWNERS | 1 + ide/coqide/idetop.ml | 19 ++-- stm/stm.ml | 66 +++---------- stm/stm.mli | 9 +- sysinit/coqargs.ml | 45 ++++----- sysinit/coqargs.mli | 13 ++- sysinit/coqinit.ml | 135 ++++++++++++++++++++++++++ sysinit/coqinit.mli | 58 ++++++++++++ sysinit/dune | 1 - sysinit/sysinit.mllib | 1 + toplevel/ccompile.ml | 34 +++---- toplevel/ccompile.mli | 4 +- toplevel/coqc.ml | 28 +++--- toplevel/coqtop.ml | 250 ++++++++++++++++--------------------------------- toplevel/coqtop.mli | 29 +++--- toplevel/workerLoop.ml | 10 +- 16 files changed, 380 insertions(+), 323 deletions(-) create mode 100644 sysinit/coqinit.ml create mode 100644 sysinit/coqinit.mli diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fe7913a3d2..56f48aaa4f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -228,6 +228,7 @@ /toplevel/ @coq/toplevel-maintainers /topbin/ @coq/toplevel-maintainers +/sysinit/ @coq/toplevel-maintainers ########## Vernacular ########## diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index ed0eb8f34b..2941497c12 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -513,9 +513,10 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop (run_mode,_) ~opts:_ state = +let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state = match run_mode with | Coqtop.Batch -> exit 0 + | Coqtop.Query_PrintTags -> Coqtop.print_style_tags color_mode; exit 0 | Coqtop.Interactive -> let open Vernac.State in set_doc state.doc; @@ -580,19 +581,19 @@ coqidetop specific options:\n\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" } -let islave_parse ~opts extra_args = +let islave_parse extra_args = let open Coqtop in - let (run_mode, stm_opts), extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra extra_args in let extra_args = parse extra_args in (* One of the role of coqidetop is to find the name of buffers to open *) (* in the command line; Coqide is waiting these names on stdout *) (* (see filter_coq_opts in coq.ml), so we send them now *) print_string (String.concat "\n" extra_args); - (run_mode, stm_opts), [] + ( { Coqtop.run_mode; color_mode }, stm_opts), [] -let islave_init (run_mode, stm_opts) ~opts = +let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts = if run_mode = Coqtop.Batch then Flags.quiet := true; - Coqtop.init_toploop opts stm_opts + Coqtop.init_toploop opts stm_opts injections let islave_default_opts = Coqargs.default @@ -600,8 +601,8 @@ let () = let open Coqtop in let custom = { parse_extra = islave_parse ; - help = coqidetop_specific_usage; - init = islave_init; + usage = coqidetop_specific_usage; + init_extra = islave_init; run = loop; - opts = islave_default_opts } in + initial_args = islave_default_opts } in start_coq custom diff --git a/stm/stm.ml b/stm/stm.ml index f4e370e7bc..7de109e596 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -301,7 +301,7 @@ end (* }}} *) type stm_doc_type = | VoDoc of string | VioDoc of string - | Interactive of Coqargs.interactive_top + | Interactive of Coqargs.top (* Dummy until we land the functional interp patch + fixed start_library *) type doc = int @@ -2312,13 +2312,6 @@ type stm_init_options = the specified [doc_type]. This distinction should disappear at some some point. *) - ; ml_load_path : CUnix.physical_path list - (** OCaml load paths for the document. *) - - ; vo_load_path : Loadpath.vo_path list - (** [vo] load paths for the document. Usually extracted from -R - options / _CoqProject *) - ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -2345,29 +2338,8 @@ let init_core () = if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers; State.register_root_state () -let dirpath_of_file f = - let ldir0 = - try - let lp = Loadpath.find_load_path (Filename.dirname f) in - Loadpath.logical lp - with Not_found -> Libnames.default_root_prefix - in - let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in - let id = Id.of_string f in - let ldir = Libnames.add_dirpath_suffix ldir0 id in - ldir - -let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = - let require_file (dir, from, exp) = - let mp = Libnames.qualid_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - - let handle_injection = function - | Coqargs.RequireInjection r -> require_file r - (* | LoadInjection l -> *) - | Coqargs.OptionInjection o -> Coqargs.set_option o in +let new_doc { doc_type ; injections; stm_options } = (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2377,37 +2349,27 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in - (* Set load path; important, this has to happen before we declare - the library below as [Declaremods/Library] will infer the module - name by looking at the load path! *) - List.iter Mltop.add_ml_dir ml_load_path; - List.iter Loadpath.add_vo_path vo_load_path; - Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; - begin match doc_type with - | Interactive ln -> - let dp = match ln with - | Coqargs.TopLogical dp -> dp - | Coqargs.TopPhysical f -> dirpath_of_file f - in - Declaremods.start_library dp + let top = + match doc_type with + | Interactive top -> Coqargs.dirpath_of_top top | VoDoc f -> - let ldir = dirpath_of_file f in - let () = Flags.verbosely Declaremods.start_library ldir in + let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in VCS.set_ldir ldir; - set_compilation_hints f + set_compilation_hints f; + ldir | VioDoc f -> - let ldir = dirpath_of_file f in - let () = Flags.verbosely Declaremods.start_library ldir in + let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in VCS.set_ldir ldir; - set_compilation_hints f - end; + set_compilation_hints f; + ldir + in - (* Import initial libraries. *) - List.iter handle_injection injections; + (* Start this library and import initial libraries. *) + Coqinit.start_library ~top injections; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; diff --git a/stm/stm.mli b/stm/stm.mli index dddd63cb52..bd42359cea 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -48,7 +48,7 @@ end type stm_doc_type = | VoDoc of string (* file path *) | VioDoc of string (* file path *) - | Interactive of Coqargs.interactive_top (* module path *) + | Interactive of Coqargs.top (* module path *) (** STM initialization options: *) type stm_init_options = @@ -57,13 +57,6 @@ type stm_init_options = the specified [doc_type]. This distinction should disappear at some some point. *) - ; ml_load_path : CUnix.physical_path list - (** OCaml load paths for the document. *) - - ; vo_load_path : Loadpath.vo_path list - (** [vo] load paths for the document. Usually extracted from -R - options / _CoqProject *) - ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 930c3b135f..32025ac434 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -35,12 +35,10 @@ let set_debug () = (******************************************************************************) -type color = [`ON | `AUTO | `EMACS | `OFF] - type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } -type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string +type top = TopLogical of Names.DirPath.t | TopPhysical of string type option_command = | OptionSet of string option @@ -54,14 +52,13 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : interactive_top; + toplevel_name : top; } type coqargs_config = { logic : coqargs_logic_config; rcfile : string option; coqlib : string option; - color : color; enable_VM : bool; native_compiler : native_compiler; native_output_dir : CUnix.physical_path; @@ -86,7 +83,7 @@ type coqargs_pre = { } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -120,7 +117,6 @@ let default_config = { logic = default_logic_config; rcfile = None; coqlib = None; - color = `AUTO; enable_VM = true; native_compiler = default_native; native_output_dir = ".coq-native"; @@ -181,18 +177,11 @@ let add_set_option opts opt_name value = (** Options for proof general *) let set_emacs opts = Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; - { opts with config = { opts.config with color = `EMACS; print_emacs = true }} + { opts with config = { opts.config with print_emacs = true }} let set_logic f oval = { oval with config = { oval.config with logic = f oval.config.logic }} -let set_color opts = function - | "yes" | "on" -> { opts with config = { opts.config with color = `ON }} - | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} - | "auto" -> { opts with config = { opts.config with color = `AUTO }} - | _ -> - error_wrong_arg ("Error: on/off/auto expected after option color") - let set_query opts q = { opts with main = match opts.main with | Run -> Queries (default_queries@[q]) @@ -306,7 +295,7 @@ let get_native_compiler s = (* Main parsing routine *) (*s Parsing of the command line *) -let parse_args ~help ~init arglist : t * string list = +let parse_args ~usage ~init arglist : t * string list = let args = ref arglist in let extras = ref [] in let rec parse oval = match !args with @@ -435,7 +424,6 @@ let parse_args ~help ~init arglist : t * string list = |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Exninfo.record_backtrace true; oval - |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> set_debug (); oval |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval @@ -462,12 +450,11 @@ let parse_args ~help ~init arglist : t * string list = Flags.quiet := true; Flags.make_warn false; oval - |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere - |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage) |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion @@ -483,8 +470,8 @@ let parse_args ~help ~init arglist : t * string list = with any -> fatal_error any (* We need to reverse a few lists *) -let parse_args ~help ~init args = - let opts, extra = parse_args ~help ~init args in +let parse_args ~usage ~init args = + let opts, extra = parse_args ~usage ~init args in let opts = { opts with pre = { opts.pre with @@ -513,3 +500,19 @@ let build_load_path opts = Coqloadpath.init_load_path ~coqlib in ml_path @ opts.pre.ml_includes , vo_path @ opts.pre.vo_includes + +let dirpath_of_file f = + let ldir0 = + try + let lp = Loadpath.find_load_path (Filename.dirname f) in + Loadpath.logical lp + with Not_found -> Libnames.default_root_prefix + in + let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in + let id = Names.Id.of_string f in + let ldir = Libnames.add_dirpath_suffix ldir0 id in + ldir + +let dirpath_of_top = function + | TopPhysical f -> dirpath_of_file f + | TopLogical dp -> dp diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index 894e0f2ef3..ebf367270d 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -8,14 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type color = [`ON | `AUTO | `EMACS | `OFF] - val default_toplevel : Names.DirPath.t type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } -type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string +type top = TopLogical of Names.DirPath.t | TopPhysical of string type option_command = | OptionSet of string option @@ -35,14 +33,13 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : interactive_top; + toplevel_name : top; } type coqargs_config = { logic : coqargs_logic_config; rcfile : string option; coqlib : string option; - color : color; enable_VM : bool; native_compiler : native_compiler; native_output_dir : CUnix.physical_path; @@ -67,7 +64,7 @@ type coqargs_pre = { } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -90,11 +87,13 @@ type t = { (* Default options *) val default : t -val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list +val parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string list val injection_commands : t -> injection_command list val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list +val dirpath_of_top : top -> Names.DirPath.t + (* Common utilities *) val get_int : opt:string -> string -> int diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml new file mode 100644 index 0000000000..cbecc52827 --- /dev/null +++ b/sysinit/coqinit.ml @@ -0,0 +1,135 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + (* OCAMLRUNPARAM environment variable is not set. + * In this case, we put in place our preferred configuration. + *) + set_gc_policy (); + if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else () + +let init_ocaml () = + CProfile.init_profile (); + init_gc (); + Sys.catch_break false (* Ctrl-C is fatal during the initialisation *) + +let init_coqlib opts = match opts.Coqargs.config.Coqargs.coqlib with + | None when opts.Coqargs.pre.Coqargs.boot -> () + | None -> + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + | Some s -> + Envars.set_user_coqlib s + +let print_query opts = let open Coqargs in function + | PrintVersion -> Usage.version () + | PrintMachineReadableVersion -> Usage.machine_readable_version () + | PrintWhere -> + let () = init_coqlib opts in + print_endline (Envars.coqlib ()) + | PrintHelp h -> Usage.print_usage stderr h + | PrintConfig -> + let () = init_coqlib opts in + Envars.print_config stdout Coq_config.all_src_dirs + +let parse_arguments ~parse_extra ~usage ?(initial_args=Coqargs.default) () = + let opts, extras = + Coqargs.parse_args ~usage ~init:initial_args + (List.tl (Array.to_list Sys.argv)) in + let customopts, extras = parse_extra extras in + if not (CList.is_empty extras) then begin + prerr_endline ("Don't know what to do with "^String.concat " " extras); + prerr_endline "See -help for the list of supported options"; + exit 1 + end; + match opts.Coqargs.main with + | Coqargs.Queries q -> List.iter (print_query opts) q; exit 0 + | Coqargs.Run -> opts, customopts + +let print_memory_stat () = + let open Pp in + (* -m|--memory from the command-line *) + Feedback.msg_notice + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); + (* operf-macro interface: + https://github.com/OCamlPro/operf-macro *) + try + let fn = Sys.getenv "OCAML_GC_STATS" in + let oc = open_out fn in + Gc.print_stat oc; + close_out oc + with _ -> () + +let init_runtime opts = + let open Coqargs in + Lib.init (); + init_coqlib opts; + if opts.post.memory_stat then at_exit print_memory_stat; + Mltop.init_known_plugins (); + + (* Configuration *) + Global.set_engagement opts.config.logic.impredicative_set; + Global.set_indices_matter opts.config.logic.indices_matter; + Global.set_VM opts.config.enable_VM; + Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); + Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); + + (* Native output dir *) + Nativelib.output_dir := opts.config.native_output_dir; + Nativelib.include_dirs := opts.config.native_include_dirs; + + (* Paths for loading stuff *) + let ml_load_path, vo_load_path = Coqargs.build_load_path opts in + List.iter Mltop.add_ml_dir ml_load_path; + List.iter Loadpath.add_vo_path vo_load_path; + + injection_commands opts + +let require_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] + +let handle_injection = function + | Coqargs.RequireInjection r -> require_file r + (* | LoadInjection l -> *) + | Coqargs.OptionInjection o -> Coqargs.set_option o + +let start_library ~top injections = + Flags.verbosely Declaremods.start_library top; + List.iter handle_injection injections diff --git a/sysinit/coqinit.mli b/sysinit/coqinit.mli new file mode 100644 index 0000000000..bea2186d81 --- /dev/null +++ b/sysinit/coqinit.mli @@ -0,0 +1,58 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* unit + +(** 2 parsing of Sys.argv + + This API parses command line options which are known by Coq components. + Ideally it is functional, but some values in the `Flags` modules are set + on the spot instead of being represented as "injection commands" (a field + of Coqargs.t). + + [parse_extra] and [usage] can be used to parse/document more options. *) +val parse_arguments : + parse_extra:(string list -> 'a * string list) -> + usage:Usage.specific_usage -> + ?initial_args:Coqargs.t -> + unit -> + Coqargs.t * 'a + +(** 3 initialization of global runtime data + + All global setup is done here, like COQLIB and the paths for native + compilation. If Coq is used to process multiple libraries, what is set up + here is really global and common to all of them. + + The returned injections are options (as in "Set This Thing" or "Require + that") as specified on the command line. + The prelude is one of these (unless "-nois" is passed). + + This API must be called, typically jsut after parsing arguments. *) +val init_runtime : Coqargs.t -> Coqargs.injection_command list + +(** 4 Start a library (sets options and loads objects like the prelude) + + Given the logical name [top] of the current library and the set of initial + options and required libraries, it starts its processing (see also + Declaremods.start_library) *) +val start_library : top:Names.DirPath.t -> Coqargs.injection_command list -> unit diff --git a/sysinit/dune b/sysinit/dune index 6146aa60d0..04b46fb2a2 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -4,5 +4,4 @@ (synopsis "Coq's initialization") (wrapped false) (libraries coq.vernac) - (modules coqloadpath coqargs usage) ) diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib index 9d35a931bc..715de2bb82 100644 --- a/sysinit/sysinit.mllib +++ b/sysinit/sysinit.mllib @@ -1,3 +1,4 @@ Usage Coqloadpath Coqargs +Coqinit \ No newline at end of file diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 4747abceb5..ca09bad441 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -93,7 +93,7 @@ let create_empty_file filename = close_out f (* Compile a vernac file *) -let compile opts stm_options copts ~echo ~f_in ~f_out = +let compile opts stm_options injections copts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in @@ -104,8 +104,6 @@ let compile opts stm_options copts ~echo ~f_in ~f_out = |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let ml_load_path, vo_load_path = build_load_path opts in - let injections = injection_commands opts in let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand in @@ -128,9 +126,7 @@ let compile opts stm_options copts ~echo ~f_in ~f_out = | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path; - vo_load_path; injections; stm_options; - } in + Stm.{ doc_type = VoDoc long_f_dot_out; injections; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in @@ -180,8 +176,7 @@ let compile opts stm_options copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path; - vo_load_path; injections; stm_options; + Stm.{ doc_type = VioDoc long_f_dot_out; injections; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in @@ -208,22 +203,22 @@ let compile opts stm_options copts ~echo ~f_in ~f_out = dump_empty_vos(); create_empty_file (long_f_dot_out ^ "k") -let compile opts stm_opts copts ~echo ~f_in ~f_out = +let compile opts stm_opts copts injections ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts stm_opts copts ~echo ~f_in ~f_out; + compile opts stm_opts injections copts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts stm_opts copts (f_in, echo) = +let compile_file opts stm_opts copts injections (f_in, echo) = let f_out = copts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts stm_opts copts ~echo ~f_in ~f_out) f_in + (fun f_in -> compile opts stm_opts copts injections ~echo ~f_in ~f_out) f_in else - compile opts stm_opts copts ~echo ~f_in ~f_out + compile opts stm_opts copts injections ~echo ~f_in ~f_out -let compile_files (opts, stm_opts) copts = +let compile_files (opts, stm_opts) copts injections = let compile_list = copts.compile_list in - List.iter (compile_file opts stm_opts copts) compile_list + List.iter (compile_file opts stm_opts copts injections) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -247,14 +242,7 @@ let schedule_vio copts = else Vio_checking.schedule_vio_compilation copts.vio_files_j l -let do_vio opts copts = - (* We must initialize the loadpath here as the vio scheduling - process happens outside of the STM *) - if copts.vio_files <> [] || copts.vio_tasks <> [] then - let ml_lp, vo_lp = build_load_path opts in - List.iter Mltop.add_ml_dir ml_lp; - List.iter Loadpath.add_vo_path vo_lp; - +let do_vio opts copts _injections = (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; (* Vio task pass *) diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 1b670a8edc..9f3783f32e 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -13,7 +13,7 @@ val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t (** [compile_files opts] compile files specified in [opts] *) -val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit +val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit (** [do_vio opts] process [.vio] files in [opts] *) -val do_vio : Coqargs.t -> Coqcargs.t -> unit +val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> unit diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 0c23c9f4e9..a896541573 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -13,10 +13,11 @@ let outputstate opts = let fname = CUnix.make_suffix ostate_file ".coq" in Vernacstate.System.dump fname) opts.Coqcargs.outputstate -let coqc_init _copts ~opts = +let coqc_init ((_,color_mode),_) injections ~opts = Flags.quiet := true; System.trust_file_cache := true; - Coqtop.init_color opts.Coqargs.config + Coqtop.init_color (if opts.Coqargs.config.Coqargs.print_emacs then `EMACS else color_mode); + injections let coqc_specific_usage = Usage.{ executable_name = "coqc"; @@ -41,14 +42,14 @@ coqc specific options:\ \n" } -let coqc_main (copts,stm_opts) ~opts = +let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files (opts,stm_opts) copts; + Ccompile.compile_files (opts,stm_opts) copts injections; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.do_vio opts copts; + Ccompile.do_vio opts copts injections; (* Allow the user to output an arbitrary state *) outputstate copts; @@ -61,10 +62,10 @@ let coqc_main (copts,stm_opts) ~opts = end; CProfile.print_profile () -let coqc_run copts ~opts () = +let coqc_run copts ~opts injections = let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in try - coqc_main ~opts copts; + coqc_main ~opts copts injections; exit 0 with exn -> flush_all(); @@ -73,15 +74,16 @@ let coqc_run copts ~opts () = let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in exit exit_code -let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel +let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel = Coqtop.{ - parse_extra = (fun ~opts extras -> + parse_extra = (fun extras -> + let color_mode, extras = Coqtop.parse_extra_colors extras in let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in - (Coqcargs.parse extras, stm_opts), []); - help = coqc_specific_usage; - init = coqc_init; + ((Coqcargs.parse extras, color_mode), stm_opts), []); + usage = coqc_specific_usage; + init_extra = coqc_init; run = coqc_run; - opts = Coqargs.default; + initial_args = Coqargs.default; } let main () = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7596df788b..714af6f51a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -33,18 +33,6 @@ let print_header () = Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let print_memory_stat () = - (* -m|--memory from the command-line *) - Feedback.msg_notice - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); - (* operf-macro interface: - https://github.com/OCamlPro/operf-macro *) - try - let fn = Sys.getenv "OCAML_GC_STATS" in - let oc = open_out fn in - Gc.print_stat oc; - close_out oc - with _ -> () (******************************************************************************) (* Input/Output State *) @@ -68,11 +56,46 @@ let fatal_error_exn exn = in exit exit_code -(******************************************************************************) -(* Color Options *) -(******************************************************************************) +type ('a,'b) custom_toplevel = + { parse_extra : string list -> 'a * string list + ; usage : Usage.specific_usage + ; init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b + ; initial_args : Coqargs.t + ; run : 'a -> opts:Coqargs.t -> 'b -> unit + } + +(** Main init routine *) +let init_toplevel { parse_extra; init_extra; usage; initial_args } = + Coqinit.init_ocaml (); + let opts, customopts = Coqinit.parse_arguments ~parse_extra ~usage ~initial_args () in + Stm.init_process (snd customopts); + let injections = Coqinit.init_runtime opts in + (* Allow the user to load an arbitrary state here *) + inputstate opts.pre; + (* This state will be shared by all the documents *) + Stm.init_core (); + let customstate = init_extra ~opts customopts injections in + opts, customopts, customstate + +let start_coq custom = + let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in + (* Init phase *) + let opts, custom_opts, state = + try init_toplevel custom + with any -> + flush_all(); + fatal_error_exn any in + Feedback.del_feeder init_feeder; + (* Run phase *) + custom.run ~opts custom_opts state + +(** ****************************************) +(** Specific support for coqtop executable *) + +type color = [`ON | `AUTO | `EMACS | `OFF] + let init_color opts = - let has_color = match opts.color with + let has_color = match opts with | `OFF -> false | `EMACS -> false | `ON -> true @@ -95,7 +118,7 @@ let init_color opts = Topfmt.default_styles (); false (* textual markers, no color *) end in - if opts.color = `EMACS then + if opts = `EMACS then Topfmt.set_emacs_print_strings () else if not term_color then begin Proof_diffs.write_color_enabled term_color; @@ -120,128 +143,14 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () -let init_coqlib opts = match opts.config.coqlib with - | None when opts.pre.boot -> () - | None -> - Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - | Some s -> - Envars.set_user_coqlib s - -let print_query opts = function - | PrintVersion -> Usage.version () - | PrintMachineReadableVersion -> Usage.machine_readable_version () - | PrintWhere -> - let () = init_coqlib opts in - print_endline (Envars.coqlib ()) - | PrintHelp h -> Usage.print_usage stderr h - | PrintConfig -> - let () = init_coqlib opts in - Envars.print_config stdout Coq_config.all_src_dirs - | PrintTags -> print_style_tags opts.config - -(** GC tweaking *) - -(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the - minor heap is heavily solicited. Unfortunately, the default size is far too - small, so we enlarge it a lot (128 times larger). - - To better handle huge memory consumers, we also augment the default major - heap increment and the GC pressure coefficient. -*) - -let set_gc_policy () = - Gc.set { (Gc.get ()) with - Gc.minor_heap_size = 32*1024*1024 (* 32Mwords x 8 bytes/word = 256Mb *) - ; Gc.space_overhead = 120 - } - -let set_gc_best_fit () = - Gc.set { (Gc.get ()) with - Gc.allocation_policy = 2 (* best-fit *) - ; Gc.space_overhead = 200 - } - -let init_gc () = - try - (* OCAMLRUNPARAM environment variable is set. - * In that case, we let ocamlrun to use the values provided by the user. - *) - ignore (Sys.getenv "OCAMLRUNPARAM") - - with Not_found -> - (* OCAMLRUNPARAM environment variable is not set. - * In this case, we put in place our preferred configuration. - *) - set_gc_policy (); - if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else () - -let init_process () = - (* Coq's init process, phase 1: - OCaml parameters, basic structures, and IO - *) - CProfile.init_profile (); - init_gc (); - Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - Lib.init () - -let init_parse parse_extra help init_opts = - let opts, extras = - parse_args ~help:help ~init:init_opts - (List.tl (Array.to_list Sys.argv)) in - let customopts, extras = parse_extra ~opts extras in - if not (CList.is_empty extras) then begin - prerr_endline ("Don't know what to do with "^String.concat " " extras); - prerr_endline "See -help for the list of supported options"; - exit 1 - end; - opts, customopts - -(** Coq's init process, phase 2: Basic Coq environment, plugins. *) -let init_execution opts custom_init = - if opts.post.memory_stat then at_exit print_memory_stat; - Mltop.init_known_plugins (); - (* Configuration *) - Global.set_engagement opts.config.logic.impredicative_set; - Global.set_indices_matter opts.config.logic.indices_matter; - Global.set_VM opts.config.enable_VM; - Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); - Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); - - (* Native output dir *) - Nativelib.output_dir := opts.config.native_output_dir; - Nativelib.include_dirs := opts.config.native_include_dirs; - - (* Allow the user to load an arbitrary state here *) - inputstate opts.pre; +type run_mode = Interactive | Batch | Query_PrintTags - (* This state will be shared by all the documents *) - Stm.init_core (); - custom_init ~opts - -type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list - -type ('a,'b) custom_toplevel = - { parse_extra : 'a extra_args_fn - ; help : Usage.specific_usage - ; init : 'a -> opts:Coqargs.t -> 'b - ; run : 'a -> opts:Coqargs.t -> 'b -> unit - ; opts : Coqargs.t - } - -(** Main init routine *) -let init_toplevel custom = - let () = init_process () in - let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in - (* Querying or running? *) - match opts.main with - | Queries q -> List.iter (print_query opts) q; exit 0 - | Run -> - let () = init_coqlib opts in - Stm.init_process (snd customopts); - let customstate = init_execution opts (custom.init customopts) in - opts, customopts, customstate +type toplevel_options = { + run_mode : run_mode; + color_mode : color; +} -let init_document opts stm_options = +let init_document opts stm_options injections = (* Coq init process, phase 3: Stm initialization, backtracking state. It is essential that the module system is in a consistent @@ -250,57 +159,56 @@ let init_document opts stm_options = *) (* Next line allows loading .vos files when in interactive mode *) Flags.load_vos_libraries := true; - let ml_load_path, vo_load_path = build_load_path opts in - let injections = injection_commands opts in let open Vernac.State in let doc, sid = Stm.(new_doc { doc_type = Interactive opts.config.logic.toplevel_name; - ml_load_path; vo_load_path; injections; stm_options; + injections; stm_options; }) in { doc; sid; proof = None; time = opts.config.time } -let start_coq custom = - let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in - (* Init phase *) - let opts, custom_opts, state = - try init_toplevel custom - with any -> - flush_all(); - fatal_error_exn any in - Feedback.del_feeder init_feeder; - (* Run phase *) - custom.run ~opts custom_opts state - -(** ****************************************) -(** Specific support for coqtop executable *) - -type run_mode = Interactive | Batch - -let init_toploop opts stm_opts = - let state = init_document opts stm_opts in +let init_toploop opts stm_opts injections = + let state = init_document opts stm_opts injections in let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init (run_mode,stm_opts) ~opts = +let coqtop_init ({ run_mode; color_mode }, async_opts) injections ~opts = if run_mode = Batch then Flags.quiet := true; - init_color opts.config; + init_color (if opts.config.print_emacs then `EMACS else color_mode); Flags.if_verbose print_header (); - init_toploop opts stm_opts + init_toploop opts async_opts injections + +let set_color = function + | "yes" | "on" -> `ON + | "no" | "off" -> `OFF + | "auto" ->`AUTO + | _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") + +let parse_extra_colors extras = + let rec parse_extra color_mode = function + | "-color" :: next :: rest -> parse_extra (set_color next) rest + | "-list-tags" :: rest -> parse_extra color_mode rest + | x :: rest -> + let color_mode, rest = parse_extra color_mode rest in color_mode, x :: rest + | [] -> color_mode, [] in + parse_extra `AUTO extras -let coqtop_parse_extra ~opts extras = - let rec parse_extra run_mode = function - | "-batch" :: rest -> parse_extra Batch rest +let coqtop_parse_extra extras = + let rec parse_extra run_mode = function + | "-batch" :: rest -> parse_extra Batch rest | x :: rest -> let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest | [] -> run_mode, [] in let run_mode, extras = parse_extra Interactive extras in - let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in - (run_mode, stm_opts), extras + let color_mode, extras = parse_extra_colors extras in + let async_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in + ({ run_mode; color_mode}, async_opts), extras -let coqtop_run (run_mode,_) ~opts state = +let coqtop_run ({ run_mode; color_mode },_) ~opts state = match run_mode with | Interactive -> Coqloop.loop ~opts ~state; + | Query_PrintTags -> print_style_tags color_mode; exit 0 | Batch -> exit 0 let coqtop_specific_usage = Usage.{ @@ -314,8 +222,8 @@ coqtop specific options:\n\ let coqtop_toplevel = { parse_extra = coqtop_parse_extra - ; help = coqtop_specific_usage - ; init = coqtop_init + ; usage = coqtop_specific_usage + ; init_extra = coqtop_init ; run = coqtop_run - ; opts = Coqargs.default + ; initial_args = Coqargs.default } diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 9ae0d86cf1..f51df102bd 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -9,18 +9,16 @@ (************************************************************************) (** Definition of custom toplevels. - [init] is used to do custom command line argument parsing. + [init_extra] is used to do custom initialization [run] launches a custom toplevel. *) -type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list - type ('a,'b) custom_toplevel = - { parse_extra : 'a extra_args_fn - ; help : Usage.specific_usage - ; init : 'a -> opts:Coqargs.t -> 'b + { parse_extra : string list -> 'a * string list + ; usage : Usage.specific_usage + ; init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b + ; initial_args : Coqargs.t ; run : 'a -> opts:Coqargs.t -> 'b -> unit - ; opts : Coqargs.t } (** The generic Coq main module. [start custom] will parse the command line, @@ -32,14 +30,23 @@ val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit (** Initializer color for output *) -val init_color : Coqargs.coqargs_config -> unit +type color = [`ON | `AUTO | `EMACS | `OFF] + +val init_color : color -> unit +val parse_extra_colors : string list -> color * string list +val print_style_tags : color -> unit (** Prepare state for interactive loop *) -val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t +val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqargs.injection_command list -> Vernac.State.t (** The specific characterization of the coqtop_toplevel *) -type run_mode = Interactive | Batch +type run_mode = Interactive | Batch | Query_PrintTags + +type toplevel_options = { + run_mode : run_mode; + color_mode : color; +} -val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel +val coqtop_toplevel : (toplevel_options * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index b0d7bb6f78..e72940d189 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -8,11 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let worker_parse_extra ~opts extra_args = +let worker_parse_extra extra_args = let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in ((),stm_opts), extra_args -let worker_init init ((),_) ~opts = +let worker_init init ((),_) _injections ~opts = Flags.quiet := true; init (); Coqtop.init_toploop opts @@ -28,9 +28,9 @@ let start ~init ~loop name = let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = worker_specific_usage name; - opts = Coqargs.default; - init = worker_init init; + usage = worker_specific_usage name; + initial_args = Coqargs.default; + init_extra = worker_init init; run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom -- cgit v1.2.3 From b9bac1d7ef4a4c06ebe842ffd9aac322186a65d3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 14:31:34 +0100 Subject: [coqc] move -output-context from sysinit/coqargs to coqc proper --- sysinit/coqargs.ml | 5 +---- sysinit/coqargs.mli | 1 - toplevel/coqc.ml | 5 +++-- toplevel/coqcargs.ml | 8 ++++++++ toplevel/coqcargs.mli | 2 ++ 5 files changed, 14 insertions(+), 7 deletions(-) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 32025ac434..bb0c4882e6 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -93,7 +93,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { @@ -143,7 +142,6 @@ let default_queries = [] let default_post = { memory_stat = false; - output_context = false; } let default = { @@ -440,10 +438,9 @@ let parse_args ~usage ~init arglist : t * string list = warn_deprecated_sprop_cumul(); add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval - |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} + |"-m"|"--memory" -> { oval with post = { memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} |"-boot" -> { oval with pre = { oval.pre with boot = true }} - |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} |"-quiet"|"-silent" -> diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index ebf367270d..acf941f730 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -74,7 +74,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index a896541573..a403640149 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -56,7 +56,7 @@ let coqc_main ((copts,_),stm_opts) injections ~opts = flush_all(); - if opts.Coqargs.post.Coqargs.output_context then begin + if copts.Coqcargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; @@ -79,7 +79,8 @@ let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqt parse_extra = (fun extras -> let color_mode, extras = Coqtop.parse_extra_colors extras in let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in - ((Coqcargs.parse extras, color_mode), stm_opts), []); + let coqc_opts = Coqcargs.parse extras in + ((coqc_opts, color_mode), stm_opts), []); usage = coqc_specific_usage; init_extra = coqc_init; run = coqc_run; diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 402a4d83c9..f84d73ed17 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -25,6 +25,8 @@ type t = ; outputstate : string option ; glob_out : Dumpglob.glob_output + + ; output_context : bool } let default = @@ -42,6 +44,8 @@ let default = ; outputstate = None ; glob_out = Dumpglob.MultFiles + + ; output_context = false } let depr opt = @@ -162,6 +166,10 @@ let parse arglist : t = depr opt; let _ = next () in oval + + (* Non deprecated options *) + | "-output-context" -> + { oval with output_context = true } (* Verbose == echo mode *) | "-verbose" -> echo := true; diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index a9fc27b1b4..905250e363 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -39,6 +39,8 @@ type t = ; outputstate : string option ; glob_out : Dumpglob.glob_output + + ; output_context : bool } val default : t -- cgit v1.2.3 From f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 17:13:59 +0100 Subject: [coqtop] handle -print-module-uid after initialization --- ide/coqide/idetop.ml | 3 ++- sysinit/coqargs.ml | 12 ------------ toplevel/coqtop.ml | 21 ++++++++++++++++++--- toplevel/coqtop.mli | 3 ++- 4 files changed, 22 insertions(+), 17 deletions(-) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2941497c12..b42c705add 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -516,7 +516,8 @@ let msg_format = ref (fun () -> let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state = match run_mode with | Coqtop.Batch -> exit 0 - | Coqtop.Query_PrintTags -> Coqtop.print_style_tags color_mode; exit 0 + | Coqtop.(Query PrintTags) -> Coqtop.print_style_tags color_mode; exit 0 + | Coqtop.(Query _) -> Printf.eprintf "Unknown query"; exit 1 | Coqtop.Interactive -> let open Vernac.State in set_doc state.doc; diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index bb0c4882e6..19350b7e98 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -220,15 +220,6 @@ let get_float ~opt n = with Failure _ -> error_wrong_arg ("Error: float expected after option "^opt) -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - Filename.(List.fold_left concat (dirname s) - [ !Nativelib.output_dir - ; Library.native_name_from_filename s - ]) - with _ -> "" - let interp_set_option opt v old = let open Goptions in let opt = String.concat " " opt in @@ -361,9 +352,6 @@ let parse_args ~usage ~init arglist : t * string list = Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); oval - |"-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 ()); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 714af6f51a..caf86ef870 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -143,7 +143,8 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () -type run_mode = Interactive | Batch | Query_PrintTags +type query = PrintTags | PrintModUid of string list +type run_mode = Interactive | Batch | Query of query type toplevel_options = { run_mode : run_mode; @@ -197,7 +198,8 @@ let parse_extra_colors extras = let coqtop_parse_extra extras = let rec parse_extra run_mode = function | "-batch" :: rest -> parse_extra Batch rest - | x :: rest -> + | "-print-mod-uid" :: rest -> Query (PrintModUid rest), [] + | x :: rest -> let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest | [] -> run_mode, [] in let run_mode, extras = parse_extra Interactive extras in @@ -205,10 +207,23 @@ let coqtop_parse_extra extras = let async_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in ({ run_mode; color_mode}, async_opts), extras +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + Filename.(List.fold_left concat (dirname s) + [ !Nativelib.output_dir + ; Library.native_name_from_filename s + ]) + with _ -> "" + let coqtop_run ({ run_mode; color_mode },_) ~opts state = match run_mode with | Interactive -> Coqloop.loop ~opts ~state; - | Query_PrintTags -> print_style_tags color_mode; exit 0 + | Query PrintTags -> print_style_tags color_mode; exit 0 + | Query (PrintModUid sl) -> + let s = String.concat " " (List.map get_native_name sl) in + print_endline s; + exit 0 | Batch -> exit 0 let coqtop_specific_usage = Usage.{ diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index f51df102bd..c675c6adec 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -42,7 +42,8 @@ val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqargs.injection_comma (** The specific characterization of the coqtop_toplevel *) -type run_mode = Interactive | Batch | Query_PrintTags +type query = PrintTags | PrintModUid of string list +type run_mode = Interactive | Batch | Query of query type toplevel_options = { run_mode : run_mode; -- cgit v1.2.3 From 2caae4d530ba97ced98711986dc504f9becdab81 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 17:14:22 +0100 Subject: [coqargs] use standard option injection for -mangle-names --- sysinit/coqargs.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 19350b7e98..ac9e430d31 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -348,9 +348,8 @@ let parse_args ~usage ~init arglist : t * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Goptions.set_bool_option_value ["Mangle"; "Names"] true; - Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); - oval + let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in + add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ()))) |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; -- cgit v1.2.3 From 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 17:31:33 +0100 Subject: [coqargs] use standard option injection for -type-in-type --- sysinit/coqargs.ml | 8 +++----- sysinit/coqargs.mli | 1 + sysinit/coqinit.ml | 1 + 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index ac9e430d31..faa26423e5 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -25,10 +25,6 @@ let error_missing_arg s = (* Imperative effects! This must be fixed at some point. *) (******************************************************************************) -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } - let set_debug () = let () = Exninfo.record_backtrace true in Flags.debug := true @@ -52,6 +48,7 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; + type_in_type : bool; toplevel_name : top; } @@ -109,6 +106,7 @@ let default_native = Coq_config.native_compiler let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; + type_in_type = false; toplevel_name = TopLogical default_toplevel; } @@ -435,7 +433,7 @@ let parse_args ~usage ~init arglist : t * string list = Flags.make_warn false; oval |"-time" -> { oval with config = { oval.config with time = true }} - |"-type-in-type" -> set_type_in_type (); oval + |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage) diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index acf941f730..cc622fabe3 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -33,6 +33,7 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; + type_in_type : bool; toplevel_name : top; } diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index cbecc52827..16c8389de5 100644 --- a/sysinit/coqinit.ml +++ b/sysinit/coqinit.ml @@ -105,6 +105,7 @@ let init_runtime opts = (* Configuration *) Global.set_engagement opts.config.logic.impredicative_set; Global.set_indices_matter opts.config.logic.indices_matter; + Global.set_check_universes (not opts.config.logic.type_in_type); Global.set_VM opts.config.enable_VM; Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); -- cgit v1.2.3 From d414273bbd53681baecf3ddc6d343243c80e8103 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 18:21:55 +0100 Subject: [coqargs] use standard option injection for -print-emacs --- sysinit/coqargs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index faa26423e5..c4f12f6bb7 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -172,7 +172,7 @@ let add_set_option opts opt_name value = (** Options for proof general *) let set_emacs opts = - Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; + let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in { opts with config = { opts.config with print_emacs = true }} let set_logic f oval = -- cgit v1.2.3 From 6e258b391363aa2345c4dc265ba381b1712fe083 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jan 2021 19:57:08 +0100 Subject: make the linter happy --- stm/stmargs.ml | 2 +- sysinit/coqargs.mli | 2 +- sysinit/sysinit.mllib | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/stm/stmargs.ml b/stm/stmargs.ml index 609d4f42e9..e2c7649a8f 100644 --- a/stm/stmargs.ml +++ b/stm/stmargs.ml @@ -137,4 +137,4 @@ let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list = let usage = "\ \n -stm-debug STM debug mode (will trace every transaction)\ -" \ No newline at end of file +" diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index cc622fabe3..aef50193f2 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -103,4 +103,4 @@ val get_float : opt:string -> string -> float val error_missing_arg : string -> 'a val error_wrong_arg : string -> 'a -val set_option : Goptions.option_name * option_command -> unit \ No newline at end of file +val set_option : Goptions.option_name * option_command -> unit diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib index 715de2bb82..6e86536648 100644 --- a/sysinit/sysinit.mllib +++ b/sysinit/sysinit.mllib @@ -1,4 +1,4 @@ Usage Coqloadpath Coqargs -Coqinit \ No newline at end of file +Coqinit -- cgit v1.2.3 From be070cfb10a59be13a478a7efbf92dd3e22401ed Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Jan 2021 11:35:35 +0100 Subject: Add sysinit to load_printer lists --- dev/core.dbg | 1 + dev/core_dune.dbg | 1 + dev/dune_db_408 | 1 + dev/dune_db_409 | 1 + dev/ocamldebug-coq.run | 2 +- 5 files changed, 5 insertions(+), 1 deletion(-) diff --git a/dev/core.dbg b/dev/core.dbg index 6d52bae773..dcf9910b0b 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,6 @@ load_printer parsing.cma load_printer printing.cma load_printer tactics.cma load_printer vernac.cma +load_printer sysinit.cma load_printer stm.cma load_printer toplevel.cma diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg index 3f73cf126a..da3022644d 100644 --- a/dev/core_dune.dbg +++ b/dev/core_dune.dbg @@ -17,5 +17,6 @@ load_printer parsing.cma load_printer printing.cma load_printer tactics.cma load_printer vernac.cma +load_printer sysinit.cma load_printer stm.cma load_printer toplevel.cma diff --git a/dev/dune_db_408 b/dev/dune_db_408 index 5f826fe383..bc86020d56 100644 --- a/dev/dune_db_408 +++ b/dev/dune_db_408 @@ -17,6 +17,7 @@ load_printer parsing.cma load_printer printing.cma load_printer tactics.cma load_printer vernac.cma +load_printer sysinit.cma load_printer stm.cma load_printer toplevel.cma diff --git a/dev/dune_db_409 b/dev/dune_db_409 index 2e58272c75..adb1f76872 100644 --- a/dev/dune_db_409 +++ b/dev/dune_db_409 @@ -16,6 +16,7 @@ load_printer parsing.cma load_printer printing.cma load_printer tactics.cma load_printer vernac.cma +load_printer sysinit.cma load_printer stm.cma load_printer toplevel.cma diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 534f20f85b..db15d9705a 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -19,7 +19,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/gramlib/.pack \ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ - -I $COQTOP/library -I $COQTOP/engine \ + -I $COQTOP/library -I $COQTOP/engine -I $COQTOP/sysinit \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -- cgit v1.2.3 From 4d6c244ca6003991d6a3932461c5b1034e32b8f4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Jan 2021 15:29:32 +0100 Subject: Typo in comment Co-authored-by: Enrico Tassi --- lib/stateid.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/stateid.mli b/lib/stateid.mli index 4563710f84..00acc962a2 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -42,7 +42,7 @@ type ('a,'b) request = { name : string } -(* Asks the document manager is the given state is valid (or belongs to an +(* Asks the document manager if the given state is valid (or belongs to an old version of the document) *) val is_valid : doc:int -> t -> bool -- cgit v1.2.3