From 1abd9033005b8a7b2df5f6ab11921bf9328855bc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Jul 2026 02:38:10 +0000 Subject: [PATCH 1/2] Report check_eliminations bypasses in Print Assumptions and rocqchk The typing flag check_eliminations turns off checking of the sort elimination constraints of inductive types (e.g. that an inductive in Prop cannot be eliminated into Type). It is recorded per declaration in const_typing_flags / mind_typing_flags, but until now nothing reported it: Print Assumptions inspected only check_guarded, check_positive and check_universes, pr_typing_flags omitted it, and the checker honored the stored flag silently. check_eliminations is independent of check_universes: Environ.set_typing_flags maps check_universes to UGraph.set_type_in_type but check_eliminations to QGraph.set_ignore_constraints, so a constant or eliminator declared while elimination checking is off still carries check_universes = true and is not reported as TypeInType. The squash information is moreover never computed at inductive-declaration time when the flag is off (indTyping.ml), so the inductive is permanently recorded as un-squashed and later matches on it typecheck silently. The only traces left are the stored typing flags, which nothing reported. Report it in the same places the other unsafe typing flags are surfaced: - Print Assumptions now lists constants and inductives relying on unchecked sort eliminations (new UncheckedEliminations axiom kind), and Set Printing All Assumptions adds a corresponding theory line. - Print Typing Flags now displays check_eliminations. - The checker (rocqchk) context summary reports constants/inductives relying on unchecked sort eliminations. There is intentionally no vernacular setter for this flag: it is only meant to be disabled from a plugin (via Global.set_typing_flags), as done by rocq-lean-import. The new test (test-suite/misc/unchecked-eliminations) therefore builds a tiny plugin that toggles the flag, declares a squashed Prop inductive with a large elimination while it is off, and checks that both Print Assumptions and rocq check report it. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- checker/check_stat.ml | 6 +++ .../22294-report-check-eliminations.rst | 10 ++++ .../proof-engine/vernacular-commands.rst | 16 ++++-- printing/printer.ml | 16 +++++- printing/printer.mli | 2 + test-suite/misc/unchecked-eliminations.sh | 49 +++++++++++++++++++ .../misc/unchecked-eliminations/.gitignore | 4 ++ .../misc/unchecked-eliminations/_CoqProject | 9 ++++ .../src/META.coq-test-suite | 11 +++++ .../unchecked-eliminations/src/elimFlag.mlg | 10 ++++ .../src/elimFlagImpl.ml | 8 +++ .../src/elimFlagImpl.mli | 2 + .../src/elim_flag_plugin.mlpack | 2 + .../theories/unchecked.v | 38 ++++++++++++++ test-suite/output-coqchk/bug_12845.out | 2 + test-suite/output-coqchk/bug_13324.out | 2 + test-suite/output-coqchk/bug_5030.out | 2 + test-suite/output-coqchk/indices_matter.out | 2 + vernac/assumptions.ml | 17 ++++++- 19 files changed, 202 insertions(+), 6 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst create mode 100755 test-suite/misc/unchecked-eliminations.sh create mode 100644 test-suite/misc/unchecked-eliminations/.gitignore create mode 100644 test-suite/misc/unchecked-eliminations/_CoqProject create mode 100644 test-suite/misc/unchecked-eliminations/src/META.coq-test-suite create mode 100644 test-suite/misc/unchecked-eliminations/src/elimFlag.mlg create mode 100644 test-suite/misc/unchecked-eliminations/src/elimFlagImpl.ml create mode 100644 test-suite/misc/unchecked-eliminations/src/elimFlagImpl.mli create mode 100644 test-suite/misc/unchecked-eliminations/src/elim_flag_plugin.mlpack create mode 100644 test-suite/misc/unchecked-eliminations/theories/unchecked.v diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d5a7662cc318..0559d14d0228 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -45,6 +45,11 @@ let pr_type_in_type env = let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in pr_assumptions "Constants/Inductives relying on type-in-type" csts +let pr_unchecked_eliminations env = + let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_eliminations then Constant.to_string c :: acc else acc) env [] in + let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_eliminations then MutInd.to_string c :: acc else acc) env csts in + pr_assumptions "Constants/Inductives relying on unchecked sort eliminations" csts + let pr_unguarded env = let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in @@ -73,6 +78,7 @@ let print_context env opac = match opac with str "* " ++ hov 0 (pr_rewrite_rules env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_unchecked_eliminations env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_indices_matter env ++ fnl())) diff --git a/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst b/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst new file mode 100644 index 000000000000..4cf9dcec60de --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst @@ -0,0 +1,10 @@ +- **Added:** + :cmd:`Print Assumptions` and the checker (``rocqchk``) now report + inductive types and constants whose sort elimination constraints were + not checked (typing flag ``check_eliminations = false``), which was + previously silently ignored, and :cmd:`Print Typing Flags` now also + displays that flag. The flag has no vernacular setter by design; it can + only be disabled from a plugin (via ``Global.set_typing_flags``), as + done for instance by ``rocq-lean-import`` + (`#22294 `_, + by Jason Gross). diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5d990b2bd188..277e8d2d5611 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -449,7 +449,9 @@ Requests to the environment (i.e., whose behavior would change under ``-indices-matter`` or :flag:`Indices Matter`), as well as uses of disabled typing flags such as :flag:`Guard Checking`, :flag:`Positivity Checking`, - :flag:`Universe Checking`, and :flag:`Definitional UIP`. + :flag:`Universe Checking`, :flag:`Definitional UIP`, and disabled + sort elimination checking (the ``check_eliminations`` typing flag, + which has no vernacular setter and can only be disabled from a plugin). The message "Closed under the global context" indicates that all the theorems and definitions have no dependencies. @@ -458,7 +460,8 @@ Requests to the environment Turn this :term:`flag` on to make :cmd:`Print Assumptions` report theory assumptions (impredicativity of :g:`Set`, rewrite rules, - disabled universe checking, indices not mattering) according to the + disabled universe checking, disabled sort elimination checking, + indices not mattering) according to the typing flags each dependency was typechecked with, in addition to the settings of the current environment. For instance, a definition typechecked with ``-impredicative-set`` is reported as assuming the @@ -1223,8 +1226,13 @@ Controlling Typing Flags .. cmd:: Print Typing Flags - Print the status of the three typing flags: guard checking, positivity checking - and universe checking. + Print the status of the typing flags: guard checking, positivity checking, + universe checking and elimination checking. + + The elimination checking flag has no vernacular setter; it can only be + disabled from a plugin (via ``Global.set_typing_flags``). When it is + disabled, inductive types (and constants depending on them) declared in + that state are reported by :cmd:`Print Assumptions`. .. example:: diff --git a/printing/printer.ml b/printing/printer.ml index 8379352eca6a..35167afed8c6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -621,6 +621,7 @@ type axiom = | Positive of MutInd.t | Guarded of GlobRef.t | TypeInType of GlobRef.t + | UncheckedEliminations of GlobRef.t | UIP of MutInd.t | IndicesNotMattering of MutInd.t @@ -644,7 +645,8 @@ struct | IndicesNotMattering m1, IndicesNotMattering m2 -> MutInd.UserOrd.compare m1 m2 | Guarded k1 , Guarded k2 - | TypeInType k1, TypeInType k2 -> + | TypeInType k1, TypeInType k2 + | UncheckedEliminations k1, UncheckedEliminations k2 -> GlobRef.UserOrd.compare k1 k2 | Constant _, _ -> -1 | _, Constant _ -> 1 @@ -654,6 +656,8 @@ struct | _, Guarded _ -> 1 | TypeInType _, _ -> -1 | _, TypeInType _ -> 1 + | UncheckedEliminations _, _ -> -1 + | _, UncheckedEliminations _ -> 1 | UIP _, _ -> -1 | _, UIP _ -> 1 @@ -678,6 +682,7 @@ type theory_assumptions = { has_impredicative_set : bool; has_rewrite_rules : bool; has_type_in_type : bool; + has_unchecked_eliminations : bool; } let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s = @@ -694,6 +699,7 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s = let show_theory_impredicative_set = (print_all && theory_info.has_impredicative_set) || is_impredicative_set env in let show_theory_rewrite_rules = (print_all && theory_info.has_rewrite_rules) || rewrite_rules_allowed env in let show_theory_type_in_type = (print_all && theory_info.has_type_in_type) || type_in_type env in + let show_theory_unchecked_eliminations = (print_all && theory_info.has_unchecked_eliminations) || ignore_elim_constraints env in if ContextObjectMap.is_empty s && not show_theory_rewrite_rules && not show_theory_impredicative_set then @@ -737,6 +743,8 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s = hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") + | UncheckedEliminations gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on unchecked sort eliminations.") | UIP mind -> hov 2 (safe_pr_inductive env mind ++ spc () ++ strbrk"relies on definitional UIP.") | IndicesNotMattering mind -> @@ -790,6 +798,11 @@ let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s = str "Type hierarchy is collapsed (logic is inconsistent)" :: theory else theory in + let theory = + if show_theory_unchecked_eliminations then + str "Sort elimination constraints are not checked (logic is inconsistent)" :: theory + else theory + in let opt_list title = function | [] -> None | l -> @@ -811,6 +824,7 @@ let pr_typing_flags flags = str "check_guarded: " ++ bool flags.check_guarded ++ fnl () ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () ++ str "check_universes: " ++ bool flags.check_universes ++ fnl () + ++ str "check_eliminations: " ++ bool flags.check_eliminations ++ fnl () ++ str "definitional uip: " ++ bool flags.allow_uip module Debug = diff --git a/printing/printer.mli b/printing/printer.mli index b855f8a1e3dc..91f9e7aa8323 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -234,6 +234,7 @@ type axiom = | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) + | UncheckedEliminations of GlobRef.t (* a constant or inductive whose sort elimination constraints were not checked *) | UIP of MutInd.t (* An inductive using the special reduction rule. *) | IndicesNotMattering of MutInd.t (* An inductive relying on indices not mattering. *) @@ -251,6 +252,7 @@ type theory_assumptions = { has_impredicative_set : bool; has_rewrite_rules : bool; has_type_in_type : bool; + has_unchecked_eliminations : bool; } val pr_assumptionset : ?flags:PrintingFlags.t -> diff --git a/test-suite/misc/unchecked-eliminations.sh b/test-suite/misc/unchecked-eliminations.sh new file mode 100755 index 000000000000..7ac44256fae4 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations.sh @@ -0,0 +1,49 @@ +#!/usr/bin/env bash + +# There is intentionally no vernacular setter for the [check_eliminations] +# typing flag. This test builds a tiny plugin that toggles it via +# [Global.set_typing_flags] (the way rocq-lean-import does), declares a +# squashed Prop inductive with a large elimination while the flag is off, and +# checks that both [Print Assumptions] and [rocq check] report it. + +set -ex + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH +export LC_ALL=C + +cd misc/unchecked-eliminations/ + +rocq makefile -f _CoqProject -o Makefile + +make clean + +make src/elim_flag_plugin.cmxs + +# Compile the .v, capturing the Print Assumptions / Print Typing Flags output. +rocq c -I src -Q theories UncheckedElim theories/unchecked.v 2>&1 | tee log + +# checked_or (declared with the flag on) must NOT be reported. +# Anchor at line start so this does not match "unchecked_or". +grep -q "^checked_or relies on unchecked sort eliminations" log && { + >&2 echo "checked_or should not rely on unchecked eliminations" + exit 1 +} + +# unchecked_or and its constructors (declared with the flag off) must be +# reported as relying on unchecked sort eliminations. +grep -q "^unchecked_or relies on unchecked sort eliminations" log +grep -q "^unchecked_l relies on unchecked sort eliminations" log +grep -q "^unchecked_r relies on unchecked sort eliminations" log + +# The theory summary line appears under Set Printing All Assumptions. +grep -q "Sort elimination constraints are not checked (logic is inconsistent)" log + +# Print Typing Flags reports the flag. +grep -q "check_eliminations:" log + +# rocq check must report the inductive in its context summary. +rocq check -Q theories UncheckedElim -o -silent -norec UncheckedElim.unchecked 2>&1 | tee chklog + +grep -q "Constants/Inductives relying on unchecked sort eliminations" chklog +grep -q "UncheckedElim.unchecked.unchecked_or" chklog diff --git a/test-suite/misc/unchecked-eliminations/.gitignore b/test-suite/misc/unchecked-eliminations/.gitignore new file mode 100644 index 000000000000..d8a51ef1b1d4 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/.gitignore @@ -0,0 +1,4 @@ +/Makefile* +/log +/chklog +/src/elimFlag.ml diff --git a/test-suite/misc/unchecked-eliminations/_CoqProject b/test-suite/misc/unchecked-eliminations/_CoqProject new file mode 100644 index 000000000000..e94422460c05 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/_CoqProject @@ -0,0 +1,9 @@ +src/META.coq-test-suite +-Q theories UncheckedElim +-I src + +src/elimFlag.mlg +src/elimFlagImpl.ml +src/elimFlagImpl.mli +src/elim_flag_plugin.mlpack +theories/unchecked.v diff --git a/test-suite/misc/unchecked-eliminations/src/META.coq-test-suite b/test-suite/misc/unchecked-eliminations/src/META.coq-test-suite new file mode 100644 index 000000000000..fc82287a2f5b --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/src/META.coq-test-suite @@ -0,0 +1,11 @@ +package "elim_flag" ( + directory = "." + version = "dev" + description = "A test plugin toggling the check_eliminations typing flag" + requires = "rocq-runtime.plugins.ltac" + archive(byte) = "elim_flag_plugin.cma" + archive(native) = "elim_flag_plugin.cmxa" + plugin(byte) = "elim_flag_plugin.cma" + plugin(native) = "elim_flag_plugin.cmxs" +) +directory = "." diff --git a/test-suite/misc/unchecked-eliminations/src/elimFlag.mlg b/test-suite/misc/unchecked-eliminations/src/elimFlag.mlg new file mode 100644 index 000000000000..d5ff6069ca81 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/src/elimFlag.mlg @@ -0,0 +1,10 @@ +{ +open ElimFlagImpl +} + +DECLARE PLUGIN "coq-test-suite.elim_flag" + +VERNAC COMMAND EXTEND ElimChecking CLASSIFIED AS SIDEFF +| [ "Unset" "Test" "Elimination" "Checking" ] -> { set_elimination_checking false } +| [ "Set" "Test" "Elimination" "Checking" ] -> { set_elimination_checking true } +END diff --git a/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.ml b/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.ml new file mode 100644 index 000000000000..e1917064d795 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.ml @@ -0,0 +1,8 @@ +(* There is intentionally no vernacular setter for [check_eliminations]: + this test plugin toggles it directly, the way plugins such as + rocq-lean-import do, so that the reporting of unchecked sort eliminations + by Print Assumptions and rocqchk can be exercised. *) + +let set_elimination_checking b = + let flags = Global.typing_flags () in + Global.set_typing_flags { flags with Declarations.check_eliminations = b } diff --git a/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.mli b/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.mli new file mode 100644 index 000000000000..40270d647f2e --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/src/elimFlagImpl.mli @@ -0,0 +1,2 @@ + +val set_elimination_checking : bool -> unit diff --git a/test-suite/misc/unchecked-eliminations/src/elim_flag_plugin.mlpack b/test-suite/misc/unchecked-eliminations/src/elim_flag_plugin.mlpack new file mode 100644 index 000000000000..220f5da5b4d6 --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/src/elim_flag_plugin.mlpack @@ -0,0 +1,2 @@ +ElimFlagImpl +ElimFlag diff --git a/test-suite/misc/unchecked-eliminations/theories/unchecked.v b/test-suite/misc/unchecked-eliminations/theories/unchecked.v new file mode 100644 index 000000000000..e2b598867b4d --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/theories/unchecked.v @@ -0,0 +1,38 @@ +Declare ML Module "coq-test-suite.elim_flag". + +(* With elimination checking on, the large elimination below is squashed. *) +Inductive checked_or (A B : Prop) : Prop := +| checked_l : A -> checked_or A B +| checked_r : B -> checked_or A B. + +Fail Definition checked_large (A B : Prop) (H : checked_or A B) : Type := + match H with + | checked_l _ _ _ => nat + | checked_r _ _ _ => bool + end. + +Print Assumptions checked_or. + +(* The plugin disables check_eliminations directly, the way rocq-lean-import + does; there is intentionally no vernacular setter for this flag. *) +Unset Test Elimination Checking. + +Inductive unchecked_or (A B : Prop) : Prop := +| unchecked_l : A -> unchecked_or A B +| unchecked_r : B -> unchecked_or A B. + +Definition unchecked_large (A B : Prop) (H : unchecked_or A B) : Type := + match H with + | unchecked_l _ _ _ => nat + | unchecked_r _ _ _ => bool + end. + +Set Test Elimination Checking. + +Print Assumptions unchecked_large. + +Set Printing All Assumptions. +Print Assumptions unchecked_large. +Unset Printing All Assumptions. + +Print Typing Flags. diff --git a/test-suite/output-coqchk/bug_12845.out b/test-suite/output-coqchk/bug_12845.out index 7e708b998cbd..b9f1e4871e3c 100644 --- a/test-suite/output-coqchk/bug_12845.out +++ b/test-suite/output-coqchk/bug_12845.out @@ -10,6 +10,8 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: +* Constants/Inductives relying on unchecked sort eliminations: + * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/bug_13324.out b/test-suite/output-coqchk/bug_13324.out index 7e708b998cbd..b9f1e4871e3c 100644 --- a/test-suite/output-coqchk/bug_13324.out +++ b/test-suite/output-coqchk/bug_13324.out @@ -10,6 +10,8 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: +* Constants/Inductives relying on unchecked sort eliminations: + * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/bug_5030.out b/test-suite/output-coqchk/bug_5030.out index 7e708b998cbd..b9f1e4871e3c 100644 --- a/test-suite/output-coqchk/bug_5030.out +++ b/test-suite/output-coqchk/bug_5030.out @@ -10,6 +10,8 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: +* Constants/Inductives relying on unchecked sort eliminations: + * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/indices_matter.out b/test-suite/output-coqchk/indices_matter.out index 6a00fb15bb04..b23db05bc266 100644 --- a/test-suite/output-coqchk/indices_matter.out +++ b/test-suite/output-coqchk/indices_matter.out @@ -10,6 +10,8 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: +* Constants/Inductives relying on unchecked sort eliminations: + * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 2e2058b9bbec..482e4d9e24a8 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -377,9 +377,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = let has_impredicative_set = ref false in let has_rewrite_rules = ref false in let has_type_in_type = ref false in + let has_unchecked_eliminations = ref false in let collect_theory_flags (tf : Declarations.typing_flags) = if tf.impredicative_set then has_impredicative_set := true; - if not tf.check_universes then has_type_in_type := true + if not tf.check_universes then has_type_in_type := true; + if not tf.check_eliminations then has_unchecked_eliminations := true in let fold obj contents accu = match obj with | VarRef id -> @@ -407,6 +409,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in + let accu = + if cb.const_typing_flags.check_eliminations then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (UncheckedEliminations obj, l)) Constr.mkProp accu + in if not (Option.has_some contents) then let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in @@ -440,6 +448,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in + let accu = + if mind.mind_typing_flags.check_eliminations then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (UncheckedEliminations obj, l)) Constr.mkProp accu + in let accu = if not (uses_uip mind) then accu else @@ -459,5 +473,6 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = has_impredicative_set = !has_impredicative_set; has_rewrite_rules = !has_rewrite_rules; has_type_in_type = !has_type_in_type; + has_unchecked_eliminations = !has_unchecked_eliminations; } in (theory, map) From d6dfea13c04d372c3822200e97af4d619b5f4b41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Jul 2026 03:04:41 +0000 Subject: [PATCH 2/2] Keep check_eliminations reporting out of sight unless relevant Per review: the flag is obscure by design, so its reporting should be too. The rocqchk context summary now omits the unchecked-sort- eliminations section entirely when there is nothing to report (the pre-existing output-coqchk fixtures are restored unchanged), and Print Typing Flags prints the check_eliminations line only when the flag has been disabled. The reference-manual text is removed; the Print Assumptions entries and theory line are unchanged (they already appear only when a dependency actually relies on the bypass). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw --- checker/check_stat.ml | 7 +++++-- .../22294-report-check-eliminations.rst | 2 +- doc/sphinx/proof-engine/vernacular-commands.rst | 16 ++++------------ printing/printer.ml | 5 ++++- test-suite/misc/unchecked-eliminations.sh | 9 +++++++-- .../unchecked-eliminations/theories/unchecked.v | 4 ++++ test-suite/output-coqchk/bug_12845.out | 2 -- test-suite/output-coqchk/bug_13324.out | 2 -- test-suite/output-coqchk/bug_5030.out | 2 -- test-suite/output-coqchk/indices_matter.out | 2 -- 10 files changed, 25 insertions(+), 26 deletions(-) diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 0559d14d0228..4af63341ff58 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -45,10 +45,13 @@ let pr_type_in_type env = let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in pr_assumptions "Constants/Inductives relying on type-in-type" csts +(* Kept out of the report when empty: this flag has no vernacular setter and + should stay obscure (see #22294 discussion). *) let pr_unchecked_eliminations env = let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_eliminations then Constant.to_string c :: acc else acc) env [] in let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_eliminations then MutInd.to_string c :: acc else acc) env csts in - pr_assumptions "Constants/Inductives relying on unchecked sort eliminations" csts + if csts = [] then mt () + else str "* " ++ hov 0 (pr_assumptions "Constants/Inductives relying on unchecked sort eliminations" csts ++ fnl()) ++ fnl() let pr_unguarded env = let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in @@ -78,7 +81,7 @@ let print_context env opac = match opac with str "* " ++ hov 0 (pr_rewrite_rules env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_unchecked_eliminations env ++ fnl()) ++ fnl() ++ + pr_unchecked_eliminations env ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_indices_matter env ++ fnl())) diff --git a/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst b/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst index 4cf9dcec60de..422147e22fa3 100644 --- a/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst +++ b/doc/changelog/08-vernac-commands-and-options/22294-report-check-eliminations.rst @@ -3,7 +3,7 @@ inductive types and constants whose sort elimination constraints were not checked (typing flag ``check_eliminations = false``), which was previously silently ignored, and :cmd:`Print Typing Flags` now also - displays that flag. The flag has no vernacular setter by design; it can + displays that flag when it has been disabled. The flag has no vernacular setter by design; it can only be disabled from a plugin (via ``Global.set_typing_flags``), as done for instance by ``rocq-lean-import`` (`#22294 `_, diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 277e8d2d5611..5d990b2bd188 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -449,9 +449,7 @@ Requests to the environment (i.e., whose behavior would change under ``-indices-matter`` or :flag:`Indices Matter`), as well as uses of disabled typing flags such as :flag:`Guard Checking`, :flag:`Positivity Checking`, - :flag:`Universe Checking`, :flag:`Definitional UIP`, and disabled - sort elimination checking (the ``check_eliminations`` typing flag, - which has no vernacular setter and can only be disabled from a plugin). + :flag:`Universe Checking`, and :flag:`Definitional UIP`. The message "Closed under the global context" indicates that all the theorems and definitions have no dependencies. @@ -460,8 +458,7 @@ Requests to the environment Turn this :term:`flag` on to make :cmd:`Print Assumptions` report theory assumptions (impredicativity of :g:`Set`, rewrite rules, - disabled universe checking, disabled sort elimination checking, - indices not mattering) according to the + disabled universe checking, indices not mattering) according to the typing flags each dependency was typechecked with, in addition to the settings of the current environment. For instance, a definition typechecked with ``-impredicative-set`` is reported as assuming the @@ -1226,13 +1223,8 @@ Controlling Typing Flags .. cmd:: Print Typing Flags - Print the status of the typing flags: guard checking, positivity checking, - universe checking and elimination checking. - - The elimination checking flag has no vernacular setter; it can only be - disabled from a plugin (via ``Global.set_typing_flags``). When it is - disabled, inductive types (and constants depending on them) declared in - that state are reported by :cmd:`Print Assumptions`. + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. .. example:: diff --git a/printing/printer.ml b/printing/printer.ml index 35167afed8c6..dddcf7dbf80b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -824,7 +824,10 @@ let pr_typing_flags flags = str "check_guarded: " ++ bool flags.check_guarded ++ fnl () ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () ++ str "check_universes: " ++ bool flags.check_universes ++ fnl () - ++ str "check_eliminations: " ++ bool flags.check_eliminations ++ fnl () + (* shown only when disabled: this flag has no vernacular setter and should + stay obscure (see #22294 discussion) *) + ++ (if flags.check_eliminations then mt () + else str "check_eliminations: " ++ bool flags.check_eliminations ++ fnl ()) ++ str "definitional uip: " ++ bool flags.allow_uip module Debug = diff --git a/test-suite/misc/unchecked-eliminations.sh b/test-suite/misc/unchecked-eliminations.sh index 7ac44256fae4..ea85dd0928bb 100755 --- a/test-suite/misc/unchecked-eliminations.sh +++ b/test-suite/misc/unchecked-eliminations.sh @@ -39,8 +39,13 @@ grep -q "^unchecked_r relies on unchecked sort eliminations" log # The theory summary line appears under Set Printing All Assumptions. grep -q "Sort elimination constraints are not checked (logic is inconsistent)" log -# Print Typing Flags reports the flag. -grep -q "check_eliminations:" log +# Print Typing Flags reports the flag only while it is disabled; the final +# Print Typing Flags (flag restored) must not mention it. +grep -q "check_eliminations: false" log +grep -q "check_eliminations: true" log && { + >&2 echo "check_eliminations should not be shown when at its default" + exit 1 +} # rocq check must report the inductive in its context summary. rocq check -Q theories UncheckedElim -o -silent -norec UncheckedElim.unchecked 2>&1 | tee chklog diff --git a/test-suite/misc/unchecked-eliminations/theories/unchecked.v b/test-suite/misc/unchecked-eliminations/theories/unchecked.v index e2b598867b4d..c714c22ccedd 100644 --- a/test-suite/misc/unchecked-eliminations/theories/unchecked.v +++ b/test-suite/misc/unchecked-eliminations/theories/unchecked.v @@ -17,6 +17,10 @@ Print Assumptions checked_or. does; there is intentionally no vernacular setter for this flag. *) Unset Test Elimination Checking. +(* While disabled, Print Typing Flags shows the flag; when it is at its + default (true) the line is omitted entirely. *) +Print Typing Flags. + Inductive unchecked_or (A B : Prop) : Prop := | unchecked_l : A -> unchecked_or A B | unchecked_r : B -> unchecked_or A B. diff --git a/test-suite/output-coqchk/bug_12845.out b/test-suite/output-coqchk/bug_12845.out index b9f1e4871e3c..7e708b998cbd 100644 --- a/test-suite/output-coqchk/bug_12845.out +++ b/test-suite/output-coqchk/bug_12845.out @@ -10,8 +10,6 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: -* Constants/Inductives relying on unchecked sort eliminations: - * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/bug_13324.out b/test-suite/output-coqchk/bug_13324.out index b9f1e4871e3c..7e708b998cbd 100644 --- a/test-suite/output-coqchk/bug_13324.out +++ b/test-suite/output-coqchk/bug_13324.out @@ -10,8 +10,6 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: -* Constants/Inductives relying on unchecked sort eliminations: - * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/bug_5030.out b/test-suite/output-coqchk/bug_5030.out index b9f1e4871e3c..7e708b998cbd 100644 --- a/test-suite/output-coqchk/bug_5030.out +++ b/test-suite/output-coqchk/bug_5030.out @@ -10,8 +10,6 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: -* Constants/Inductives relying on unchecked sort eliminations: - * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: diff --git a/test-suite/output-coqchk/indices_matter.out b/test-suite/output-coqchk/indices_matter.out index b23db05bc266..6a00fb15bb04 100644 --- a/test-suite/output-coqchk/indices_matter.out +++ b/test-suite/output-coqchk/indices_matter.out @@ -10,8 +10,6 @@ CONTEXT SUMMARY * Constants/Inductives relying on type-in-type: -* Constants/Inductives relying on unchecked sort eliminations: - * Constants/Inductives relying on unsafe (co)fixpoints: * Inductives whose positivity is assumed: