diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d5a7662cc318..4af63341ff58 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -45,6 +45,14 @@ 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 + 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 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 +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() ++ + 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 new file mode 100644 index 000000000000..422147e22fa3 --- /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 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 `_, + by Jason Gross). diff --git a/printing/printer.ml b/printing/printer.ml index 8379352eca6a..dddcf7dbf80b 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,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 () + (* 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/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..ea85dd0928bb --- /dev/null +++ b/test-suite/misc/unchecked-eliminations.sh @@ -0,0 +1,54 @@ +#!/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 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 + +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..c714c22ccedd --- /dev/null +++ b/test-suite/misc/unchecked-eliminations/theories/unchecked.v @@ -0,0 +1,42 @@ +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. + +(* 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. + +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/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)