diff options
90 files changed, 1030 insertions, 1018 deletions
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/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/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/doc/release-process.md b/dev/doc/release-process.md index 19562b60a2..894244044a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -144,6 +144,7 @@ in time. together with its SHA256 hash in a signed e-mail to `dsi.securite` @ `inria.fr` putting `@maximedenes` in carbon copy. + The MacOS packages should be signed with our own certificate. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). +- [ ] Upload the PDF version of the reference manual to the GitHub release. (*TODO:* automate this.) - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). - [ ] Merge the website update, publish the release @@ -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/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 \ 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/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst new file mode 100644 index 0000000000..4ea54a1ab6 --- /dev/null +++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst @@ -0,0 +1,9 @@ +- **Removed:** + double induction tactic. Replace :n:`double induction @ident @ident` + with :n:`induction @ident; induction @ident` (or + :n:`induction @ident ; destruct @ident` depending on the exact needs). + Replace :n:`double induction @natural__1 @natural__2` with + :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result + of :n:`natural__2 - natural__1` + (`#13762 <https://github.com/coq/coq/pull/13762>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst new file mode 100644 index 0000000000..84d6bdea89 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst @@ -0,0 +1,4 @@ +- **Removed:** + The Hide Obligations flag, deprecated in 8.12 + (`#13758 <https://github.com/coq/coq/pull/13758>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst new file mode 100644 index 0000000000..7f0650d8ee --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst @@ -0,0 +1,4 @@ +- **Removed:** + SearchHead command. Use the `headconcl:` clause of :cmd:`Search` instead + (`#13763 <https://github.com/coq/coq/pull/13763>`_, + by Jim Fehrle). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 2b24ced8a1..8f2b51ccce 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -320,14 +320,6 @@ optional tactic is replaced by the default one if not specified. (the default), or if the system should infer which obligations can be declared opaque. -.. flag:: Hide Obligations - - .. deprecated:: 8.12 - - Controls whether obligations appearing in the - term should be hidden as implicit arguments of the special - constant ``Program.Tactics.obligation``. - The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also adds some useful notations, as documented in the file itself. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index a08a110930..4769636ae8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1230,7 +1230,7 @@ Flags, options and attributes :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** - :flag:`Hide Obligations` flag + `Hide Obligations` flag (`#11828 <https://github.com/coq/coq/pull/11828>`_, by Emilio Jesus Gallego Arias). - **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical @@ -1301,7 +1301,7 @@ Commands Declaration of arbitrary terms as hints. Global references are now preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by Pierre-Marie Pédrot). -- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:` +- **Deprecated:** `SearchHead` in favor of the new `headconcl:` clause of :cmd:`Search` (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). - **Added:** diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..665bae7077 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -77,7 +77,7 @@ specified, the default selector is used. .. todo: fully describe selectors. At the moment, ltac has a fairly complete description .. todo: mention selectors can be applied to some commands, such as - Check, Search, SearchHead, SearchPattern, SearchRewrite. + Check, Search, SearchPattern, SearchRewrite. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -498,10 +498,16 @@ one or more of its hypotheses. :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. - Occurrences are numbered from left to right starting with 1 when the - goal is printed with the :flag:`Printing All` flag. (In particular, occurrences - in :ref:`implicit arguments <ImplicitArguments>` and - :ref:`coercions <Coercions>` are counted but not shown by default.) + Occurrences are numbered starting with 1 following a depth-first traversal + of the term's expression, including occurrences in + :ref:`implicit arguments <ImplicitArguments>` + and :ref:`coercions <Coercions>` that are not displayed by default. + (Set the :flag:`Printing All` flag to show those in the printed term.) + + For example, when matching the pattern `_ + _` in the term `(a + b) + c`, + occurrence 1 is `(...) + c` and + occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`, + occurrence 1 is `a + (...)` and occurrence 2 is `b + c`. Specifying `-` includes all occurrences *except* the ones listed. @@ -2067,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent premise of the goal. -.. tacn:: double induction @ident @ident - :name: double induction - - This tactic is deprecated and should be replaced by - :n:`induction @ident; induction @ident` (or - :n:`induction @ident ; destruct @ident` depending on the exact needs). - -.. tacv:: double induction @natural__1 @natural__2 - - This tactic is deprecated and should be replaced by - :n:`induction num1; induction num3` where :n:`num3` is the result - of :n:`num2 - num1` - .. tacn:: dependent induction @ident :name: dependent induction diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8e2f577f6b..8d1817b61f 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -312,31 +312,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } - - .. deprecated:: 8.12 - - Use the `headconcl:` clause of :cmd:`Search` instead. - - Displays the name and type of all hypotheses of the - selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` - matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` - matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. - - See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - - .. example:: :cmd:`SearchHead` examples - - .. coqtop:: none reset - - Add Search Blacklist "internal_". - - .. coqtop:: all warn - - SearchHead le. - SearchHead (@eq bool). - .. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the @@ -384,7 +359,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. table:: Search Blacklist @string Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, - :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose fully-qualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. @@ -395,7 +370,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. flag:: Search Output Name Only This flag restricts the output of search commands to identifier names; - turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, + turning it on causes invocations of :cmd:`Search`, :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 0a4a48555f..663337bc64 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -91,7 +91,10 @@ Rewriting with Leibniz and setoid equality in the conclusion is replaced. If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. + :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality, + which means that you must `Require Setoid` to use that form. + However, note that :tacn:`rewrite` (even when using setoid rewriting) and + :tacn:`setoid_rewrite` don't behave identically (as already mentioned above). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml index 711986c2b2..2d75ad9ff6 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -207,7 +207,6 @@ let state_preserving = [ "Recursive Extraction Library"; "Search"; - "SearchHead"; "SearchPattern"; "SearchRewrite"; diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 528e2a756b..b42c705add 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -513,9 +513,11 @@ 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.(Query _) -> Printf.eprintf "Unknown query"; exit 1 | Coqtop.Interactive -> let open Vernac.State in set_doc state.doc; @@ -580,32 +582,28 @@ 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, 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, [] + ( { Coqtop.run_mode; color_mode }, stm_opts), [] -let islave_init run_mode ~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 + Coqtop.init_toploop opts stm_opts injections -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 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/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..00acc962a2 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -42,3 +42,10 @@ type ('a,'b) request = { name : string } +(* 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 + +(* 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/library/summary.ml b/library/summary.ml index 221ac868fa..572467ada3 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -131,28 +131,27 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x module Local = struct -type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref +type 'a local_ref = 'a CEphemeron.key ref * 'a CEphemeron.key Dyn.tag -let set r v = r := (CEphemeron.create v, snd !r) +let set (r, tag) v = r := CEphemeron.create v -let get r = - let key, name = !r in - try CEphemeron.get key +let get (key, name) = + try CEphemeron.get !key with CEphemeron.InvalidKey -> let { init_function } = DynMap.find name !sum_map in init_function (); - CEphemeron.get (fst !r) + CEphemeron.get !key -let ref ?(freeze=fun x -> x) ~name init = +let ref (type a) ~name (init : a) : a local_ref = let () = check_name (mangle name) in - let tag : 'a Dyn.tag = Dyn.create (mangle name) in - let r = pervasives_ref (CEphemeron.create init, tag) in + let tag : a CEphemeron.key Dyn.tag = Dyn.create (mangle name) in + let r = pervasives_ref (CEphemeron.create init) in let () = sum_map := DynMap.add tag - { freeze_function = (fun ~marshallable -> freeze (get r)); - unfreeze_function = (set r); - init_function = (fun () -> set r init) } !sum_map + { freeze_function = (fun ~marshallable -> !r); + unfreeze_function = (fun v -> r := v); + init_function = (fun () -> r := CEphemeron.create init) } !sum_map in - r + (r, tag) let (!) = get let (:=) = set diff --git a/library/summary.mli b/library/summary.mli index 7c5e1bee6f..a6f94a49ae 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -53,7 +53,7 @@ val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a module Local : sig type 'a local_ref - val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val ref : name:string -> 'a -> 'a local_ref val (:=) : 'a local_ref -> 'a -> unit val (!) : 'a local_ref -> 'a diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index e39c066c95..b20c4d173d 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } END -(** Double induction *) - -TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () } -| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - { Elim.h_double_induction h1 h2 } -END - (* Admit *) TACTIC EXTEND admit diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 6bf330c830..e7902d06eb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program -| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } -| [ "Obligations" ] -> { show_obligations None } +| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) } +| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None } END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program -| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } -| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) } +| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } +| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) } END { 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/pretyping/tacred.ml b/pretyping/tacred.ml index a103699716..430813e874 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -384,11 +384,6 @@ let x = Name default_dependent_ident do so that the reduction uses this extra information *) let dummy = mkProp -let vfx = Id.of_string "_expanded_fix_" -let vfun = Id.of_string "_eliminator_function_" -let venv = let open Context.Named.Declaration in - val_of_named_context [LocalAssum (make_annot vfx Sorts.Relevant, dummy); - LocalAssum (make_annot vfun Sorts.Relevant, dummy)] (* Mark every occurrence of substituted vars (associated to a function) as a problem variable: an evar that can be instantiated either by @@ -403,10 +398,10 @@ let substl_with_function subst sigma constr = match v.(i-k-1) with | (fx, Some (min, ref)) -> let sigma = !evd in - let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in + let (sigma, evk) = Evarutil.new_pure_evar empty_named_context_val sigma dummy in evd := sigma; - minargs := Evar.Map.add evk min !minargs; - Vars.lift k (mkEvar (evk, [fx; ref])) + minargs := Evar.Map.add evk (min, fx, ref) !minargs; + mkEvar (evk, []) | (fx, None) -> Vars.lift k fx else mkRel (i - Array.length v) | _ -> @@ -419,14 +414,14 @@ exception Partial (* each problem variable that cannot be made totally applied even by reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = - let evm = ref sigma in - let set_fix i = evm := Evd.define i (mkVar vfx) !evm in + let set = ref Evar.Set.empty in + let set_fix i = set := Evar.Set.add i !set in let rec check strict c = let c' = whd_betaiotazeta env sigma c in let (h,rcargs) = decompose_app_vect sigma c' in match EConstr.kind sigma h with - Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> - let minargs = Evar.Map.find i fxminargs in + Evar(i,_) when Evar.Map.mem i fxminargs && not (Evar.Set.mem i !set) -> + let minargs, _, _ = Evar.Map.find i fxminargs in if Array.length rcargs < minargs then if strict then set_fix i else raise Partial; @@ -435,45 +430,95 @@ let solve_arity_problem env sigma fxminargs c = (let ev, u = destEvalRefU sigma h in match reference_opt_value env sigma ev u with | Some h' -> - let bak = !evm in + let bak = !set in (try Array.iter (check false) rcargs with Partial -> - evm := bak; + set := bak; check strict (mkApp(h',rcargs))) | None -> Array.iter (check strict) rcargs) | _ -> EConstr.iter sigma (check strict) c' in check true c; - !evm + !set let substl_checking_arity env subst sigma c = (* we initialize the problem: *) let body,sigma,minargs = substl_with_function subst sigma c in (* we collect arity constraints *) - let sigma' = solve_arity_problem env sigma minargs body in + let ans = solve_arity_problem env sigma minargs body in (* we propagate the constraints: solved problems are substituted; the other ones are replaced by the function symbol *) - let rec nf_fix c = match EConstr.kind sigma c with - | Evar (i,[fx;f]) when Evar.Map.mem i minargs -> + let rec nf_fix k c = match EConstr.kind sigma c with + | Evar (i, []) -> (* FIXME: find a less hackish way of doing this *) - begin match EConstr.kind sigma' c with - | Evar _ -> f - | c -> EConstr.of_kind c + begin match Evar.Map.find i minargs with + | (_, fx, ref) -> + if Evar.Set.mem i ans then Vars.lift k fx + else Vars.lift k ref + | exception Not_found -> + (* An argumentless evar that was not generated by substl_with_function *) + c end - | _ -> EConstr.map sigma nf_fix c + | _ -> EConstr.map_with_binders sigma succ nf_fix k c in - nf_fix body + nf_fix 0 body type fix_reduction_result = NotReducible | Reduced of (constr * constr list) let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = + let (names, (nbfix, lv, n)), u, largs = f in + let lu = List.firstn n largs in + let p = List.length lv in + let lyi = List.map fst lv in + let la = + List.map_i (fun q aq -> + (* k from the comment is q+1 *) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) + with Not_found -> Vars.lift p aq) + 0 lu + in + let f i = match names.(i) with + | None -> None + | Some (minargs,ref) -> + let body = applist (mkEvalRef ref u, la) in + let g = + List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> + let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in + let tij' = Vars.substl (List.rev subst) tij in + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) + in Some (minargs,g) + in let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = List.init nbodies make_Fi in - substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) + let c = substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) in + nf_beta env sigma c let contract_cofix_use_function env sigma f - (bodynum,(_names,_,bodies as typedbodies)) = + (bodynum,(names,_,bodies as typedbodies)) args = + let f = + if isConst sigma f then + let minargs = List.length args in + fun i -> + if Int.equal i bodynum then Some (minargs, f) + else match names.(i).binder_name with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + mutual inductive, try to reuse the global name if + the block was indeed initially built as a global + definition *) + let (kn, u) = destConst sigma f in + let kn = Constant.change_label kn (Label.of_id id) in + let cst = (kn, EInstance.kind sigma u) in + try match constant_opt_value_in env cst with + | None -> None + (* TODO: check kn is correct *) + | Some _ -> Some (minargs,mkConstU (kn, u)) + with Not_found -> None + else + fun _ -> None in let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = List.init nbodies make_Fi in @@ -503,7 +548,7 @@ let reduce_mind_case env sigma mia = mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false -let reduce_mind_case_use_function func env sigma mia = +let reduce_mind_case_use_function f env sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((_, i as cstr),u) -> let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in @@ -512,30 +557,8 @@ let reduce_mind_case_use_function func env sigma mia = let br = it_mkLambda_or_LetIn (snd br) ctx in applist (br, real_cargs) | CoFix (bodynum,(names,_,_) as cofix) -> - let build_cofix_name = - if isConst sigma func then - let minargs = List.length mia.mcargs in - fun i -> - if Int.equal i bodynum then Some (minargs,func) - else match names.(i).binder_name with - | Anonymous -> None - | Name id -> - (* In case of a call to another component of a block of - mutual inductive, try to reuse the global name if - the block was indeed initially built as a global - definition *) - let (kn, u) = destConst sigma func in - let kn = Constant.change_label kn (Label.of_id id) in - let cst = (kn, EInstance.kind sigma u) in - try match constant_opt_value_in env cst with - | None -> None - (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConstU (kn, u)) - with Not_found -> None - else - fun _ -> None in let cofix_def = - contract_cofix_use_function env sigma build_cofix_name cofix in + contract_cofix_use_function env sigma f cofix mia.mcargs in mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -686,7 +709,7 @@ let rec red_elim_const env sigma ref u largs = let f = ([|Some (minfxargs,ref)|],infos), u, largs in (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) + | Reduced (c,rest) -> (c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> let rec descend (ref,u) args = let c = reference_value env sigma ref u in @@ -700,7 +723,7 @@ let rec red_elim_const env sigma ref u largs = let f = refinfos, u, midargs in (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) + | Reduced (c,rest) -> (c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase @@ -825,29 +848,6 @@ and reduce_fix_use_function env sigma f fix stack = let stack' = List.assign stack recargnum (applist recarg') in (match EConstr.kind sigma recarg'hd with | Construct _ -> - let (names, (nbfix, lv, n)), u, largs = f in - let lu = List.firstn n largs in - let p = List.length lv in - let lyi = List.map fst lv in - let la = - List.map_i (fun q aq -> - (* k from the comment is q+1 *) - try mkRel (p+1-(List.index Int.equal (n-q) lyi)) - with Not_found -> Vars.lift p aq) - 0 lu - in - let f i = match names.(i) with - | None -> None - | Some (minargs,ref) -> - let body = applist (mkEvalRef ref u, la) in - let g = - List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> - let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in - let tij' = Vars.substl (List.rev subst) tij in - let x = make_annot x Sorts.Relevant in (* TODO relevance *) - mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some (minargs,g) - in Reduced (contract_fix_use_function env sigma f fix,stack') | _ -> NotReducible) @@ -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 1c06c1efb7..7de109e596 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.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 = @@ -801,6 +799,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 @@ -2305,34 +2306,13 @@ end (* }}} *) (** STM initialization options: *) -type option_command = OptionSet of string option | 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 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 : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -2349,67 +2329,17 @@ 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; 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 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 in - let handle_injection = function - | RequireInjection r -> require_file r - (* | LoadInjection l -> *) - | OptionInjection o -> set_option o in +let new_doc { doc_type ; injections; stm_options } = (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2419,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 - | TopLogical dp -> dp - | 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 097bcbe0ca..bd42359cea 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -42,29 +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 | 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.top (* module path *) (** STM initialization options: *) type stm_init_options = @@ -73,14 +57,7 @@ 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 : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -91,8 +68,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 831369625f..a77e0c79e7 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -3,10 +3,10 @@ Dag Vcs TQueue WorkerPool -Vernac_classifier CoqworkmgrApi AsyncTaskQueue Partac Stm +Stmargs ProofBlockDelimiter Vio_checking diff --git a/stm/stmargs.ml b/stm/stmargs.ml new file mode 100644 index 0000000000..e2c7649a8f --- /dev/null +++ b/stm/stmargs.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let fatal_error exn = + Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn); + let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in + exit exit_code + +let set_worker_id opt s = + assert (s <> "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)\ +" 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val parse_args : init:Stm.AsyncOpts.stm_opt -> string list -> Stm.AsyncOpts.stm_opt * string list + +val usage : string diff --git a/toplevel/coqargs.ml b/sysinit/coqargs.ml index fbf3b4873b..c4f12f6bb7 100644 --- a/toplevel/coqargs.ml +++ b/sysinit/coqargs.ml @@ -24,37 +24,42 @@ let error_missing_arg s = (******************************************************************************) (* Imperative effects! This must be fixed at some point. *) (******************************************************************************) -let set_worker_id opt s = - assert (s <> "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 } +let set_debug () = + let () = Exninfo.record_backtrace true in + Flags.debug := true (******************************************************************************) -type color = [`ON | `AUTO | `EMACS | `OFF] - type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } +type top = TopLogical of Names.DirPath.t | TopPhysical of string + +type option_command = + | OptionSet of string option + | OptionUnset + | OptionAppend of string + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + | RequireInjection of (string * string option * bool option) + type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : Stm.interactive_top; + type_in_type : bool; + 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; native_include_dirs : CUnix.physical_path list; - stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; time : bool; print_emacs : bool; @@ -69,13 +74,13 @@ type coqargs_pre = { vo_includes : Loadpath.vo_path list; load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; + injections : injection_command list; inputstate : string option; } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -85,7 +90,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { @@ -102,19 +106,18 @@ let default_native = Coq_config.native_compiler let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; - toplevel_name = Stm.TopLogical default_toplevel; + type_in_type = false; + toplevel_name = 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; @@ -137,7 +140,6 @@ let default_queries = [] let default_post = { memory_stat = false; - output_context = false; } let default = { @@ -160,29 +162,22 @@ let add_vo_include opts unix_path coq_path implicit = 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 }} + { opts with pre = { opts.pre with injections = 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 }} + { opts with pre = { opts.pre with injections = 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 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 = { 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]) @@ -204,61 +199,39 @@ let set_inputstate opts s = (******************************************************************************) (* Parsing helpers *) (******************************************************************************) -let get_bool opt = function +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 = +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 = +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 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" @@ -309,7 +282,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 @@ -351,55 +324,6 @@ let parse_args ~help ~init arglist : t * string list = { 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) @@ -422,16 +346,12 @@ let parse_args ~help ~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 - - |"-print-mod-uid" -> - let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + 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; - Flags.profile_ltac_cutoff := get_float opt (next ()); + Flags.profile_ltac_cutoff := get_float ~opt (next ()); oval |"-rfrom" -> @@ -451,28 +371,18 @@ let parse_args ~help ~init arglist : t * string list = 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 }}} + { 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 = 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 + { 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 - (CWarnings.set_flags w; oval) - else - let w = CWarnings.get_flags () ^ "," ^ w in - CWarnings.set_flags (CWarnings.normalize_flags_string w); - oval + 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 ()) }} + { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} |"-native-compiler" -> let native_compiler = get_native_compiler (next ()) in @@ -480,10 +390,10 @@ let parse_args ~help ~init arglist : t * string list = | "-set" -> let opt, v = parse_option_set @@ next() in - add_set_option oval opt (Stm.OptionSet v) + add_set_option oval opt (OptionSet v) | "-unset" -> - add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset + add_set_option oval (to_opt_key @@ next ()) OptionUnset |"-native-output-dir" -> let native_output_dir = next () in @@ -494,49 +404,39 @@ let parse_args ~help ~init arglist : t * string list = { 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 + |"-debug" -> set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval |"-diffs" -> - add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) - |"-stm-debug" -> Stm.stm_debug := true; oval + 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 (Stm.OptionSet None) + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) |"-disallow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset + 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 (Stm.OptionSet None) + 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" -> 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 + |"-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 help) + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage) |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion @@ -552,8 +452,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 @@ -572,13 +472,29 @@ let parse_args ~help ~init args = 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 + 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 - Coqinit.libs_init_load_path ~coqlib in + 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/toplevel/coqargs.mli b/sysinit/coqargs.mli index f6222e4ec4..aef50193f2 100644 --- a/toplevel/coqargs.mli +++ b/sysinit/coqargs.mli @@ -8,29 +8,43 @@ (* * (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 top = TopLogical of Names.DirPath.t | TopPhysical of string + +type option_command = + | OptionSet of string option + | OptionUnset + | OptionAppend of string + +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. *) + type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : Stm.interactive_top; + type_in_type : bool; + 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; native_include_dirs : CUnix.physical_path list; - stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; time : bool; print_emacs : bool; @@ -45,13 +59,13 @@ type coqargs_pre = { vo_includes : Loadpath.vo_path list; load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; + injections : injection_command list; inputstate : string option; } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -61,7 +75,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { @@ -74,8 +87,20 @@ type t = { (* Default options *) val default : t -val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list -val error_wrong_arg : string -> unit +val parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string list -val injection_commands : t -> Stm.injection_command 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 +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 diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml new file mode 100644 index 0000000000..16c8389de5 --- /dev/null +++ b/sysinit/coqinit.ml @@ -0,0 +1,136 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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_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_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); + + (* 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Main etry point to the sysinit component, all other modules are private. + + The following API shoud be called in order, and the first 3 steps only once + since they initialize global data. On the contrary step 4 can be called + many times to init the compilation of a unit. +*) + +(** 1 initialization of OCaml's runtime + + Profiling, GC parameters and signals. Nothing specific to Coq per se, but + the defaults here are good for Coq. + This API should be called up very early, or not at all. *) +val init_ocaml : unit -> 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/toplevel/coqinit.ml b/sysinit/coqloadpath.ml index 501047c520..8635345e00 100644 --- a/toplevel/coqinit.ml +++ b/sysinit/coqloadpath.ml @@ -13,44 +13,6 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 -let set_debug () = - let () = Exninfo.record_backtrace true in - Flags.debug := true - -(* Loading of the resource file. - rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one - does not exist. *) - -let rcdefaultname = "coqrc" - -let load_rcfile ~rcfile ~state = - try - match rcfile with - | Some rcfile -> - 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 @@ -73,7 +35,7 @@ let build_userlib_path ~unix_path = else [], [] (* LoadPath for Coq user libraries *) -let libs_init_load_path ~coqlib = +let init_load_path ~coqlib = let open Loadpath in let user_contrib = coqlib/"user-contrib" in diff --git a/toplevel/coqinit.mli b/sysinit/coqloadpath.mli index b96a0ef162..d853e9ea54 100644 --- a/toplevel/coqinit.mli +++ b/sysinit/coqloadpath.mli @@ -8,15 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Initialization. *) - -val set_debug : unit -> 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 +val init_load_path : coqlib:CUnix.physical_path -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/sysinit/dune b/sysinit/dune new file mode 100644 index 0000000000..04b46fb2a2 --- /dev/null +++ b/sysinit/dune @@ -0,0 +1,7 @@ +(library + (name sysinit) + (public_name coq.sysinit) + (synopsis "Coq's initialization") + (wrapped false) + (libraries coq.vernac) + ) diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib new file mode 100644 index 0000000000..6e86536648 --- /dev/null +++ b/sysinit/sysinit.mllib @@ -0,0 +1,4 @@ +Usage +Coqloadpath +Coqargs +Coqinit diff --git a/toplevel/usage.ml b/sysinit/usage.ml index 6fb5f821ee..1831a3f9b2 100644 --- a/toplevel/usage.ml +++ b/sysinit/usage.ml @@ -74,7 +74,6 @@ let print_usage_common co command = \n -debug debug mode (implies -bt)\ \n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ -\n -stm-debug STM debug mode (will trace every transaction)\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ diff --git a/toplevel/usage.mli b/sysinit/usage.mli index cbc3b4f7e8..2d1a8e94cc 100644 --- a/toplevel/usage.mli +++ b/sysinit/usage.mli @@ -26,4 +26,3 @@ type specific_usage = { given executable. } *) val print_usage : out_channel -> specific_usage -> unit - diff --git a/tactics/elim.ml b/tactics/elim.ml index 9a55cabc86..9e7843b2bb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -19,7 +19,6 @@ open Tacmach.New open Tacticals.New open Clenv open Tactics -open Proofview.Notations type branch_args = { branchnum : int; (* the branch number *) @@ -28,8 +27,6 @@ type branch_args = { true=assumption, false=let-in *) branchnames : Tactypes.intro_patterns} -module NamedDecl = Context.Named.Declaration - type elim_kind = Case of bool | Elim (* Find the right elimination suffix corresponding to the sort of the goal *) @@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l let h_decompose_or = decompose_or let h_decompose_and = decompose_and - -(* The tactic Double performs a double induction *) - -let induction_trailer abs_i abs_j bargs = - tclTHEN - (tclDO (abs_j - abs_i) intro) - (onLastHypId - (fun id -> - Proofview.Goal.enter begin fun gl -> - let idty = pf_get_type_of gl (mkVar id) in - let fvty = global_vars (pf_env gl) (project gl) idty in - let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs - in - let (hyps,_) = - List.fold_left - (fun (bring_ids,leave_ids) d -> - let cid = NamedDecl.get_id d in - if not (List.mem cid leave_ids) - then (d::bring_ids,leave_ids) - else (bring_ids,cid::leave_ids)) - ([],fvty) possible_bring_hyps - in - let ids = List.rev (ids_of_named_context hyps) in - (tclTHENLIST - [revert ids; elimination_then (fun _ -> tclIDTAC) id]) - end - )) - -let double_ind h1 h2 = - Proofview.Goal.enter begin fun gl -> - let abs_i = depth_of_quantified_hypothesis true h1 gl in - let abs_j = depth_of_quantified_hypothesis true h2 gl in - let abs = - if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else - if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else - let info = Exninfo.reify () in - tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in - abs >>= fun (abs_i,abs_j) -> - (tclTHEN (tclDO abs_i intro) - (onLastHypId - (fun id -> - elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) id))) - end - -let h_double_induction = double_ind - - diff --git a/tactics/elim.mli b/tactics/elim.mli index 01053502e4..a603b472f7 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option -> val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic val h_decompose_and : constr -> unit Proofview.tactic -val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d93f3bc434..c07073a91a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -77,11 +77,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic val intros : unit Proofview.tactic -(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in - the conclusion of goal [g], up to head-reduction if [b] is [true] *) -val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> Proofview.Goal.t -> int - val intros_until : quantified_hypothesis -> unit Proofview.tactic val intros_clearing : bool list -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v new file mode 100644 index 0000000000..cc25157b9b --- /dev/null +++ b/test-suite/bugs/closed/bug_13755.v @@ -0,0 +1,5 @@ +Module M1. +Lemma t1 : True. +Fail End M1. +Proof. exact I. Qed. +End M1. diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh new file mode 100755 index 0000000000..eef7786ebc --- /dev/null +++ b/test-suite/misc/non-marshalable-state.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/non-marshalable-state/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs +make src/good_plugin.cmxs + +RC=1 +# must fail +coqc -async-proofs on -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0 +# for this reason +grep -q 'Marshalling error' log1 || RC=1 + +# must work +coqc -async-proofs off -I src -Q theories Marshal theories/evil.v + +# must work +coqc -async-proofs on -I src -Q theories Marshal theories/good.v + + +exit $RC diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject new file mode 100644 index 0000000000..09e68d866c --- /dev/null +++ b/test-suite/misc/non-marshalable-state/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Marshal +-I src + +src/evil.mlg +src/good.mlg +src/evil_plugin.mlpack +src/good_plugin.mlpack +theories/evil.v +theories/good.v diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg new file mode 100644 index 0000000000..59b2b5a8ac --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil.mlg @@ -0,0 +1,15 @@ +DECLARE PLUGIN "evil_plugin" + +{ + +let state = Summary.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack new file mode 100644 index 0000000000..6382aa69e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack @@ -0,0 +1 @@ +Evil diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg new file mode 100644 index 0000000000..c6b9cbefd5 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good.mlg @@ -0,0 +1,16 @@ +DECLARE PLUGIN "good_plugin" + +{ + +let state = Summary.Local.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + let open Summary.Local in + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack new file mode 100644 index 0000000000..cd9dd73b78 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack @@ -0,0 +1 @@ +Good diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v new file mode 100644 index 0000000000..661482a975 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/evil.v @@ -0,0 +1,5 @@ +Declare ML Module "evil_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v new file mode 100644 index 0000000000..eab9a043e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/good.v @@ -0,0 +1,5 @@ +Declare ML Module "good_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v deleted file mode 100644 index 2ee8a0d184..0000000000 --- a/test-suite/output/SearchHead.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Some tests of the Search command *) - -SearchHead le. (* app nodes *) -SearchHead bool. (* no apps *) -SearchHead (@eq nat). (* complex pattern *) - -Definition newdef := fun x:nat => x = x. - -Goal forall n:nat, newdef n -> False. - intros n h. - SearchHead newdef. (* search hypothesis *) -Abort. - - -Goal forall n (P:nat -> Prop), P n -> False. - intros n P h. - SearchHead P. (* search hypothesis also for patterns *) -Abort. - diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out index 2f0d854ac6..24e2ee76af 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/Search_headconcl.out @@ -1,17 +1,9 @@ -File "stdin", line 3, characters 0-14: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] le_n: forall n : nat, n <= n le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m -File "stdin", line 4, characters 0-16: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] false: bool true: bool negb: bool -> bool @@ -35,10 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool Decimal.int_beq: Decimal.int -> Decimal.int -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool -File "stdin", line 5, characters 0-21: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -57,13 +45,5 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -File "stdin", line 11, characters 2-20: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: newdef n -File "stdin", line 17, characters 2-15: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: P n diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v new file mode 100644 index 0000000000..8b168dcd25 --- /dev/null +++ b/test-suite/output/Search_headconcl.v @@ -0,0 +1,18 @@ +(* Some tests of the Search command *) + +Search headconcl: le. (* app nodes *) +Search headconcl: bool. (* no apps *) +Search headconcl: (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + Search headconcl: newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + Search headconcl: P. (* search hypothesis also for patterns *) +Abort. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4983ee3c0d..615350c58c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -154,50 +154,6 @@ induction H. change (0 = z -> True) in IHrepr''. Abort. -(* Test double induction *) - -(* This was failing in 8.5 and before because of a bug in the order of - hypotheses *) - -Set Warnings "-deprecated". - -Inductive I2 : Type := - C2 : forall x:nat, x=x -> I2. -Goal forall a b:I2, a = b. -double induction a b. -Abort. - -(* This was leaving useless hypotheses in 8.5 and before because of - the same bug. This is a change of compatibility. *) - -Inductive I3 : Prop := - C3 : forall x:nat, x=x -> I3. -Goal forall a b:I3, a = b. -double induction a b. -Fail clear H. (* H should have been erased *) -Abort. - -(* This one had quantification in reverse order in 8.5 and before *) -(* This is a change of compatibility. *) - -Goal forall m n, le m n -> le n m -> n=m. -intros m n. double induction 1 2. -3:destruct 1. (* Should be "S m0 <= m0" *) -Abort. - -(* Idem *) - -Goal forall m n p q, le m n -> le p q -> n+p=m+q. -intros *. double induction 1 2. -3:clear H2. (* H2 should have been erased *) -Abort. - -(* This is unchanged *) - -Goal forall m n:nat, n=m. -double induction m n. -Abort. - (* Mentioned as part of bug #12944 *) Inductive test : Set := cons : forall (IHv : nat) (v : test), test. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index fce69437d7..d852ad24fe 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -319,7 +319,3 @@ Create HintDb program discriminated. Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. - -Definition obligation (A : Type) {a : A} := a. - -Register obligation as program.tactics.obligation. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 50aa658128..9cb3baf92c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -42,7 +42,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite"; + "Search"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index b75a4199ea..ca09bad441 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 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,9 +104,6 @@ let compile opts 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 stm_options = opts.config.stm_flags in let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand in @@ -129,9 +126,7 @@ let compile opts 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 @@ -181,8 +176,7 @@ let compile opts 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 @@ -209,22 +203,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 injections ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile 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 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 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 copts ~echo ~f_in ~f_out + compile opts stm_opts copts injections ~echo ~f_in ~f_out -let compile_files opts copts = +let compile_files (opts, stm_opts) copts injections = let compile_list = copts.compile_list in - List.iter (compile_file opts copts) compile_list + List.iter (compile_file opts stm_opts copts injections) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -248,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 8c154488d0..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 -> 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 03c53d6991..a403640149 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,30 +42,30 @@ coqc specific options:\ \n" } -let coqc_main copts ~opts = +let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files 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; 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; 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,12 +74,17 @@ 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, []); - help = coqc_specific_usage; - init = coqc_init; +let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel + = Coqtop.{ + 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 + let coqc_opts = Coqcargs.parse extras in + ((coqc_opts, 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/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 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let ( / ) s1 s2 = Filename.concat s1 s2 + +(* Loading of the resource file. + rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one + does not exist. *) + +let rcdefaultname = "coqrc" + +let load_rcfile ~rcfile ~state = + try + match rcfile with + | Some rcfile -> + 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d0d50aee70..caf86ef870 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,131 +143,15 @@ 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 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; - 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; +type query = PrintTags | PrintModUid of string list +type run_mode = Interactive | Batch | Query of query - (* Allow the user to load an arbitrary state here *) - inputstate opts.pre; - - (* 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 - 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 = +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 @@ -253,57 +160,70 @@ let init_document opts = *) (* 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 stm_options = opts.config.stm_flags 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 = - let state = init_document 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 ~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 - -let coqtop_parse_extra ~opts extras = - let rec parse_extra run_mode = function - | "-batch" :: rest -> parse_extra Batch rest + 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 extras = + let rec parse_extra run_mode = function + | "-batch" :: rest -> parse_extra Batch 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 - run_mode, 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 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 ~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 + | 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.{ @@ -317,8 +237,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 e535c19252..c675c6adec 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, @@ -28,18 +26,28 @@ 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 *) -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 -> 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 query = PrintTags | PrintModUid of string list +type run_mode = Interactive | Batch | Query of query + +type toplevel_options = { + run_mode : run_mode; + color_mode : color; +} -val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel +val coqtop_toplevel : (toplevel_options * 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/workerLoop.ml b/toplevel/workerLoop.ml index 59e10b09a0..e72940d189 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -8,10 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let worker_parse_extra ~opts extra_args = - (), 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 @@ -27,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; - run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); + 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 diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index af51f4fafb..1b811f3db7 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -105,12 +105,6 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let deprecated_searchhead = - CWarnings.create - ~name:"deprecated-searchhead" - ~category:"deprecated" - (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead.")) - let interp_search env sigma s r = let r = interp_search_restriction r in let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in @@ -138,9 +132,6 @@ let interp_search env sigma s r = (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchHead c -> - deprecated_searchhead (); - (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> Search.prioritize_search) pr_search); diff --git a/vernac/declare.ml b/vernac/declare.ml index c715304419..48aa329e5e 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -889,13 +889,6 @@ let add_hint local prg cst = let locality = if local then Goptions.OptLocal else Goptions.OptExport in Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst) -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true - ~key:["Hide"; "Obligations"] - ~value:false - let declare_obligation prg obl ~uctx ~types ~body = let poly = prg.prg_info.Info.poly in let univs = UState.univ_entry ~poly uctx in @@ -1046,51 +1039,10 @@ let obligation_substitution expand prg = let ints = intset_to (pred (Array.length obls)) in obl_substitution expand obls ints -let hide_obligation () = - Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; - UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref "program.tactics.obligation") - -(* XXX: Is this the right place? *) -let rec prod_app t n = - match - Constr.kind - (EConstr.Unsafe.to_constr - (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) - (* FIXME *) - with - | Prod (_, _, b) -> Vars.subst1 n b - | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n - | _ -> - CErrors.user_err ~hdr:"prod_app" - Pp.(str "Needed a product, but didn't find one" ++ fnl ()) - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let t, b = Id.List.assoc (destVar f) subst in - mkApp - ( delayed_force hide_obligation - , [|prod_applist t c'; Term.applistc b c'|] ) - with Not_found -> Constr.map aux c - else Constr.map aux c - in - Constr.map aux - let subst_prog subst prg = - if get_hide_obligations () then - ( replace_appvars subst prg.prg_body - , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ ) - else - let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in - ( Vars.replace_vars subst' prg.prg_body - , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ ) + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ ) let declare_definition ~pm prg = let varsubst = obligation_substitution true prg in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 5c329f60a9..f8a28332b1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -965,8 +965,6 @@ GRAMMAR EXTEND Gram (* Searching the environment *) | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> { fun g -> VernacPrint (PrintAbout (qid,l,g)) } - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> - { fun g -> VernacSearch (SearchHead c,g, l) } | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchPattern c,g, l) } | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index ff4365c8d3..8e5942440b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -242,7 +242,6 @@ let pr_search a gopt b pr_p = pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with - | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | Search sl -> diff --git a/vernac/search.ml b/vernac/search.ml index 501e5b1a91..98e231de19 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -185,14 +185,6 @@ let rec pattern_filter pat ref env sigma typ = | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ | _ -> false -let rec head_filter pat ref env sigma typ = - let typ = Termops.strip_outer_cast sigma typ in - if Constr_matching.is_matching_head env sigma pat typ then true - else match EConstr.kind sigma typ with - | Prod (_, _, typ) - | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ - | _ -> false - let full_name_of_reference ref = let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id @@ -274,19 +266,6 @@ let search_rewrite env sigma pat mods pr_search = (** Search *) -let search_by_head env sigma pat mods pr_search = - let filter ref kind env typ = - module_filter mods ref kind env sigma typ && - head_filter pat ref env sigma (EConstr.of_constr typ) && - blacklist_filter ref kind env sigma typ - in - let iter ref kind env typ = - if filter ref kind env typ then pr_search ref kind env typ - in - generic_search env iter - -(** Search *) - let search env sigma items mods pr_search = let filter ref kind env typ = let eqb b1 b2 = if b1 then b2 else not b2 in diff --git a/vernac/search.mli b/vernac/search.mli index 09847f4e03..6557aa5986 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -47,8 +47,6 @@ val search_filter : glob_search_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool - -> display_function -> unit val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool 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/stm/vernac_classifier.ml b/vernac/vernac_classifier.ml index ffae2866c0..ffae2866c0 100644 --- a/stm/vernac_classifier.ml +++ b/vernac/vernac_classifier.ml diff --git a/stm/vernac_classifier.mli b/vernac/vernac_classifier.mli index 61bf3a503a..61bf3a503a 100644 --- a/stm/vernac_classifier.mli +++ b/vernac/vernac_classifier.mli diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1c774a35bf..481bc3071b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1215,9 +1215,11 @@ let msg_of_subsection ss id = in Pp.str kind ++ spc () ++ Id.print id -let vernac_end_segment ~pm ({v=id} as lid) = +let vernac_end_segment ~pm ~stack ({v=id} as lid) = let ss = Lib.find_opening_node id in let what_for = msg_of_subsection ss lid.v in + if Option.has_some stack then + CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); Declare.Obls.check_solved_obligations ~pm ~what_for; match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid @@ -2173,9 +2175,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtNoProof(fun () -> vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> - VtReadProgram(fun ~pm -> + VtReadProgram(fun ~stack ~pm -> unsupported_attributes atts; - vernac_end_segment ~pm lid) + vernac_end_segment ~pm ~stack lid) | VernacNameSectionHypSet (lid, set) -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 2e360cf969..46acaf7264 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -75,7 +75,6 @@ type search_request = type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr - | SearchHead of constr_pattern_expr | Search of (bool * search_request) list type locatable = diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ed63332861..f320b65954 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -59,7 +59,7 @@ type typed_vernac = | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) - | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index e1e3b4cfe5..070c737882 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -77,7 +77,7 @@ type typed_vernac = | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) - | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 3a8a80d25a..e42775b76c 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -48,7 +48,7 @@ let interp_typed_vernac c ~pm ~stack = vernac_require_open_lemma ~stack (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate)); stack, pm - | VtReadProgram f -> f ~pm; stack, pm + | VtReadProgram f -> f ~stack ~pm; stack, pm | VtModifyProgram f -> let pm = f ~pm in stack, pm | VtDeclareProgram f -> |