diff options
28 files changed, 364 insertions, 162 deletions
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-common.sh b/dev/ci/ci-common.sh index 006565df5c..6d1e6d788a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -138,8 +138,8 @@ make() if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; then # Not submake and parallel make requested - command make --output-sync -j "$NJOBS" "$@" + command make -j "$NJOBS" "$@" else - command make --output-sync "$@" + command make "$@" fi } 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/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/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/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/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/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 index 5e1150146e..9ea751eef9 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -28,10 +28,10 @@ let new_counter ~name a ~incr ~build = 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; + let x = CThread.with_lock m ~scope:f in build x in let mk_thsafe_remote_getter f () = - Mutex.lock m; let x = f () in Mutex.unlock m; x in + CThread.with_lock m ~scope:f 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 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..2cb615170b 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,6 @@ 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 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. This is useful for calling Constr.hash *) @@ -59,6 +71,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 +357,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 +389,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 +447,7 @@ module EBinOp = struct open EBinOpT let name = "BinOp" + let gref = coq_BinOp let table = table let mk_elt evd i a = @@ -473,6 +489,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 +516,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 +549,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 +576,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 +589,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 +601,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 +633,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 +642,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 +660,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 +696,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 +710,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 +724,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 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/stm.ml b/stm/stm.ml index 9480bbdc2e..f5768726c3 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 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/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/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index f6ade67c5f..a08a56b20e 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. 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/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 | [] -> () |