From 56c5ce550f574fae1fef4fe61731a18a179fcd73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 4 Apr 2023 14:13:40 +0200 Subject: [PATCH 1/2] Cleanup vernac_check_guard Guard checking stop raising UserError a long time ago. --- vernac/vernacentries.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1953823a8f4e..16d78bf6c966 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2151,16 +2151,11 @@ let vernac_show ~pstate = let vernac_check_guard ~pstate = let pts = Declare.Proof.get pstate in let pfterm = List.hd (Proof.partial_proof pts) in - let message = - try - let { Proof.entry; Proof.sigma } = Proof.data pts in - let hyps, _, _ = List.hd (Proofview.initial_goals entry) in - let env = Environ.reset_with_named_context hyps (Global.env ()) in - Inductiveops.control_only_guard env sigma pfterm; - (str "The condition holds up to here") - with UserError s -> - (str ("Condition violated: ") ++ s ++ str ".") - in message + let { Proof.entry; Proof.sigma } = Proof.data pts in + let hyps, _, _ = List.hd (Proofview.initial_goals entry) in + let env = Environ.reset_with_named_context hyps (Global.env ()) in + Inductiveops.control_only_guard env sigma pfterm; + str "The condition holds up to here." let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with | EVernacNotation { local; decl } -> From 66f72f0b6549dea05e23947a4e24a5b7ea909147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 4 Apr 2023 14:45:20 +0200 Subject: [PATCH 2/2] Validate Proof command: runs typing.ml on the current proof --- .../17467-validate-proof.rst | 5 +++ doc/sphinx/language/core/variants.rst | 5 +++ .../proofs/writing-proofs/proof-mode.rst | 7 +++ doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + test-suite/success/ValidateProof.v | 22 ++++++++++ vernac/g_proofs.mlg | 1 + vernac/ppvernac.ml | 2 + vernac/vernac_classifier.ml | 2 +- vernac/vernacentries.ml | 43 +++++++++++++++++++ vernac/vernacexpr.mli | 1 + 11 files changed, 89 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst create mode 100644 test-suite/success/ValidateProof.v diff --git a/doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst b/doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst new file mode 100644 index 000000000000..1df1495e02b8 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst @@ -0,0 +1,5 @@ +- **Added:** + :cmd:`Validate Proof` runs the type checker on the current proof, + complementary with :cmd:`Guarded` which runs the guard checker. + (`#17467 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index f19c1db20a7a..9d79aeab466b 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -39,6 +39,11 @@ Private (matching) inductive types quotient types / higher-order inductive types in projects such as the `HoTT library `_. + Reducing definitions from the inductive's module can expose + :g:`match` constructs to unification, which may result in invalid proof terms. + Errors from such terms are delayed until proof completion (i.e. on the :cmd:`Qed`). Use + :cmd:`Validate Proof` to identify which tactic produced the problematic term. + .. example:: .. coqtop:: all diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index d099d297a2ed..945de411820c 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -1023,6 +1023,13 @@ Requesting information fixpoint and cofixpoint is violated at some time of the construction of the proof without having to wait the completion of the proof. +.. cmd:: Validate Proof + + Checks that the current partial proof is well-typed. + It is useful for finding tactic bugs since without it, such errors will only be detected at :cmd:`Qed` time. + + It does not check the guard condition. Use :cmd:`Guarded` for that. + .. _showing_diffs: Showing differences between proof steps diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3f881ca88eff..70709505a590 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -520,6 +520,7 @@ command: [ | "Show" "Intros" | "Show" "Match" reference | "Guarded" +| "Validate" "Proof" | "Create" "HintDb" IDENT; [ "discriminated" | ] | "Remove" "Hints" LIST1 global opt_hintbases | "Hint" hint opt_hintbases diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 4c899c10143d..c5892b685932 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -818,6 +818,7 @@ command: [ | "Show" "Intros" | "Show" "Match" qualid | "Guarded" +| "Validate" "Proof" | "Create" "HintDb" ident OPT "discriminated" | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident ) | "Comments" LIST0 [ one_term | string | natural ] diff --git a/test-suite/success/ValidateProof.v b/test-suite/success/ValidateProof.v new file mode 100644 index 000000000000..4cb74a55ad62 --- /dev/null +++ b/test-suite/success/ValidateProof.v @@ -0,0 +1,22 @@ + +Module M. + Private Inductive foo := . + + Definition to_nat (f:foo) : nat := match f with end. +End M. + +Lemma bar : False. +Proof. + exact_no_check I. + Fail Validate Proof. +Abort. + +Lemma bar f : M.to_nat f = 0. +Proof. + Validate Proof. + + cbv. + + Fail Validate Proof. + +Abort. diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 7629316a9e69..b5e80388ccb6 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -95,6 +95,7 @@ GRAMMAR EXTEND Gram | IDENT "Show"; IDENT "Intros" -> { VernacSynPure (VernacShow (ShowIntros true)) } | IDENT "Show"; IDENT "Match"; id = reference -> { VernacSynPure (VernacShow (ShowMatch id)) } | IDENT "Guarded" -> { VernacSynPure VernacCheckGuard } + | IDENT "Validate"; IDENT "Proof" -> { VernacSynPure VernacValidateProof } (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8fa0f4322e28..6b4b898acf09 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -724,6 +724,8 @@ let pr_synpure_vernac_expr v = | VernacCheckGuard -> return (keyword "Guarded") + | VernacValidateProof -> return (keyword "Validate Proof") + (* Resetting *) | VernacResetName id -> return (keyword "Reset" ++ spc() ++ pr_lident id) diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml index 94ad66b7defa..61a8e50ecfbf 100644 --- a/vernac/vernac_classifier.ml +++ b/vernac/vernac_classifier.ml @@ -100,7 +100,7 @@ let classify_vernac e = | VernacProof _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ - | VernacCheckGuard + | VernacCheckGuard | VernacValidateProof | VernacUnfocused | VernacBullet _ -> VtProofStep { proof_block_detection = Some "bullet" } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 16d78bf6c966..dc4453523c92 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2157,6 +2157,45 @@ let vernac_check_guard ~pstate = Inductiveops.control_only_guard env sigma pfterm; str "The condition holds up to here." +let vernac_validate_proof ~pstate = + let pts = Declare.Proof.get pstate in + let { Proof.entry; Proof.sigma } = Proof.data pts in + let hyps, pfterm, pftyp = List.hd (Proofview.initial_goals entry) in + (* XXX can the initial hyps contain something broken? For now assume they're correct. + NB: in the "Lemma foo args : bla." case the args are part of the + term and intro'd after the proof is opened. Only the section + variables are in the hyps. *) + let env = Environ.reset_with_named_context hyps (Global.env ()) in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + let sigma' = Typing.check env sigma pfterm pftyp in + let evar_issues = + (* Use Evar.Map.merge as a kind of for_all2 *) + Evar.Map.merge (fun e orig now -> match orig, now with + | None, None -> assert false + | Some _, Some _ -> None (* assume same *) + | Some evi, None -> + let EvarInfo evi' = Evd.find sigma' e in + let body = match Evd.evar_body evi' with + | Evar_empty -> assert false + | Evar_defined body -> body + in + Some + Pp.(str "Evar " ++ Printer.pr_evar sigma (e, evi) + ++ spc() ++ str "was inferred by unification to be" ++ spc() + ++ pr_econstr_env (Evd.evar_env env evi') sigma' body) + | None, Some _ -> (* ignore new evar *) + assert (not (Evd.is_defined sigma e)); + None + ) + (Evd.undefined_map sigma) + (Evd.undefined_map sigma') + in + (* TODO check ustate *) + + if Evar.Map.is_empty evar_issues then + str "No issues found." + else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues) + let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with | EVernacNotation { local; decl } -> vtdefault(fun () -> Metasyntax.add_notation_interpretation ~local (Global.env()) decl) @@ -2477,6 +2516,10 @@ let translate_pure_vernac ?loc ~atts v = let open Vernacextend in match v with vtreadproof(fun ~pstate -> unsupported_attributes atts; Feedback.msg_notice @@ vernac_check_guard ~pstate) + | VernacValidateProof -> + vtreadproof(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_validate_proof ~pstate) | VernacProof (tac, using) -> vtmodifyproof(fun ~pstate -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index d416cdfbf209..0354f9526f41 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -486,6 +486,7 @@ type nonrec synpure_vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard + | VernacValidateProof | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacAddOption of Goptions.option_name * Goptions.table_value list