Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[declare] Warn on unused using attributes on sub-obligations #19007

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

[declare] Warn on unused using attributes on sub-obligations #19007

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
19 changes: 17 additions & 2 deletions vernac/declare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1437,7 +1437,8 @@ let obligation_uctx_terminator prg uctx ~poly ~defined =

let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto; check_final} =
let env = Global.env () in
let ty = entry.proof_entry_type in
let ty, opaque = entry.proof_entry_type, entry.proof_entry_opaque in
(* EJGA: CAREFUL HERE, other stuff in the entry is lost *)
let body, uctx = inline_private_constants ~uctx env entry in
let sigma = Evd.from_ctx uctx in
Inductiveops.control_only_guard (Global.env ()) sigma
Expand All @@ -1447,7 +1448,7 @@ let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto; check_final}
let {obls; remaining = rem} = prg.prg_obligations in
let obl = obls.(num) in
let status =
match (obl.obl_status, entry.proof_entry_opaque) with
match (obl.obl_status, opaque) with
| (_, Evar_kinds.Expand), true -> err_not_transp ()
| (true, _), true -> err_not_transp ()
| (false, _), true -> Evar_kinds.Define true
Expand Down Expand Up @@ -2549,6 +2550,10 @@ let auto_solve_obligations ~pm n ?oblset tac : State.t * progress =
let prg = get_unique_prog ~pm n in
solve_prg_obligations ~pm prg ?oblset tac

let warn_unused_using =
CWarnings.create ~name:"using-on-sub-obligation" (fun () ->
Pp.str "Using declarations are ignored in sub-obligations.")

let solve_obligation ?check_final prg num tac =
let user_num = succ num in
let { obls; remaining=rem } = Internal.get_obligations prg in
Expand All @@ -2570,7 +2575,17 @@ let solve_obligation ?check_final prg num tac =
Proof_ending.End_obligation {name; num; auto; check_final}
in
let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in

(* EJGA/HH: Note that this using won't have any effect as
[obligation_terminator] discards the using data in the entry set
by the call below to [Proof.start_core]. We still pass it to the
proof context, but emit a warning. Note that we only warn if
using the attribute, [Proof Using] doesn't do the check to see if
we are in a obligation [could be done by checking terminator type
tho] *)
let using =
(* TODO: locate this *)
let () = warn_unused_using () ?loc:None in
let using = Internal.get_using prg in
let env = Global.env () in
let f {CInfo.name; typ; _} = name, [typ] in
Comment on lines +2588 to 2591
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The warning should be when using is non-None, and, then, the idea would be that the useless computation that follows is removed.

Expand Down