diff options
73 files changed, 718 insertions, 428 deletions
diff --git a/.gitignore b/.gitignore index bf7430cc2e..1abead3c67 100644 --- a/.gitignore +++ b/.gitignore @@ -115,6 +115,9 @@ doc/stdlib/index-body.html doc/stdlib/index-list.html doc/tools/docgram/editedGrammar doc/tools/docgram/prodnGrammar +doc/tools/docgram/prodnCommands +doc/tools/docgram/prodnTactics +doc/tools/docgram/updated_rsts doc/unreleased.rst # .mll files diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ce6be777f3..52b03e455b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -20,7 +20,7 @@ variables: # Format: $IMAGE-V$DATE-$hash # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g. # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10) - CACHEKEY: "bionic_coq-V2021-02-11-b601de5a7b" + CACHEKEY: "bionic_coq-V2021-04-14-802aebab96" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/Makefile.build b/Makefile.build index d619fd3c85..cbd4f4efbe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -893,7 +893,7 @@ PLUGININCLUDES=$(addprefix -I plugins/, $(PLUGINDIRS)) $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### diff --git a/checker/values.ml b/checker/values.ml index f7a367b986..1353435181 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -87,7 +87,7 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|] (** kernel/univ *) -let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|] +let v_level_global = v_tuple "Level.Global.t" [|v_dp;String;Int|] let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *) [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] diff --git a/clib/cThread.ml b/clib/cThread.ml index 89ca2f7d83..3796fdf788 100644 --- a/clib/cThread.ml +++ b/clib/cThread.ml @@ -107,3 +107,22 @@ let mask_sigalrm f x = let create f x = Thread.create (mask_sigalrm f) x + +(* + Atomic mutex lock taken from https://gitlab.com/gadmm/memprof-limits/-/blob/master/src/thread_map.ml#L23-34 + Critical sections : + - Mutex.lock does not poll on leaving the blocking section + since 4.12. + - Never inline, to avoid theoretically-possible reorderings with + flambda. + (workaround to the lack of masking) +*) + +(* We inline the call to Mutex.unlock to avoid polling in bytecode mode *) +external unlock: Mutex.t -> unit = "caml_mutex_unlock" + +let[@inline never] with_lock m ~scope = + let () = Mutex.lock m (* BEGIN ATOMIC *) in + match (* END ATOMIC *) scope () with + | (* BEGIN ATOMIC *) x -> unlock m ; (* END ATOMIC *) x + | (* BEGIN ATOMIC *) exception e -> unlock m ; (* END ATOMIC *) raise e diff --git a/clib/cThread.mli b/clib/cThread.mli index 87889f3356..d974135d43 100644 --- a/clib/cThread.mli +++ b/clib/cThread.mli @@ -29,3 +29,8 @@ val thread_friendly_really_read_line : thread_ic -> string (* Wrapper around Thread.create that blocks signals such as Sys.sigalrm (used * for Timeout *) val create : ('a -> 'b) -> 'a -> Thread.t + +(* + Atomic mutex lock taken from https://gitlab.com/gadmm/memprof-limits/-/blob/master/src/thread_map.ml#L23-34 +*) +val with_lock : Mutex.t -> scope:(unit -> 'a) -> 'a diff --git a/clib/exninfo.ml b/clib/exninfo.ml index 07b7f47529..4c1f47df30 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -71,10 +71,9 @@ let record_backtrace b = let get_backtrace e = get e backtrace_info let iraise (e,i) = - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let () = current := (id, (e,i)) :: remove_assoc id !current in - let () = Mutex.unlock lock in + CThread.with_lock lock ~scope:(fun () -> + let id = Thread.id (Thread.self ()) in + current := (id, (e,i)) :: remove_assoc id !current); match get i backtrace_info with | None -> raise e @@ -82,12 +81,11 @@ let iraise (e,i) = Printexc.raise_with_backtrace e bt let find_and_remove () = - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let (v, l) = find_and_remove_assoc id !current in - let () = current := l in - let () = Mutex.unlock lock in - v + CThread.with_lock lock ~scope:(fun () -> + let id = Thread.id (Thread.self ()) in + let (v, l) = find_and_remove_assoc id !current in + let () = current := l in + v) let info e = let (src, data) = find_and_remove () in diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh index 1b2d6a73a2..d2e0ee89bf 100755 --- a/dev/ci/ci-paramcoq.sh +++ b/dev/ci/ci-paramcoq.sh @@ -5,7 +5,4 @@ ci_dir="$(dirname "$0")" git_download paramcoq -# Typically flaky on our worker configuration -# https://gitlab.com/coq/coq/-/jobs/1144081161 -export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8f14625c63..00729cd168 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc, pytest for coqtail -RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ +RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ pytest==5.4.3 @@ -44,7 +44,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.13.0" + BASE_ONLY_OPAM="elpi.1.13.1" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh new file mode 100644 index 0000000000..d1606711dc --- /dev/null +++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh @@ -0,0 +1 @@ +overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050 diff --git a/dev/ci/user-overlays/14111-gares-update-elpi.sh b/dev/ci/user-overlays/14111-gares-update-elpi.sh new file mode 100644 index 0000000000..8827127a38 --- /dev/null +++ b/dev/ci/user-overlays/14111-gares-update-elpi.sh @@ -0,0 +1,2 @@ +overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.5 14111 +overlay hierarchy_builder https://github.com/math-comp/hierarchy-builder coq-master+1.1.0 14111 diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst new file mode 100644 index 0000000000..9753ce915b --- /dev/null +++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow scope delimiters in Ltac2 open_constr:(...) quotation + (`#13939 <https://github.com/coq/coq/pull/13939>`_, + fixes `#12806 <https://github.com/coq/coq/issues/12806>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 <https://github.com/coq/coq/pull/14093>`_, + fixes `#14092 <https://github.com/coq/coq/issues/14092>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst new file mode 100644 index 0000000000..355c0bd7b7 --- /dev/null +++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst @@ -0,0 +1,8 @@ +- **Changed:** + ``coqdep`` now reports an error if files specified on the + command line don't exist or if it encounters unreadable files. + Unknown options now generate a warning. Previously these + conditions were ignored. + (`#14024 <https://github.com/coq/coq/pull/14024>`_, + fixes `#14023 <https://github.com/coq/coq/issues/14023>`_, + by Hendrik Tews). diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 2a618f68d2..a4850a738b 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -69,7 +69,7 @@ } .ansi-fg-white { - color: #2e3436; + color: #ffffff; } .ansi-fg-light-black { diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9f097b4fe9..abe928fa26 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -5,7 +5,7 @@ The underlying formal language of Coq is a :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related -work are provided in a separate chapter; see *Credits*. +work are provided in a separate chapter; see :ref:`history`. .. _The-terms: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 294c56ef06..25ac72069b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1375,8 +1375,9 @@ table further down lists the classes that that are handled plainly. the term (as described in :ref:`LocalInterpretationRulesForNotations`). The last :token:`scope_key` is the top of the scope stack that's applied to the :token:`term`. - :n:`open_constr` - Parses an open :token:`term`. + :n:`open_constr {? ( {+, @scope_key } ) }` + Parses an open :token:`term`. Like :n:`constr` above, this class + accepts a list of notation scopes with the same effects. :n:`ident` Parses :token:`ident` or :n:`$@ident`. The first form returns :n:`ident:(@ident)`, diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -467,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 9e23be2409..6700c20b1a 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -91,7 +91,10 @@ def parse_ansi(code): leading ‘^[[’ or the final ‘m’ """ classes = [] - parse_style([int(c) for c in code.split(';')], 0, classes) + if code == "37": + pass # ignore white fg + else: + parse_style([int(c) for c in code.split(';')], 0, classes) return ["ansi-" + cls for cls in classes] if __name__ == '__main__': diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ab1a9d4c75..0c8980b1bd 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1778,7 +1778,6 @@ simple_tactic: [ | "zify_iter_let" tactic (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5b19b7fc55..40bb980e90 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1856,7 +1856,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) diff --git a/engine/univGen.ml b/engine/univGen.ml index 278ca6bf34..b917d91512 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,14 +13,14 @@ open Names open Constr open Univ -type univ_unique_id = int (* Generator of levels *) -let new_univ_id, set_remote_new_univ_id = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> n) +let new_univ_id = + let cnt = ref 0 in + fun () -> incr cnt; !cnt let new_univ_global () = - Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) + let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in + Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ()) let fresh_level () = Univ.Level.make (new_univ_global ()) diff --git a/engine/univGen.mli b/engine/univGen.mli index 05737411f5..743d819747 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -13,12 +13,6 @@ open Constr open Environ open Univ - -(** The global universe counter *) -type univ_unique_id -val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer -val new_univ_id : unit -> univ_unique_id (** for the stm *) - (** Side-effecting functions creating new universe levels. *) val new_univ_global : unit -> Level.UGlobal.t diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 83c158e057..fd3ff25fc1 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -129,10 +129,12 @@ let tokens con = egram.gtokens; !list +(** Used to propagate possible presence of SELF/NEXT in a rule (binary and) *) type ('a, 'b, 'c) ty_and_rec = | NoRec2 : (norec, norec, norec) ty_and_rec | MayRec2 : ('a, 'b, mayrec) ty_and_rec +(** Used to propagate possible presence of SELF/NEXT in a tree (ternary and) *) type ('a, 'b, 'c, 'd) ty_and_rec3 = | NoRec3 : (norec, norec, norec, norec) ty_and_rec3 | MayRec3 : ('a, 'b, 'c, mayrec) ty_and_rec3 @@ -167,6 +169,7 @@ and ('self, 'trec, 'a) ty_symbol = | Sself : ('self, mayrec, 'self) ty_symbol | Snext : ('self, mayrec, 'self) ty_symbol | Snterm : 'a ty_entry -> ('self, norec, 'a) ty_symbol + (* norec but the entry can nevertheless introduce a loop with the current entry*) | Snterml : 'a ty_entry * string -> ('self, norec, 'a) ty_symbol | Stree : ('self, 'trec, Loc.t -> 'a) ty_tree -> ('self, 'trec, 'a) ty_symbol @@ -346,8 +349,11 @@ let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree = fun ar symbols pf tree action -> match symbols, pf with - TCns (ars, s, sl), RelS pf -> insert_in_tree ar ars s sl pf tree action + TCns (ars, s, sl), RelS pf -> + (* descent in tree at symbol [s] *) + insert_in_tree ar ars s sl pf tree action | TNil, Rel0 -> + (* insert the action *) let node (type tb) ({node = s; son = son; brother = bro} : (_, _, _, tb, _, _) ty_node) = let ar : (norec, tb, tb) ty_and_ex = match get_rec_tree bro with MayRec -> NR10 | NoRec -> NR11 in @@ -381,43 +387,56 @@ let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and | MayRec2, _, NoRec -> Node (MayRec3, node NR11) | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11) and try_insert : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_rec -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree option = - fun ar ars s sl pf tree action -> + fun ar ars symb symbl pf tree action -> match tree with - Node (arn, {node = s1; son = son; brother = bro}) -> - begin match eq_symbol s s1 with + Node (arn, {node = symb1; son = son; brother = bro}) -> + (* merging rule [symb; symbl -> action] in tree [symb1; son | bro] *) + begin match eq_symbol symb symb1 with | Some Refl -> - let MayRecNR arss = and_symbols_tree sl son in - let son = insert arss sl pf son action in - let node = {node = s1; son = son; brother = bro} in + (* reducing merge of [symb; symbl -> action] with [symb1; son] to merge of [symbl -> action] with [son] *) + let MayRecNR arss = and_symbols_tree symbl son in + let son = insert arss symbl pf son action in + let node = {node = symb1; son = son; brother = bro} in + (* propagate presence of SELF/NEXT *) begin match ar, ars, arn, arss with | MayRec2, _, _, _ -> Some (Node (MayRec3, node)) | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end | None -> let ar' = and_and_tree ar arn bro in - if is_before s1 s || derive_eps s && not (derive_eps s1) then + if is_before symb1 symb || derive_eps symb && not (derive_eps symb1) then + (* inserting new rule after current rule, i.e. in [bro] *) let bro = - match try_insert ar' ars s sl pf bro action with - Some bro -> bro + match try_insert ar' ars symb symbl pf bro action with + Some bro -> + (* could insert in [bro] *) + bro | None -> - let MayRecNR arss = and_symbols_tree sl DeadEnd in - let son = insert arss sl pf DeadEnd action in - let node = {node = s; son = son; brother = bro} in + (* not ok to insert in [bro] or after; we insert now *) + let MayRecNR arss = and_symbols_tree symbl DeadEnd in + let son = insert arss symbl pf DeadEnd action in + let node = {node = symb; son = son; brother = bro} in + (* propagate presence of SELF/NEXT *) match ar, ars, arn, arss with | MayRec2, _, _, _ -> Node (MayRec3, node) | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node) in - let node = {node = s1; son = son; brother = bro} in + let node = {node = symb1; son = son; brother = bro} in + (* propagate presence of SELF/NEXT *) match ar, arn with | MayRec2, _ -> Some (Node (MayRec3, node)) | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) else - match try_insert ar' ars s sl pf bro action with + (* should insert in [bro] or before the tree [symb1; son | bro] *) + match try_insert ar' ars symb symbl pf bro action with Some bro -> - let node = {node = s1; son = son; brother = bro} in + (* could insert in [bro] *) + let node = {node = symb1; son = son; brother = bro} in begin match ar, arn with | MayRec2, _ -> Some (Node (MayRec3, node)) | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end - | None -> None + | None -> + (* should insert before [symb1; son | bro] *) + None end | LocAct (_, _) -> None | DeadEnd -> None in @@ -470,6 +489,7 @@ let is_level_labelled n (Level lev) = let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = match symbols with | TCns (_, Sself, symbols) -> + (* Insert a rule of the form "SELF; ...." *) let Level slev = slev in let RelS pf = pf in let MayRecTree lsuffix = insert_tree entry_name symbols pf action slev.lsuffix in @@ -478,6 +498,7 @@ let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (p lsuffix = lsuffix; lprefix = slev.lprefix} | _ -> + (* Insert a rule not starting with SELF *) let Level slev = slev in let MayRecTree lprefix = insert_tree entry_name symbols pf action slev.lprefix in Level @@ -1097,27 +1118,51 @@ let skip_if_empty bp p strm = if Stream.count strm == bp then fun a -> p strm else raise Stream.Failure -let continue entry bp a s son p1 (strm__ : _ Stream.t) = - let a = (entry_of_symb entry s).econtinue 0 bp a strm__ in +let continue entry bp a symb son p1 (strm__ : _ Stream.t) = + let a = (entry_of_symb entry symb).econtinue 0 bp a strm__ in let act = try p1 strm__ with - Stream.Failure -> raise (Stream.Error (tree_failed entry a s son)) + Stream.Failure -> raise (Stream.Error (tree_failed entry a symb son)) in fun _ -> act a -let do_recover parser_of_tree entry nlevn alevn bp a s son +(** Recover from a success on [symb] with result [a] followed by a + failure on [son] in a rule of the form [a = symb; son] *) +let do_recover parser_of_tree entry nlevn alevn bp a symb son (strm__ : _ Stream.t) = - try parser_of_tree entry nlevn alevn (top_tree entry son) strm__ with + try + (* Try to replay the son with the top occurrence of NEXT (by + default at level nlevn) and trailing SELF (by default at alevn) + replaced with self at top level; + This allows for instance to recover from a failure on the + second SELF of « SELF; "\/"; SELF » by doing as if it were + « SELF; "\/"; same-entry-at-top-level » with application e.g. to + accept "A \/ forall x, x = x" w/o requiring the expected + parentheses as in "A \/ (forall x, x = x)". *) + parser_of_tree entry nlevn alevn (top_tree entry son) strm__ + with Stream.Failure -> try + (* Discard the rule if what has been consumed before failing is + the empty sequence (due to some OPT or LIST0); example: + « OPT "!"; ident » fails to see an ident and the OPT was resolved + into the empty sequence, with application e.g. to being able to + safely write « LIST1 [ OPT "!"; id = ident -> id] ». *) skip_if_empty bp (fun (strm__ : _ Stream.t) -> raise Stream.Failure) strm__ with Stream.Failure -> - continue entry bp a s son (parser_of_tree entry nlevn alevn son) + (* In case of success on just SELF, NEXT or an explicit call to + a subentry followed by a failure on the rest (son), retry + parsing as if this entry had been called at its toplevel; + example: « "{"; entry-at-some-level; "}" » fails on "}" and + is retried with « "{"; same-entry-at-top-level; "}" », allowing + e.g. to parse « {1 + 1} » while « {(1 + 1)} » would + have been expected according to the level. *) + continue entry bp a symb son (parser_of_tree entry nlevn alevn son) strm__ -let recover parser_of_tree entry nlevn alevn bp a s son strm = - do_recover parser_of_tree entry nlevn alevn bp a s son strm +let recover parser_of_tree entry nlevn alevn bp a symb son strm = + do_recover parser_of_tree entry nlevn alevn bp a symb son strm let token_count = ref 0 @@ -1143,15 +1188,22 @@ let token_ematch gram tok = let tematch = L.tok_match tok in fun tok -> tematch tok +(** + nlevn: level for Snext + alevn: level for recursive calls on the left-hand side of the rule (depending on associativity) +*) + let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_tree -> r parser_t = fun entry nlevn alevn -> function DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure) | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act) | Node (_, {node = Sself; son = LocAct (act, _); brother = DeadEnd}) -> + (* SELF on the right-hand side of the last rule *) (fun (strm__ : _ Stream.t) -> let a = entry.estart alevn strm__ in act a) | Node (_, {node = Sself; son = LocAct (act, _); brother = bro}) -> + (* SELF on the right-hand side of a rule *) let p2 = parser_of_tree entry nlevn alevn bro in (fun (strm__ : _ Stream.t) -> match @@ -1394,6 +1446,33 @@ and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser fun entry symb -> parser_of_symbol entry 0 (top_symb entry symb) +(** [start_parser_of_levels entry clevn levels levn strm] goes + top-down from level [clevn] to the last level, ignoring rules + between [levn] and [clevn], as if starting from + [max(clevn,levn)]. On each rule of the form [prefix] (where + [prefix] is a rule not starting with [SELF]), it tries to consume + the stream [strm]. + + The interesting case is [entry.estart] which is + [start_parser_of_levels entry 0 entry.edesc], thus practically + going from [levn] to the end. + + More schematically, assuming each level has the form + + level n: [ a = SELF; b = suffix_tree_n -> action_n(a,b) + | a = prefix_tree_n -> action'_n(a) ] + + then the main loop does the following: + + estart n = + if prefix_tree_n matches the stream as a then econtinue n (action'_n(a)) + else start (n+1) + + econtinue n a = + if suffix_tree_n matches the stream as b then econtinue n (action_n(a,b)) + else if n=0 then a else econtinue (n-1) a +*) + let rec start_parser_of_levels entry clevn = function [] -> (fun levn (strm__ : _ Stream.t) -> raise Stream.Failure) @@ -1426,7 +1505,9 @@ let rec start_parser_of_levels entry clevn = entry.econtinue levn bp a strm) | _ -> fun levn strm -> - if levn > clevn then p1 levn strm + if levn > clevn then + (* Skip rules before [levn] *) + p1 levn strm else let (strm__ : _ Stream.t) = strm in let bp = Stream.count strm__ in @@ -1437,6 +1518,18 @@ let rec start_parser_of_levels entry clevn = entry.econtinue levn bp a strm | _ -> p1 levn strm__ +(** [continue_parser_of_levels entry clevn levels levn bp a strm] goes + bottom-up from the last level to level [clevn], ignoring rules + between [levn] and [clevn], as if stopping at [max(clevn,levn)]. + It tries to consume the stream [strm] on the suffix of rules of + the form [SELF; suffix] knowing that [a] is what consumed [SELF] + at level [levn] (or [levn+1] depending on associativity). + + The interesting case is [entry.econtinue levn bp a] which is [try + continue_parser_of_levels entry 0 entry.edesc levn bp a with + Failure -> a], thus practically going from the end to [levn]. +*) + let rec continue_parser_of_levels entry clevn = function [] -> (fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure) @@ -1452,7 +1545,9 @@ let rec continue_parser_of_levels entry clevn = in let p2 = parser_of_tree entry (succ clevn) alevn tree in fun levn bp a strm -> - if levn > clevn then p1 levn bp a strm + if levn > clevn then + (* Skip rules before [levn] *) + p1 levn bp a strm else let (strm__ : _ Stream.t) = strm in try p1 levn bp a strm__ with diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 20e9f0134f..dc616066c2 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -538,7 +538,7 @@ struct let implicit = BoolOpt ["Printing"; "Implicit"] let coercions = BoolOpt ["Printing"; "Coercions"] - let raw_matching = BoolOpt ["Printing"; "Matching"] + let nested_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] @@ -553,8 +553,8 @@ struct let bool_items = [ { opts = [implicit]; init = false; label = "Display _implicit arguments" }; { opts = [coercions]; init = false; label = "Display _coercions" }; - { opts = [raw_matching]; init = true; - label = "Display raw _matching expressions" }; + { opts = [nested_matching]; init = true; + label = "Display nested _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; { opts = [parentheses]; init = false; label = "Display _parentheses" }; { opts = [all_basic]; init = false; diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml index 6e02d7fed1..3a080d5f51 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -93,7 +93,6 @@ let commands = [ ]; ["Read Module"; "Record"; - "Variant"; "Remark"; "Remove LoadPath"; "Remove Printing Constructor"; diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index badfabf07e..82eca905ea 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -77,7 +77,7 @@ let init () = \n <separator/>\ \n <menuitem action='Display implicit arguments' />\ \n <menuitem action='Display coercions' />\ -\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display nested matching expressions' />\ \n <menuitem action='Display notations' />\ \n <menuitem action='Display parentheses' />\ \n <menuitem action='Display all basic low-level contents' />\ diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 72b54d329f..0a0b932c46 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -489,11 +489,11 @@ let eval_call c = let print_xml = let m = Mutex.create () in fun oc xml -> - Mutex.lock m; - if !Flags.xml_debug then - Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); - try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m - with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e + CThread.with_lock m ~scope:(fun () -> + if !Flags.xml_debug then + Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); + try Control.protect_sigalrm (Xml_printer.print oc) xml + with e -> let e = Exninfo.capture e in Exninfo.iraise e) let slave_feeder fmt xml_oc msg = let xml = Xmlprotocol.(of_feedback fmt msg) in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6cb61174d3..ddbd5fa0a7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -717,7 +717,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) +let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) "" 0)) let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = let anon = Context.make_annot Anonymous Sorts.Relevant in diff --git a/kernel/univ.ml b/kernel/univ.ml index a2fd14025e..c2496f10b0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -38,20 +38,22 @@ struct open Names module UGlobal = struct - type t = DirPath.t * int + type t = DirPath.t * string * int - let make dp i = (DirPath.hcons dp,i) + let make dp s i = (DirPath.hcons dp,s,i) let repr x : t = x - let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' + let equal (d, s, i) (d', s', i') = Int.equal i i' && DirPath.equal d d' && String.equal s s' - let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d) + let hash (d,s,i) = Hashset.Combine.combine3 i (String.hash s) (DirPath.hash d) - let compare (d, i) (d', i') = - let c = Int.compare i i' in - if Int.equal c 0 then DirPath.compare d d' - else c + let compare (d, s, i) (d', s', i') = + if i < i' then -1 + else if i' < i then 1 + else let c = DirPath.compare d d' in + if not (Int.equal c 0) then c + else String.compare s s' end type t = @@ -84,10 +86,7 @@ struct | Set, Set -> 0 | Set, _ -> -1 | _, Set -> 1 - | Level (dp1, i1), Level (dp2, i2) -> - if i1 < i2 then -1 - else if i1 > i2 then 1 - else DirPath.compare dp1 dp2 + | Level l1, Level l2 -> UGlobal.compare l1 l2 | Level _, _ -> -1 | _, Level _ -> 1 | Var n, Var m -> Int.compare n m @@ -98,8 +97,8 @@ struct | SProp, SProp -> true | Prop, Prop -> true | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' + | Level (d,s,n), Level (d',s',n') -> + n == n' && s==s' && d == d' | Var n, Var n' -> n == n' | _ -> false @@ -107,9 +106,10 @@ struct | SProp as x -> x | Prop as x -> x | Set as x -> x - | Level (d,n) as x -> + | Level (d,s,n) as x -> + let s' = CString.hcons s in let d' = Names.DirPath.hcons d in - if d' == d then x else Level (d',n) + if s' == s && d' == d then x else Level (d',s',n) | Var _n as x -> x open Hashset.Combine @@ -119,7 +119,7 @@ struct | Prop -> combinesmall 1 1 | Set -> combinesmall 1 2 | Var n -> combinesmall 2 n - | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + | Level l -> combinesmall 3 (UGlobal.hash l) end @@ -200,7 +200,10 @@ module Level = struct | SProp -> "SProp" | Prop -> "Prop" | Set -> "Set" - | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (d,s,n) -> + Names.DirPath.to_string d ^ + (if CString.is_empty s then "" else "." ^ s) ^ + "." ^ string_of_int n | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -218,7 +221,7 @@ module Level = struct let name u = match data u with - | Level (d, n) -> Some (d, n) + | Level l -> Some l | _ -> None end diff --git a/kernel/univ.mli b/kernel/univ.mli index 7286fc84cb..eeaa1ad62d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -15,8 +15,8 @@ sig module UGlobal : sig type t - val make : Names.DirPath.t -> int -> t - val repr : t -> Names.DirPath.t * int + val make : Names.DirPath.t -> string -> int -> t + val repr : t -> Names.DirPath.t * string * int val equal : t -> t -> bool val hash : t -> int val compare : t -> t -> int diff --git a/lib/future.ml b/lib/future.ml index 23d089fb6b..247b139798 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -112,8 +112,8 @@ let create_delegate ?(blocking=true) ~name fix_exn = if not blocking then (fun () -> raise (NotReady name)), ignore else let lock = Mutex.create () in let cond = Condition.create () in - (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), - (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.wait cond lock)), + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.broadcast cond)) in let ck = create ~name ~fix_exn (Delegated wait) in ck, assignment signal ck diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml deleted file mode 100644 index 5e1150146e..0000000000 --- a/lib/remoteCounter.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -type remote_counters_status = (string * Obj.t) list - -let counters : remote_counters_status ref = ref [] - -let (!!) x = !(!x) - -let new_counter ~name a ~incr ~build = - assert(not (List.mem_assoc name !counters)); - let data = ref (ref a) in - counters := (name, Obj.repr data) :: !counters; - let m = Mutex.create () in - let mk_thsafe_local_getter f () = - (* - slaves must use a remote counter getter, not this one! *) - (* - in the main process there is a race condition between slave - managers (that are threads) and the main thread, hence the mutex *) - if Flags.async_proofs_is_worker () then - CErrors.anomaly(Pp.str"Slave processes must install remote counters."); - Mutex.lock m; let x = f () in Mutex.unlock m; - build x in - let mk_thsafe_remote_getter f () = - Mutex.lock m; let x = f () in Mutex.unlock m; x in - let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in - let installer f = - if not (Flags.async_proofs_is_worker ()) then - CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); - getter := mk_thsafe_remote_getter f in - (fun () -> !getter ()), installer - -let backup () = !counters - -let snapshot () = - List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters - -let restore l = - List.iter (fun (name, data) -> - assert(List.mem_assoc name !counters); - let dataref = Obj.obj (List.assoc name !counters) in - !dataref := !!(Obj.obj data)) - l diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli deleted file mode 100644 index 42d1f8a8d1..0000000000 --- a/lib/remoteCounter.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -(* Remote counters are *global* counters for fresh ids. In the master/slave - * scenario, the slave installs a getter that asks the master for a fresh - * value. In the scenario of a slave that runs after the death of the master - * on some marshalled data, a backup of all counters status should be taken and - * restored to avoid reusing ids. - * Counters cannot be created by threads, they must be created once and forall - * as toplevel module declarations. *) - - -type 'a getter = unit -> 'a -type 'a installer = ('a getter) -> unit - -val new_counter : name:string -> - 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer - -type remote_counters_status -val backup : unit -> remote_counters_status -(* like backup but makes a copy so that further increment does not alter - * the snapshot *) -val snapshot : unit -> remote_counters_status -val restore : remote_counters_status -> unit diff --git a/man/coqdep.1 b/man/coqdep.1 index bb6b20c0bb..5ca558b7c5 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -70,6 +70,21 @@ Output dependencies for .vos files (this is not the default as it breaks dune's .B \-boot For coq developers, prints dependencies over coq library files (omitted by default). +.TP +.B \-noinit +Currently no effect. + + +.SH EXIT STATUS +.IP "1" +A file given on the command line cannot be found or some file +cannot be opened. +.IP "0" +In all other cases. In particular, when a dependency cannot be +found or an invalid option is encountered, +.B coqdep +prints a warning and exits with status +.B 0\fR. .SH SEE ALSO diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 53aa619d10..1018271751 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) = in List.map snd (List.filter has_mon bounds) @ snd l +let bound_monomials = tr_sys "bound_monomials" bound_monomials + let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth; @@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys = It would only be safe if the variable is linear... *) let sys1 = - elim_simple_linear_equality (WithProof.subst_constant true sys) + normalise + (elim_simple_linear_equality (WithProof.subst_constant true sys)) in + let bnd1 = bound_monomials sys1 in let sys2 = saturate_by_linear_equalities sys1 in - let sys3 = nlinear_preprocess (sys1 @ sys2) in + let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in let sys4 = make_cstr_system (*sys2@*) sys3 in (* [reduction_equations] is too brutal - there should be some non-linear reasoning *) xlia (List.map fst sys) enum reduction_equations sys4 diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 74b0708743..d18065088c 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -24,17 +24,17 @@ let warn_deprecated_Spec = DECLARE PLUGIN "zify_plugin" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF -| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } -| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t } -| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t } -| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t } -| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } -| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } -| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } -| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "Zify" "InjTyp" reference(t) ] -> { Zify.InjTable.register t } +| ["Add" "Zify" "BinOp" reference(t) ] -> { Zify.BinOp.register t } +| ["Add" "Zify" "UnOp" reference(t) ] -> { Zify.UnOp.register t } +| ["Add" "Zify" "CstOp" reference(t) ] -> { Zify.CstOp.register t } +| ["Add" "Zify" "BinRel" reference(t) ] -> { Zify.BinRel.register t } +| ["Add" "Zify" "PropOp" reference(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropBinOp" reference(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropUOp" reference(t) ] -> { Zify.PropUnOp.register t } +| ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register t } +| ["Add" "Zify" "UnOpSpec" reference(t) ] -> { Zify.UnOpSpec.register t } +| ["Add" "Zify" "Saturate" reference(t) ] -> { Zify.Saturate.register t } END TACTIC EXTEND ITER diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 800dc6cee2..b780c1833e 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -23,6 +23,19 @@ let zify str = (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref ("ZifyClasses." ^ str))) +(** classes *) +let coq_InjTyp = lazy (Coqlib.lib_ref "ZifyClasses.InjTyp") + +let coq_BinOp = lazy (Coqlib.lib_ref "ZifyClasses.BinOp") +let coq_UnOp = lazy (Coqlib.lib_ref "ZifyClasses.UnOp") +let coq_CstOp = lazy (Coqlib.lib_ref "ZifyClasses.CstOp") +let coq_BinRel = lazy (Coqlib.lib_ref "ZifyClasses.BinRel") +let coq_PropBinOp = lazy (Coqlib.lib_ref "ZifyClasses.PropBinOp") +let coq_PropUOp = lazy (Coqlib.lib_ref "ZifyClasses.PropUOp") +let coq_BinOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.BinOpSpec") +let coq_UnOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.UnOpSpec") +let coq_Saturate = lazy (Coqlib.lib_ref "ZifyClasses.Saturate") + (* morphism like lemma *) let mkapp2 = lazy (zify "mkapp2") @@ -46,7 +59,7 @@ let op_iff_morph = lazy (zify "iff_morph") let op_not = lazy (zify "not") let op_not_morph = lazy (zify "not_morph") let op_True = lazy (zify "True") -let whd = Reductionops.clos_whd_flags CClosure.all +let op_I = lazy (zify "I") (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. This is useful for calling Constr.hash *) @@ -59,6 +72,7 @@ let gl_pr_constr e = let evd = Evd.from_env genv in pr_constr genv evd e +let whd = Reductionops.clos_whd_flags CClosure.all let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2) (** [get_type_of] performs beta reduction ; @@ -344,6 +358,7 @@ module type Elt = sig (** name *) val name : string + val gref : GlobRef.t Lazy.t val table : (term_kind * decl_kind) ConstrMap.t ref val cast : elt decl -> decl_kind val dest : decl_kind -> elt decl option @@ -375,6 +390,7 @@ module EInj = struct type elt = EInjT.t let name = "EInj" + let gref = coq_InjTyp let table = table let cast x = InjTyp x let dest = function InjTyp x -> Some x | _ -> None @@ -432,6 +448,7 @@ module EBinOp = struct open EBinOpT let name = "BinOp" + let gref = coq_BinOp let table = table let mk_elt evd i a = @@ -473,6 +490,7 @@ module ECstOp = struct open ECstOpT let name = "CstOp" + let gref = coq_CstOp let table = table let cast x = CstOp x let dest = function CstOp x -> Some x | _ -> None @@ -499,6 +517,7 @@ module EUnOp = struct open EUnOpT let name = "UnOp" + let gref = coq_UnOp let table = table let cast x = UnOp x let dest = function UnOp x -> Some x | _ -> None @@ -531,6 +550,7 @@ module EBinRel = struct open EBinRelT let name = "BinRel" + let gref = coq_BinRel let table = table let cast x = BinRel x let dest = function BinRel x -> Some x | _ -> None @@ -557,6 +577,7 @@ module EPropBinOp = struct open EPropBinOpT let name = "PropBinOp" + let gref = coq_PropBinOp let table = table let cast x = PropOp x let dest = function PropOp x -> Some x | _ -> None @@ -569,7 +590,8 @@ module EPropUnOp = struct open EPropUnOpT - let name = "PropUnOp" + let name = "PropUOp" + let gref = coq_PropUOp let table = table let cast x = PropUnOp x let dest = function PropUnOp x -> Some x | _ -> None @@ -580,7 +602,7 @@ end let constr_of_term_kind = function Application c -> c | OtherTerm c -> c module type S = sig - val register : Constrexpr.constr_expr -> unit + val register : Libnames.qualid -> unit val print : unit -> unit end @@ -612,7 +634,7 @@ module MakeTable (E : Elt) = struct let c = EConstr.of_constr c in let t = get_type_of env evd c in match EConstr.kind evd t with - | App (intyp, args) -> + | App (intyp, args) when EConstr.isRefX evd (Lazy.force E.gref) intyp -> let styp = args.(E.get_key) in let elt = {decl = c; deriv = make_elt (evd, c)} in register_hint evd styp elt @@ -621,10 +643,11 @@ module MakeTable (E : Elt) = struct raise (CErrors.user_err Pp.( - str ": Cannot register term " - ++ pr_constr env evd c ++ str ". It has type " - ++ pr_constr env evd t - ++ str " which should be of the form [F X1 .. Xn]")) + str "Cannot register " ++ pr_constr env evd c + ++ str ". It has type " ++ pr_constr env evd t + ++ str " instead of type " + ++ Printer.pr_global (Lazy.force E.gref) + ++ str " X1 ... Xn")) let register_obj : Constr.constr -> Libobject.obj = let cache_constr (_, c) = @@ -638,17 +661,19 @@ module MakeTable (E : Elt) = struct ("register-zify-" ^ E.name) ~cache:cache_constr ~subst:(Some subst_constr) - (** [register c] is called from the VERNACULAR ADD [name] constr(t). + (** [register c] is called from the VERNACULAR ADD [name] reference(t). The term [c] is interpreted and registered as a [superglobal_object_nodischarge]. TODO: pre-compute [get_type_of] - [cache_constr] is using another environment. *) let register c = - let env = Global.env () in - let evd = Evd.from_env env in - let evd, c = Constrintern.interp_open_constr env evd c in - let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in - () + try + let c = UnivGen.constr_of_monomorphic_global (Nametab.locate c) in + let _ = Lib.add_anonymous_leaf (register_obj c) in + () + with Not_found -> + raise + (CErrors.user_err Pp.(Libnames.pr_qualid c ++ str " does not exist.")) let pp_keys () = let env = Global.env () in @@ -672,6 +697,7 @@ module ESat = struct open ESatT let name = "Saturate" + let gref = coq_Saturate let table = saturate let cast x = Saturate x let dest = function Saturate x -> Some x | _ -> None @@ -685,6 +711,7 @@ module EUnopSpec = struct type elt = ESpecT.t let name = "UnopSpec" + let gref = coq_UnOpSpec let table = specs let cast x = UnOpSpec x let dest = function UnOpSpec x -> Some x | _ -> None @@ -698,6 +725,7 @@ module EBinOpSpec = struct type elt = ESpecT.t let name = "BinOpSpec" + let gref = coq_BinOpSpec let table = specs let cast x = BinOpSpec x let dest = function BinOpSpec x -> Some x | _ -> None @@ -1511,41 +1539,51 @@ let spec_of_hyps = let iter_specs = spec_of_hyps let find_hyp evd t l = - try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)) + try + Some + (EConstr.mkVar + (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))) with Not_found -> None -let sat_constr c d = - Proofview.Goal.enter (fun gl -> - let evd = Tacmach.New.project gl in - let env = Tacmach.New.pf_env gl in - let hyps = Tacmach.New.pf_hyps_types gl in - match EConstr.kind evd c with - | App (c, args) -> - if Array.length args = 2 then - let h1 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) - in - let h2 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) - in - match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with - | Some h1, Some h2 -> - let n = - Tactics.fresh_id_in_env Id.Set.empty - (Names.Id.of_string "__sat") - env - in - let trm = - EConstr.mkApp - ( d.ESatT.satOK - , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] ) - in - Tactics.pose_proof (Names.Name n) trm - | _, _ -> Tacticals.New.tclIDTAC - else Tacticals.New.tclIDTAC - | _ -> Tacticals.New.tclIDTAC) +let find_proof evd t l = + if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I) + else find_hyp evd t l + +(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where + - sub' is a fresh subscript obtained from sub + - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c' + - hyps' is obtained from hyps' + taclist and hyps are threaded to avoid adding duplicates + *) +let sat_constr env evd (sub,taclist, hyps) c d = + match EConstr.kind evd c with + | App (c, args) -> + if Array.length args = 2 then + let h1 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) + in + let h2 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) + in + let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in + let trm = + match (find_proof evd h1 hyps, find_proof evd h2 hyps) with + | Some h1, Some h2 -> + (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|])) + | Some h1, _ -> + EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|]) + | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|]) + in + let rtrm = Tacred.cbv_beta env evd trm in + let typ = Retyping.get_type_of env evd rtrm in + match find_hyp evd typ hyps with + | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps) + | Some _ -> (sub, taclist, hyps) + else (sub,taclist,hyps) + | _ -> (sub,taclist,hyps) + let get_all_sat env evd c = List.fold_left @@ -1569,8 +1607,10 @@ let saturate = Array.iter sat args; if Array.length args = 2 then let ds = get_all_sat env evd c in - if ds = [] then () - else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds + if ds = [] || CstrTable.HConstr.mem table t + then () + else List.iter (fun x -> + CstrTable.HConstr.add table t x.deriv) ds else () | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous -> sat t1; sat t2 @@ -1579,5 +1619,6 @@ let saturate = (* Collect all the potential saturation lemma *) sat concl; List.iter (fun (_, t) -> sat t) hyps; - Tacticals.New.tclTHENLIST - (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table [])) + let s0 = fresh_subscript env in + let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in + Tacticals.New.tclTHENLIST tacs) diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 555bb4c7fb..68f23393ee 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -7,10 +7,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Constrexpr module type S = sig - val register : constr_expr -> unit + val register : Libnames.qualid -> unit val print : unit -> unit end diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index dd80ff21aa..a9f203014f 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -56,12 +56,8 @@ module Make(T : Task) () = struct type response = | Response of T.response | RespFeedback of Feedback.feedback - | RespGetCounterNewUnivLevel type request = Request of T.request - type more_data = - | MoreDataUnivLevel of UnivGen.univ_unique_id list - let slave_respond (Request r) = let res = T.perform r in Response res @@ -94,16 +90,6 @@ module Make(T : Task) () = struct with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("unmarshal_response: "^s) - let marshal_more_data oc (res : more_data) = - try marshal_to_channel oc res - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_more_data: "^s) - - let unmarshal_more_data ic = - try (CThread.thread_friendly_input_value ic : more_data) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_more_data: "^s) - let report_status ?(id = !Flags.async_proofs_worker_id) s = let open Feedback in feedback ~id:Stateid.initial (WorkerStatus(id, s)) @@ -198,8 +184,6 @@ module Make(T : Task) () = struct | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in - let more_univs n = - CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -231,9 +215,6 @@ module Make(T : Task) () = struct marshal_request oc (Request req); let rec continue () = match unmarshal_response ic with - | RespGetCounterNewUnivLevel -> - marshal_more_data oc (MoreDataUnivLevel (more_univs 10)); - continue () | RespFeedback fbk -> T.forward_feedback fbk; continue () | Response resp -> match T.use_response !worker_age task resp with @@ -315,13 +296,6 @@ module Make(T : Task) () = struct let ic, oc = Spawned.get_channels () in slave_oc := Some oc; slave_ic := Some ic - let bufferize f = - let l = ref [] in - fun () -> - match !l with - | [] -> let data = f () in l := List.tl data; List.hd data - | x::tl -> l := tl; x - let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) @@ -339,11 +313,6 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc) () in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); - (* We ask master to allocate universe identifiers *) - UnivGen.set_remote_new_univ_id (bufferize @@ Control.protect_sigalrm (fun () -> - marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; - match unmarshal_more_data (Option.get !slave_ic) with - | MoreDataUnivLevel l -> l)); let working = ref false in slave_handshake (); while true do diff --git a/stm/stm.ml b/stm/stm.ml index 9480bbdc2e..6287943cee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -98,8 +98,7 @@ let forward_feedback, forward_feedback_hook = let m = Mutex.create () in Hook.make ~default:(function | { doc_id = did; span_id = id; route; contents } -> - try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m - with e -> Mutex.unlock m; raise e) () + CThread.with_lock m ~scope:(fun () -> feedback ~did ~id ~route contents)) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () @@ -758,17 +757,16 @@ end = struct (* {{{ *) let worker = ref None let set_last_job j = - Mutex.lock m; - job := Some j; - Condition.signal c; - Mutex.unlock m + CThread.with_lock m ~scope:(fun () -> + job := Some j; + Condition.signal c) let get_last_job () = - Mutex.lock m; - while Option.is_empty !job do Condition.wait c m; done; - match !job with - | None -> assert false - | Some x -> job := None; Mutex.unlock m; x + CThread.with_lock m ~scope:(fun () -> + while Option.is_empty !job do Condition.wait c m; done; + match !job with + | None -> assert false + | Some x -> job := None; x) let run_command () = try while true do get_last_job () () done @@ -2449,24 +2447,21 @@ let join ~doc = VCS.print (); doc -let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () - -type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status -let check_task name (tasks,rcbackup) i = - RemoteCounter.restore rcbackup; +type tasks = int Slaves.tasks +let check_task name tasks i = let vcs = VCS.backup () in try let rc = State.purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false -let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u p (t,rcbackup as tasks) = - RemoteCounter.restore rcbackup; +let info_tasks = Slaves.info_tasks + +let finish_tasks name u p tasks = let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u p t) i in + let u = State.purify (Slaves.finish_task name u p tasks) i in VCS.restore vcs; u in try @@ -2517,13 +2512,13 @@ let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, below, [snapshot] gets computed even if [create_vos] is true. *) - let (tasks,counters) = dump_snapshot() in + let tasks = Slaves.dump_snapshot() in let except = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in let todo_proofs = if create_vos then Library.ProofsTodoSomeEmpty except - else Library.ProofsTodoSome (except,tasks,counters) + else Library.ProofsTodoSome (except,tasks) in Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 2aaca85582..f5bd726dde 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -68,61 +68,54 @@ let create () = { let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) tq = let { queue = q; lock = m; cond = c; cond_waiting = cn } = tq in - Mutex.lock m; - if tq.release then (Mutex.unlock m; raise BeingDestroyed); - while not (PriorityQueue.exists picky q || !destroy) do - tq.nwaiting <- tq.nwaiting + 1; - Condition.broadcast cn; - Condition.wait c m; - tq.nwaiting <- tq.nwaiting - 1; - if tq.release || !destroy then (Mutex.unlock m; raise BeingDestroyed) - done; - if !destroy then (Mutex.unlock m; raise BeingDestroyed); - let x = PriorityQueue.pop ~picky q in - Condition.signal c; - Condition.signal cn; - Mutex.unlock m; - x + CThread.with_lock m ~scope:(fun () -> + if tq.release then raise BeingDestroyed; + while not (PriorityQueue.exists picky q || !destroy) do + tq.nwaiting <- tq.nwaiting + 1; + Condition.broadcast cn; + Condition.wait c m; + tq.nwaiting <- tq.nwaiting - 1; + if tq.release || !destroy then raise BeingDestroyed + done; + if !destroy then raise BeingDestroyed; + let x = PriorityQueue.pop ~picky q in + Condition.signal c; + Condition.signal cn; + x) let broadcast tq = let { lock = m; cond = c } = tq in - Mutex.lock m; - Condition.broadcast c; - Mutex.unlock m + CThread.with_lock m ~scope:(fun () -> + Condition.broadcast c) let push tq x = let { queue = q; lock = m; cond = c; release } = tq in if release then CErrors.anomaly(Pp.str "TQueue.push while being destroyed! Only 1 producer/destroyer allowed."); - Mutex.lock m; - PriorityQueue.push q x; - Condition.broadcast c; - Mutex.unlock m + CThread.with_lock m ~scope:(fun () -> + PriorityQueue.push q x; + Condition.broadcast c) let length tq = let { queue = q; lock = m } = tq in - Mutex.lock m; - let n = PriorityQueue.length q in - Mutex.unlock m; - n + CThread.with_lock m ~scope:(fun () -> + PriorityQueue.length q) let clear tq = let { queue = q; lock = m; cond = c } = tq in - Mutex.lock m; - PriorityQueue.clear q; - Mutex.unlock m + CThread.with_lock m ~scope:(fun () -> + PriorityQueue.clear q) let clear_saving tq f = let { queue = q; lock = m; cond = c } = tq in - Mutex.lock m; let saved = ref [] in - while not (PriorityQueue.is_empty q) do - let elem = PriorityQueue.pop q in - match f elem with - | Some x -> saved := x :: !saved - | None -> () - done; - Mutex.unlock m; + CThread.with_lock m ~scope:(fun () -> + while not (PriorityQueue.is_empty q) do + let elem = PriorityQueue.pop q in + match f elem with + | Some x -> saved := x :: !saved + | None -> () + done); List.rev !saved let is_empty tq = PriorityQueue.is_empty tq.queue @@ -130,32 +123,28 @@ let is_empty tq = PriorityQueue.is_empty tq.queue let destroy tq = tq.release <- true; while tq.nwaiting > 0 do - Mutex.lock tq.lock; - Condition.broadcast tq.cond; - Mutex.unlock tq.lock; + CThread.with_lock tq.lock ~scope:(fun () -> + Condition.broadcast tq.cond) done; tq.release <- false let wait_until_n_are_waiting_and_queue_empty j tq = - Mutex.lock tq.lock; - while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do - Condition.wait tq.cond_waiting tq.lock - done; - Mutex.unlock tq.lock + CThread.with_lock tq.lock ~scope:(fun () -> + while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do + Condition.wait tq.cond_waiting tq.lock + done) let wait_until_n_are_waiting_then_snapshot j tq = let l = ref [] in - Mutex.lock tq.lock; - while not (PriorityQueue.is_empty tq.queue) do - l := PriorityQueue.pop tq.queue :: !l - done; - while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done; - List.iter (PriorityQueue.push tq.queue) (List.rev !l); - if !l <> [] then Condition.broadcast tq.cond; - Mutex.unlock tq.lock; + CThread.with_lock tq.lock ~scope:(fun () -> + while not (PriorityQueue.is_empty tq.queue) do + l := PriorityQueue.pop tq.queue :: !l + done; + while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done; + List.iter (PriorityQueue.push tq.queue) (List.rev !l); + if !l <> [] then Condition.broadcast tq.cond); List.rev !l let set_order tq rel = - Mutex.lock tq.lock; - PriorityQueue.set_rel rel tq.queue; - Mutex.unlock tq.lock + CThread.with_lock tq.lock ~scope:(fun () -> + PriorityQueue.set_rel rel tq.queue) diff --git a/stm/workerPool.ml b/stm/workerPool.ml index 45c92c3748..fef9300377 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -72,12 +72,7 @@ let worker_handshake slave_ic slave_oc = exit 1 let locking { lock; pool = p } f = - try - Mutex.lock lock; - let x = f p in - Mutex.unlock lock; - x - with e -> Mutex.unlock lock; raise e + CThread.with_lock lock ~scope:(fun () -> f p) let rec create_worker extra pool priority id = let cancel = ref false in diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v new file mode 100644 index 0000000000..ee221d33a6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12806.v @@ -0,0 +1,9 @@ +Require Import Ltac2.Ltac2. + +Declare Scope my_scope. +Delimit Scope my_scope with my_scope. + +Notation "###" := tt : my_scope. + +Ltac2 Notation "bar" c(open_constr(my_scope)) := c. +Ltac2 Eval bar ###. diff --git a/test-suite/micromega/bug_11656.v b/test-suite/micromega/bug_11656.v new file mode 100644 index 0000000000..19846ad50a --- /dev/null +++ b/test-suite/micromega/bug_11656.v @@ -0,0 +1,11 @@ +Require Import Lia. +Require Import NArith. +Open Scope N_scope. + +Goal forall (a b c: N), + a <> 0 -> + c <> 0 -> + a * ((b + 1) * c) <> 0. +Proof. + intros. nia. +Qed. diff --git a/test-suite/micromega/bug_12184.v b/test-suite/micromega/bug_12184.v new file mode 100644 index 0000000000..d329a3fa7f --- /dev/null +++ b/test-suite/micromega/bug_12184.v @@ -0,0 +1,8 @@ +Require Import Lia. +Require Import ZArith. + +Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z. +Proof. + intros p. + lia. +Qed. diff --git a/test-suite/micromega/bug_14054.v b/test-suite/micromega/bug_14054.v new file mode 100644 index 0000000000..d97e13375f --- /dev/null +++ b/test-suite/micromega/bug_14054.v @@ -0,0 +1,46 @@ +(* bug 13242 *) + +Require Import Lia. +Fail Add Zify InjTyp id. + +(* bug 14054 *) + +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. +Require Coq.Init.Byte . +Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia. + +Notation byte := Coq.Init.Byte.byte. + +Module byte. + Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b). +End byte. + +Section WithA. + Context (A: Type). + Fixpoint tuple(n: nat): Type := + match n with + | O => unit + | S m => A * tuple m + end. +End WithA. + +Module LittleEndian. + Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z := + match n with + | O => fun _ => 0 + | S n => fun bs => Z.lor (byte.unsigned (fst bs)) + (Z.shiftl (combine n (snd bs)) 8) + end. + Lemma combine_bound: forall {n: nat} (t: tuple byte n), + 0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n). + Admitted. +End LittleEndian. + +Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {| + inj := LittleEndian.combine n; + pred x := 0 <= x < 2 ^ (8 * Z.of_nat n); + cstr := @LittleEndian.combine_bound n; +|}. +Fail Add Zify InjTyp InjByteTuple. +Fail Add Zify UnOp InjByteTuple. +Fail Add Zify UnOp X. diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index d70bb809c6..d22e2b7c8c 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -12,6 +12,12 @@ Open Scope Z_scope. Require Import ZMicromega. Require Import VarMap. +Lemma power_pos : forall x y, 0 <= x \/ False -> x^ y >= 0. +Proof. + intros. + lia. +Qed. + Lemma not_so_easy : forall x n : Z, 2*x + 1 <= 2 *n -> x <= n-1. Proof. diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v index 485c24f0c9..e79b76b810 100644 --- a/test-suite/micromega/example_nia.v +++ b/test-suite/micromega/example_nia.v @@ -7,10 +7,16 @@ (************************************************************************) Require Import ZArith. -Require Import Psatz. Open Scope Z_scope. -Require Import ZMicromega. +Require Import ZMicromega Lia. Require Import VarMap. +Unset Nia Cache. + +Goal forall (x y: Z), 0 < (1+y^2)^(x^2). +Proof. nia. Qed. + +Goal forall (x y: Z), 0 <= (y^2)^x. +Proof. nia. Qed. (* false in Q : x=1/2 and n=1 *) @@ -347,8 +353,8 @@ Lemma hol_light17 : forall x y, -> x * y * (x + y) <= x ^ 2 + y ^ 2. Proof. intros. - Fail nia. -Abort. + nia. +Qed. Lemma hol_light18 : forall x y, @@ -507,3 +513,24 @@ Proof. intros. lia. Qed. + +Lemma mult : forall x x0 x1 x2 n n0 n1 n2, + 0 <= x -> 0 <= x0 -> 0 <= x1 -> 0 <= x2 -> + 0 <= n -> 0 <= n0 -> 0 <= n1 -> 0 <= n2 -> + (n1 * x <= n2 * x1) -> + (n * x0 <= n0 * x2) -> + (n1 * n * (x * x0) > n2 * n0 * (x1 * x2)) -> False. +Proof. + intros. + nia. +Qed. + + +Lemma mult_nat : forall x x0 x1 x2 n n0 n1 n2, + (n1 * x <= n2 * x1)%nat -> + (n * x0 <= n0 * x2)%nat -> + (n1 * n * (x * x0) > n2 * n0 * (x1 * x2))%nat -> False. +Proof. + intros. + nia. +Qed. diff --git a/test-suite/misc/vio_checking.sh b/test-suite/misc/vio_checking.sh new file mode 100755 index 0000000000..ffa909e93b --- /dev/null +++ b/test-suite/misc/vio_checking.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +set -ex + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc + +rm -f vio_checking{,bad}.{vo,vio} + +coqc -vio vio_checking.v +coqc -vio vio_checking_bad.v + +coqc -schedule-vio-checking 2 vio_checking.vio + +if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then + echo 'vio-checking on vio_checking_bad.vio should have failed!' + exit 1 +fi +if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then + echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!' + exit 1 +fi + +coqc -vio2vo vio_checking.vio +coqchk -silent vio_checking.vo + +if coqc -vio2vo vio_checking_bad.vio; then + echo 'vio2vo on vio_checking_bad.vio should have failed!' + exit 1 +fi diff --git a/test-suite/misc/vio_checking.v b/test-suite/misc/vio_checking.v new file mode 100644 index 0000000000..8dd5e47383 --- /dev/null +++ b/test-suite/misc/vio_checking.v @@ -0,0 +1,9 @@ + +Lemma foo : Type. +Proof. exact Type. Qed. + +Lemma foo1 : Type. +Proof. exact Type. Qed. + +Lemma foo2 : Type. +Proof. exact foo1. Qed. diff --git a/test-suite/misc/vio_checking_bad.v b/test-suite/misc/vio_checking_bad.v new file mode 100644 index 0000000000..f32d06f34a --- /dev/null +++ b/test-suite/misc/vio_checking_bad.v @@ -0,0 +1,4 @@ +(* a file to check that vio-checking is not a noop *) + +Lemma foo : Type. +Proof. match goal with |- ?G => exact G end. Qed. diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index bbdf9762a3..a530c34297 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,4 +1,3 @@ - Require Import Lia ZArith. (* Submitted by Xavier Urbain 18 Jan 2002 *) diff --git a/test-suite/success/RemoteUnivs.v b/test-suite/success/RemoteUnivs.v new file mode 100644 index 0000000000..5ab4937dda --- /dev/null +++ b/test-suite/success/RemoteUnivs.v @@ -0,0 +1,31 @@ + + +Goal Type * Type. +Proof. + split. + par: exact Type. +Qed. + +Goal Type. +Proof. + exact Type. +Qed. + +(* (* coqide test, note the delegated proofs seem to get an empty dirpath? + or I got confused because I had lemma foo in file foo + *) +Definition U := Type. + +Lemma foo : U. +Proof. + exact Type. +Qed. + + +Lemma foo1 : Type. +Proof. + exact (U:Type). +Qed. + +Print foo. +*) diff --git a/test-suite/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v new file mode 100644 index 0000000000..6302adefc2 --- /dev/null +++ b/test-suite/vio/univ_constraints_statements_body.v @@ -0,0 +1,7 @@ +Definition T := Type. +Definition T1 : T := Type. + +Lemma x : True. +Proof. +exact (let a : T := Type in I). +Qed. diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 2a26b6b12a..4bf971668d 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with y;auto with zarith. rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. - assert (0 < 2^p);auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a3ebe67325..d3fac82d09 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1428,7 +1428,7 @@ Proof. assert (Hp3: (0 < Φ (WW ih il))). {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } + } cbv zeta. case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. @@ -1465,7 +1465,6 @@ Proof. apply Hrec; rewrite H; clear u H. assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. - 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. split. replace (φ j + Φ (WW ih il) / φ j)%Z with (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 01cc9ad810..3a50001b1f 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -33,5 +33,6 @@ Ltac zify := intros; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; - zify_to_euclidean_division_equations ; zify_post_hook. + zify_to_euclidean_division_equations ; + zify_post_hook; + zify_saturate. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index f6ade67c5f..019d11d951 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -250,8 +250,18 @@ Register rew_iff as ZifyClasses.rew_iff. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. + +Register InjTyp as ZifyClasses.InjTyp. +Register BinOp as ZifyClasses.BinOp. +Register UnOp as ZifyClasses.UnOp. +Register CstOp as ZifyClasses.CstOp. +Register BinRel as ZifyClasses.BinRel. +Register PropOp as ZifyClasses.PropOp. +Register PropUOp as ZifyClasses.PropUOp. Register BinOpSpec as ZifyClasses.BinOpSpec. Register UnOpSpec as ZifyClasses.UnOpSpec. +Register Saturate as ZifyClasses.Saturate. + (** Propositional logic *) Register and as ZifyClasses.and. @@ -264,3 +274,4 @@ Register impl_morph as ZifyClasses.impl_morph. Register not as ZifyClasses.not. Register not_morph as ZifyClasses.not_morph. Register True as ZifyClasses.True. +Register I as ZifyClasses.I. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index dd31b998d4..8dee70be45 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -480,39 +480,20 @@ Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) -Instance SatProd : Saturate Z.mul := - {| - PArg1 := fun x => 0 <= x; - PArg2 := fun y => 0 <= y; - PRes := fun r => 0 <= r; - SatOk := Z.mul_nonneg_nonneg - |}. -Add Zify Saturate SatProd. - -Instance SatProdPos : Saturate Z.mul := +Instance SatPowPos : Saturate Z.pow := {| PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; + PArg2 := fun y => 0 <= y; PRes := fun r => 0 < r; - SatOk := Z.mul_pos_pos + SatOk := Z.pow_pos_nonneg |}. -Add Zify Saturate SatProdPos. - -Lemma pow_pos_strict : - forall a b, - 0 < a -> 0 < b -> 0 < a ^ b. -Proof. - intros. - apply Z.pow_pos_nonneg; auto. - apply Z.lt_le_incl;auto. -Qed. - +Add Zify Saturate SatPowPos. -Instance SatPowPos : Saturate Z.pow := +Instance SatPowNonneg : Saturate Z.pow := {| - PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; - PRes := fun r => 0 < r; - SatOk := pow_pos_strict + PArg1 := fun x => 0 <= x; + PArg2 := fun y => True; + PRes := fun r => 0 <= r; + SatOk := fun a b Ha _ => @Z.pow_nonneg a b Ha |}. -Add Zify Saturate SatPowPos. +Add Zify Saturate SatPowNonneg. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index f1dbac889b..199fc4225d 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -34,7 +34,8 @@ let usage () = eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; - eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; + eprintf " -noinit : currently no effect\n"; + eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; @@ -64,6 +65,7 @@ let rec parse = function | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-noinit" :: ll -> (* do nothing *) parse ll | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () @@ -80,6 +82,8 @@ let rec parse = function | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () + | opt :: ll when String.length opt > 0 && opt.[0] = '-' -> + coqdep_warning "unknown option %s" opt; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index dca9291da3..a6634586f3 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -157,6 +157,18 @@ let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 +let error_cannot_stat s unix_error = + (* Print an arbitrary line number, such that the message matches + common error message pattern. *) + Printf.eprintf "File \"%s\", line 1: %s\n" s (error_message unix_error); + exit 1 + +let error_cannot_open s msg = + (* Print an arbitrary line number, such that the message matches + common error message pattern. *) + Printf.eprintf "File \"%s\", line 1: %s\n" s msg; + exit 1 + let warning_module_notfound f s = coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!" f (String.concat "." s) @@ -368,7 +380,7 @@ let rec find_dependencies basename = | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j) - with Sys_error _ -> [] (* TODO: report an error? *) + with Sys_error msg -> error_cannot_open (basename ^ ".v") msg let write_vos = ref false @@ -472,7 +484,12 @@ let rec treat_file old_dirname old_name = | (Some d1,d2) -> Some (d1//d2) in let complete_name = file_name name dirname in - match try (stat complete_name).st_kind with _ -> S_BLK with + let stat_res = + try stat complete_name + with Unix_error(error, _, _) -> error_cannot_stat complete_name error + in + match stat_res.st_kind + with | S_DIR -> (if name.[0] <> '.' then let newdirname = diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune index cc888a959f..432d88b2ff 100644 --- a/tools/coqdoc/dune +++ b/tools/coqdoc/dune @@ -5,6 +5,13 @@ (coqdoc.css as tools/coqdoc/coqdoc.css) (coqdoc.sty as tools/coqdoc/coqdoc.sty))) +; File needs to be here too. +(install + (section share) + (package coq-core) + (files + (coqdoc.sty as texmf/tex/latex/misc/coqdoc.sty))) + (executable (name main) (public_name coqdoc) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 041097d2d3..df6f04792e 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -194,7 +194,7 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = if mode = BuildVio then dump_empty_vos() | Vio2Vo -> - + Flags.async_proofs_worker_id := "Vio2Vo"; let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_in in let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in @@ -223,6 +223,7 @@ let compile_file opts stm_opts copts injections = (* VIO Dispatching *) (******************************************************************************) let check_vio_tasks copts = + Flags.async_proofs_worker_id := "VioChecking"; let rc = List.fold_left (fun acc (n,f) -> let f_in = ensure ".vio" f f in diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 457b8e1acf..4758ecf5bd 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1754,6 +1754,16 @@ let () = add_scope "constr" (fun arg -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) ) +let () = add_scope "open_constr" (fun arg -> + let delimiters = List.map (function + | SexprRec (_, { v = Some s }, []) -> s + | _ -> scope_fail "open_constr" arg) + arg + in + let act e = Tac2quote.of_open_constr ~delimiters e in + Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) + ) + let add_expr_scope name entry f = add_scope name begin function | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f) @@ -1782,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_ let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format -let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern (** seq scope, a bit hairy *) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 6be5ba80d5..7af530ab0f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose" let q_assert = Pcoq.Entry.create "q_assert" end +let () = + let entries = [ + Pcoq.AnyEntry Pltac.ltac2_expr; + ] in + Pcoq.register_grammars_by_name "ltac2" entries + (** Tactic definition *) type tacdef = { diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 90c8528203..206f4df19d 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -467,7 +467,9 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme = let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" - (fun () -> strbrk "The following expression should have type unit.") + (fun (env, t) -> + strbrk "The following expression should have type unit but has type " ++ + pr_glbtype env t ++ str ".") let warn_redundant_clause = CWarnings.create ~name:"redundant-clause" ~category:"ltac" @@ -480,7 +482,7 @@ let check_elt_unit loc env t = | GTypRef (Tuple 0, []) -> true | GTypRef _ -> false in - if not maybe_unit then warn_not_unit ?loc () + if not maybe_unit then warn_not_unit ?loc (env, t) let check_elt_empty loc env t = match kind env t with | GTypVar _ -> @@ -504,7 +506,7 @@ let check_unit ?loc t = | GTypRef (Tuple 0, []) -> true | GTypRef _ -> false in - if not maybe_unit then warn_not_unit ?loc () + if not maybe_unit then warn_not_unit ?loc (env, t) let check_redundant_clause = function | [] -> () diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index d1a72fcfd1..2d65f9ec3e 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -102,18 +102,22 @@ let of_anti f = function let of_ident {loc;v=id} = inj_wit ?loc wit_ident id +let quote_constr ?delimiters c = + let loc = Constrexpr_ops.constr_loc c in + Option.cata + (List.fold_left (fun c d -> + CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c)) + c) + c delimiters + let of_constr ?delimiters c = let loc = Constrexpr_ops.constr_loc c in - let c = Option.cata - (List.fold_left (fun c d -> - CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c)) - c) - c delimiters - in + let c = quote_constr ?delimiters c in inj_wit ?loc wit_constr c -let of_open_constr c = +let of_open_constr ?delimiters c = let loc = Constrexpr_ops.constr_loc c in + let c = quote_constr ?delimiters c in inj_wit ?loc wit_open_constr c let of_bool ?loc b = diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index fcd1339cd7..6e2f548319 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -36,7 +36,7 @@ val of_ident : Id.t CAst.t -> raw_tacexpr val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr -val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr +val of_open_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr val of_list : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a list -> raw_tacexpr diff --git a/vernac/library.ml b/vernac/library.ml index cc9e3c3c44..eedf8aa670 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -448,10 +448,10 @@ let save_library_base f sum lib univs tasks proofs = Sys.remove f; Exninfo.iraise reraise -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) let save_library_to todo_proofs ~output_native_objects dir f otab = assert( @@ -464,7 +464,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let except = match todo_proofs with | ProofsTodoNone -> Future.UUIDSet.empty | ProofsTodoSomeEmpty except -> except - | ProofsTodoSome (except,l,_) -> except + | ProofsTodoSome (except,l) -> except in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in @@ -473,13 +473,13 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = | ProofsTodoNone -> None, None | ProofsTodoSomeEmpty _except -> None, Some (Univ.ContextSet.empty,false) - | ProofsTodoSome (_except, tasks, rcbackup) -> + | ProofsTodoSome (_except, tasks) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b with Not_found -> assert b; { r with uuid = -1 }, b) tasks in - Some (tasks,rcbackup), + Some tasks, Some (Univ.ContextSet.empty,false) in let sd = { diff --git a/vernac/library.mli b/vernac/library.mli index d0e9f84691..4c6c654c58 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -41,13 +41,13 @@ type seg_proofs = Opaqueproof.opaque_proofterm array argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) val save_library_to : - ('document,'counters) todo_proofs -> + 'document todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit diff --git a/vernac/record.ml b/vernac/record.ml index fccc3e4fbd..53f3508806 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -766,11 +766,9 @@ let add_inductive_class env sigma ind = let k = let ctx = oneind.mind_arity_ctxt in let univs = Declareops.inductive_polymorphic_context mind in - let env = push_context ~strict:false (Univ.AUContext.repr univs) env in - let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in let ty = Inductive.type_of_inductive ((mind, oneind), inst) in - let r = Inductive.relevance_of_inductive env ind in + let r = oneind.mind_relevance in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; cl_context = ctx; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af40292f18..54f034c74e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -413,7 +413,7 @@ let sort_universes g = let levels = traverse LMap.empty [normalize Level.set, 0] in let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in + let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in let ulevels = Array.cons Level.set ulevels in (* Add the normal universes *) let fold (cur, ans) u = |