diff options
32 files changed, 178 insertions, 219 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 529a912bb6..cbead97529 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -21,6 +21,7 @@ well. - [Support](#support) - [Standard libraries](#standard-libraries) - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) + - [Contributing to the editor support packages](#contributing-to-the-editor-support-packages) - [Contributing to the website or the package archive](#contributing-to-the-website-or-the-package-archive) - [Other ways of creating content](#other-ways-of-creating-content) - [Issues](#issues) @@ -208,6 +209,10 @@ manifesto's README][coq-community-manifesto]. ### Contributing to the editor support packages ### +Besides CoqIDE, whose sources are available in this repository, and to +which you are welcome to contribute, there are a number of alternative +user interfaces for Coq, more often as an editor support package. + Here are the URLs of the repositories of the various editor support packages: @@ -216,6 +221,11 @@ packages: - Coqtail (Vim) <https://github.com/whonore/Coqtail> - VsCoq Reloaded (VsCode) <https://github.com/coq-community/vscoq> +And here are alternative user interfaces to be run in the web browser: + +- JsCoq (Coq executed in your browser) <https://github.com/ejgallego/jscoq> +- Jupyter kernel for Coq <https://github.com/EugeneLoy/coq_jupyter/> + Each of them has their own contribution process. ### Contributing to the website or the package archive ### @@ -616,8 +626,26 @@ documentation][coqdoc-documentation] to learn more. ### Fixing bugs and performing small changes ### -Just open a PR with your fix. If it is not yet completed, do not -hesitate to open a [*draft PR*][GitHub-draft-PR] to get early +Before fixing a bug, it is best to check that it was reported before: + +- If it was already reported and you intend to fix it, self-assign the + issue (if you have the permission), or leave a comment marking your + intention to work on it (and a contributor with write-access may + then assign the issue to you). + +- If the issue already has an assignee, you should check with them if + they still intend to work on it. If the assignment is several + weeks, months, or even years (!) old, there are good chances that it + does not reflect their current priorities. + +- If the bug has not been reported before, it can be a good idea to + open an issue about it, while stating that you are preparing a fix. + The issue can be the place to discuss about the bug itself while the + PR will be the place to discuss your proposed fix. + +In any case, feel free to just ignore the recommendation above, and +jump ahead and open a PR with your fix. If it is not yet complete, do +not hesitate to open a [*draft PR*][GitHub-draft-PR] to get early feedback, and talk to developers on [Gitter][]. It is generally a good idea to add a regression test to the @@ -638,12 +666,12 @@ merged. So it is recommended that before spending a lot of time coding, you seek feedback from maintainers to see if your change would be -supported, and if they have recommendation about its implementation. +supported, and if they have recommendations about its implementation. You can do this informally by opening an issue, or more formally by producing a design document as a [Coq Enhancement Proposal][CEP]. Another recommendation is that you do not put several unrelated -changes (even if you produced them together) in the same PR. In +changes in the same PR (even if you produced them together). In particular, make sure you split bug fixes into separate PRs when this is possible. More generally, smaller-sized PRs, or PRs changing less components, are more likely to be reviewed and merged promptly. diff --git a/Makefile.build b/Makefile.build index d1ed9a6f96..610af5fe40 100644 --- a/Makefile.build +++ b/Makefile.build @@ -396,9 +396,8 @@ doc_gram_rsts: doc/tools/docgram/orderedGrammar ########################################################################### # Specific rules for Uint63 ########################################################################### -kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml - $(SHOW)'WRITE $@' - $(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<)) +kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml + rm -f $@ && cp $< $@ && chmod a-w $@ ########################################################################### # Main targets (coqtop.opt, coqtop.byte) @@ -642,12 +641,6 @@ gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack # Specific rules for gramlib to pack it Dune / OCaml 4.08 style GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) -gramlib/.pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49 -gramlib/.pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49 - -gramlib/.pack/gramlib.%: COND_OPENFLAGS= -gramlib/.pack/gramlib__%: COND_OPENFLAGS=-open Gramlib - gramlib/.pack/gramlib.cma: $(GRAMOBJS) gramlib/.pack/gramlib.cmo $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^ @@ -701,14 +694,15 @@ kernel/kernel.cmxa: kernel/kernel.mllib COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,) COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,) -# For module packing -COND_OPENFLAGS= +COND_GRAMFLAGS=$(if $(filter gramlib/.pack/%,$<),-no-alias-deps -w -49,) $(if $(filter gramlib/.pack/gramlib__%,$<),-open Gramlib,) + +COND_KERFLAGS=$(if $(filter kernel/%,$<),-w +a-4-44-50,) COND_BYTEFLAGS= \ - $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_OPENFLAGS) + $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS) COND_OPTFLAGS= \ - $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_OPENFLAGS) + $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS) plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' @@ -718,8 +712,6 @@ plugins/nsatz/%.cmi: plugins/nsatz/%.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -kernel/%.cmi: COND_BYTEFLAGS+=-w +a-4-44-50 - %.cmi: %.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -732,8 +724,6 @@ plugins/nsatz/%.cmo: plugins/nsatz/%.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -kernel/%.cmo: COND_BYTEFLAGS+=-w +a-4-44-50 - %.cmo: %.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -783,8 +773,6 @@ user-contrib/%.cmx: user-contrib/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< -kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 - %.cmx: %.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< diff --git a/Makefile.ide b/Makefile.ide index cb026cdf43..0a11f83a18 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -121,7 +121,7 @@ $(COQIDEBYTE): $(LINKIDE) ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile @rm -f $@ cp $< $@ - @chmod -w $@ + @chmod a-w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' diff --git a/configure.ml b/configure.ml index 3ced82718e..cef4faaf1a 100644 --- a/configure.ml +++ b/configure.ml @@ -1141,6 +1141,7 @@ let write_makefile f = pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; + pr "OCAML_INT_SIZE:=%d\n" Sys.int_size; pr "HASNATDYNLINK=%s\n\n" natdynlinkflag; pr "# Supplementary libs for some systems, currently:\n"; pr "# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n"; diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index f86cb0f6f2..ff0b90dcff 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -10,6 +10,9 @@ open Util module type GLexerType = Plexing.Lexer +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -27,8 +30,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules @@ -92,9 +93,6 @@ let tokens con = egram.gtokens; !list -type ty_norec = TyNoRec -type ty_mayrec = TyMayRec - type ('a, 'b, 'c) ty_and_rec = | NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec | MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 658baf1de9..9e48460206 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -19,6 +19,9 @@ module type GLexerType = Plexing.Lexer (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -36,8 +39,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 8d6a266c30..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -20,31 +20,21 @@ let open_glob_file f = let close_glob_file () = close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then + if dump () && !glob_output != Feedback then output_string !glob_file s let start_dump_glob ~vfile ~vofile = @@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 60d62a1cb2..2b6a116a01 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -8,19 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val open_glob_file : string -> unit -val close_glob_file : unit -> unit - val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -val noglob : unit -> unit -val dump_into_file : string -> unit (** special handling of "stdout" *) +type glob_output = + | NoGlob + | Feedback + | MultFiles (* one glob file per .v file *) + | File of string (* Single file for all coqc arguments *) -val dump_to_dotglob : unit -> unit -val feedback_glob : unit -> unit +(* Default "NoGlob" *) +val set_glob_output : glob_output -> unit val pause : unit -> unit val continue : unit -> unit diff --git a/kernel/dune b/kernel/dune index 4038bf5638..5f7502ef6b 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) (libraries lib byterun dynlink)) (executable @@ -16,7 +16,7 @@ (rule (targets uint63.ml) - (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) (documentation diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 5542716af2..d22ba3468f 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + type t val uint_size : int diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_31.ml index b8eccd19fb..b8eccd19fb 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_31.ml diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_63.ml index 5c4028e1c8..5c4028e1c8 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_63.ml diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml deleted file mode 100644 index 57a170c8f5..0000000000 --- a/kernel/write_uint63.ml +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -(** Equivalent of rm -f *) -let safe_remove f = - try Unix.chmod f 0o644; Sys.remove f with _ -> () - -(** * Generate an implementation of 63-bit arithmetic *) -let ml_file_copy input output = - safe_remove output; - let i = open_in input in - let o = open_out output in - let pr s = Printf.fprintf o s in - pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n"; - pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n"; - try - while true do - output_string o (input_line i); output_char o '\n' - done - with End_of_file -> - close_in i; - close_out o; - Unix.chmod output 0o444 - -let write_uint63 () = - ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" - else (* 64 bits *) "uint63_amd64_63.ml") - "uint63.ml" - -let () = write_uint63 () diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 60c8fb4449..b241fdc6cc 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t val aux_file_name_for : string -> string val start_aux_file : aux_file:string -> v_file:string -> unit -val stop_aux_file : unit -> unit +val stop_aux_file : unit -> unit val recording : unit -> bool val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 190de5853d..f09dc48f5d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let record_aux_file = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 1c96796220..185a5f8425 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,10 +31,6 @@ (** Command-line flags *) -(** Set by coqtop to tell the kernel to output to the aux file; will - be eventually removed by cleanups such as PR#1103 *) -val record_aux_file : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/parsing/extend.ml b/parsing/extend.ml index 63e121c0d1..ed6ebe5aed 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -79,8 +79,10 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) -type norec = NoRec (* just two *) -type mayrec = MayRec (* incompatible types *) +(* Should be merged with gramlib's implementation *) + +type norec = Gramlib.Grammar.ty_norec +type mayrec = Gramlib.Grammar.ty_mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol @@ -107,15 +109,3 @@ and 'a rules = type 'a production_rule = | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3aaba27579..e0d63a723e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -131,73 +131,57 @@ end (** Binding general entry keys to symbol *) -type ('s, 'trec, 'a, 'r) casted_rule = -| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule -| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule - -type ('s, 'trec, 'a) casted_symbol = -| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol -| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol - -let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol = +let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol = function -| Atoken t -> CastedSNo (G.s_token t) +| Atoken t -> G.s_token t | Alist1 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1 s) - | CastedSMay s -> CastedSMay (G.s_list1 s) end + let s = symbol_of_prod_entry_key s in + G.s_list1 s | Alist1sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list1sep s sep false | Alist0 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0 s) - | CastedSMay s -> CastedSMay (G.s_list0 s) end + let s = symbol_of_prod_entry_key s in + G.s_list0 s | Alist0sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list0sep s sep false | Aopt s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_opt s) - | CastedSMay s -> CastedSMay (G.s_opt s) end -| Aself -> CastedSMay G.s_self -| Anext -> CastedSMay G.s_next -| Aentry e -> CastedSNo (G.s_nterm e) -| Aentryl (e, n) -> CastedSNo (G.s_nterml e n) + let s = symbol_of_prod_entry_key s in + G.s_opt s +| Aself -> G.s_self +| Anext -> G.s_next +| Aentry e -> G.s_nterm e +| Aentryl (e, n) -> G.s_nterml e n | Arules rs -> let warning msg = Feedback.msg_warning Pp.(str msg) in - CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)) + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) -and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function -| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc) +and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function +| Stop -> + G.r_stop | Next (r, s) -> - begin match symbol_of_rule r, symbol_of_prod_entry_key s with - | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next r s | NextNoRec (r, s) -> - let CastedRNo (r, cast) = symbol_of_rule r in - let CastedSNo s = symbol_of_prod_entry_key s in - CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x))) + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next_norec r s and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function | Rules (r, act) -> - let CastedRNo (symb, cast) = symbol_of_rule r in - G.rules (symb, cast act) + let symb = symbol_of_rule r in + G.rules (symb,act) (** FIXME: This is a hack around a deficient camlp5 API *) type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> - match symbol_of_rule toks with - | CastedRNo (symb, cast) -> AnyProduction (symb, cast act) - | CastedRMay (symb, cast) -> AnyProduction (symb, cast act) + AnyProduction (symbol_of_rule toks, act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, assoc, List.map of_coq_production_rule rule) @@ -215,6 +199,18 @@ let fix_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + type extend_rule = | ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule @@ -462,11 +458,10 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end + let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = - let r = - match symbol_of_prod_entry_key e with - | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) - | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in + let s = symbol_of_prod_entry_key e in + let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7efeab6ba0..10f78a5a72 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -212,8 +212,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) -val grammar_extend : 'a Entry.t -> gram_reinit option -> - 'a Extend.extend_statement -> unit +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + +val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 94af4a3151..ba759441e5 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -189,31 +189,32 @@ let flatten_contravariant_disj _ ist = tclTHEN (tclTHENLIST tacs) tac0 | _ -> fail -let make_unfold name = - let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in - let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in - Locus.(AllOccurrences, ArgArg (EvalConstRef const, None)) +let evalglobref_of_globref = + function + | GlobRef.VarRef v -> EvalVarRef v + | GlobRef.ConstRef c -> EvalConstRef c + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> assert false -let u_not = make_unfold "not" +let make_unfold name = + let const = evalglobref_of_globref (Coqlib.lib_ref name) in + Locus.(AllOccurrences, ArgArg (const, None)) let reduction_not_iff _ ist = let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in let tac = match !negation_unfolding with - | true -> make_reduce [u_not] + | true -> make_reduce [make_unfold "core.not.type"] | false -> TacId [] in eval_tactic_ist ist tac -let coq_nnpp_path = - let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in - Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP") - let apply_nnpp _ ist = + let nnpp = "core.nnpp.type" in Proofview.tclBIND (Proofview.tclUNIT ()) - begin fun () -> try - Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply - with Not_found -> tclFAIL 0 (Pp.mt ()) + begin fun () -> + if Coqlib.has_ref nnpp + then Tacticals.New.pf_constr_of_global (Coqlib.lib_ref nnpp) >>= apply + else tclFAIL 0 (Pp.mt ()) end (* This is the uniform mode dealing with ->, not, iff and types isomorphic to diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - diff --git a/tactics/declare.ml b/tactics/declare.ml index c280760e84..c23ee4a76e 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -224,7 +224,7 @@ let cast_opaque_proof_entry e = let vars = global_vars_set env pf in ids_typ, vars in - let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in + let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in keep_hyps env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0c0a1897a8..296c253363 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -822,4 +822,4 @@ Defined. Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b'). Proof. destruct b, b'; now constructor. -Qed. +Defined. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 6af7b1fe6e..9c47b73193 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -26,6 +26,8 @@ unfold not; intros; elim (classic p); auto. intro NP; elim (H NP). Qed. +Register NNPP as core.nnpp.type. + (** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. Thanks to [forall P, False -> P], it is equivalent to the following form *) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index d8a3dbb4bb..fe5361c156 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -108,8 +108,6 @@ let compile opts copts ~echo ~f_in ~f_out = in match copts.compilation_mode with | BuildVo -> - Flags.record_aux_file := true; - let long_f_dot_v, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".v" ".vo" in @@ -124,8 +122,11 @@ let compile opts copts ~echo ~f_in ~f_out = Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); + + Dumpglob.set_glob_output copts.glob_out; Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); + let wall_clock1 = Unix.gettimeofday () in let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in @@ -139,9 +140,6 @@ let compile opts copts ~echo ~f_in ~f_out = Dumpglob.end_dump_glob () | BuildVio -> - Flags.record_aux_file := false; - Dumpglob.noglob (); - let long_f_dot_v, long_f_dot_vio = ensure_exists_with_prefix f_in f_out ".v" ".vio" in @@ -174,9 +172,6 @@ let compile opts copts ~echo ~f_in ~f_out = Stm.reset_task_queue () | Vio2Vo -> - - Flags.record_aux_file := false; - Dumpglob.noglob (); let long_f_dot_vio, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".vio" ".vo" in let sum, lib, univs, tasks, proofs = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 67d70416c8..64c1da20b6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -59,7 +59,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } @@ -125,7 +124,6 @@ let default_config = { debug = false; diffs_set = false; time = false; - glob_opt = false; print_emacs = false; set_options = []; @@ -380,13 +378,6 @@ let parse_args ~help ~init arglist : t * string list = Flags.compat_version := v; add_compat_require oval v - |"-dump-glob" -> - Dumpglob.dump_into_file (next ()); - { oval with config = { oval.config with glob_opt = true }} - - |"-feedback-glob" -> - Dumpglob.feedback_glob (); oval - |"-exclude-dir" -> System.exclude_directory (next ()); oval @@ -524,7 +515,6 @@ let parse_args ~help ~init arglist : t * string list = |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = 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; }} diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index e414888861..26f22386a0 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -35,7 +35,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 5678acb2b1..019577ac85 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -16,8 +16,7 @@ let outputstate opts = let coqc_init _copts ~opts = Flags.quiet := true; System.trust_file_cache := true; - Coqtop.init_color opts.Coqargs.config; - if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () + Coqtop.init_color opts.Coqargs.config let coqc_specific_usage = Usage.{ executable_name = "coqc"; diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 5cced2baac..0b5481fe72 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -23,7 +23,8 @@ type t = ; echo : bool - ; outputstate : string option; + ; outputstate : string option + ; glob_out : Dumpglob.glob_output } let default = @@ -40,6 +41,7 @@ let default = ; echo = false ; outputstate = None + ; glob_out = Dumpglob.MultFiles } let depr opt = @@ -187,6 +189,15 @@ let parse arglist : t = | "-outputstate" -> set_outputstate oval (next ()) + (* Glob options *) + |"-no-glob" | "-noglob" -> + { oval with glob_out = Dumpglob.NoGlob } + + |"-dump-glob" -> + let file = next () in + { oval with glob_out = Dumpglob.File file } + + (* Rest *) | s -> extras := s :: !extras; oval diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index b02eeeb9ee..13bea3bf3e 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -24,6 +24,7 @@ type t = ; echo : bool ; outputstate : string option + ; glob_out : Dumpglob.glob_output } val default : t diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 78640334e2..07466d641e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -438,19 +438,15 @@ let rec loop ~state = loop ~state (* Default toplevel loop *) -let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) let drop_args = ref None + let loop ~opts ~state = drop_args := Some opts; let open Coqargs in print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; let _ = loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 094e2c1184..cfb3248c7b 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip = str "should start with one of the following commands:"++spc()++ v 0 ( prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - if !Flags.record_aux_file + if Aux_file.recording () then let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in record_proof_using s |