Stream: Ltac2

Topic: Control.new_goal leaving goal shelved


view this post on Zulip Janno (Apr 27 2023 at 09:29):

Why is the one remaining and focused goal in the example below also still on the shelf after Control.new_goal?

From Ltac2 Require Import Ltac2 Constr.
Import Constr.Unsafe.
Goal True.
  let t := open_constr:(_ : False) in
  match kind t with
  | Cast t _ _ =>
      match kind t with
      | Evar e _ => Control.new_goal e > [refine 'I|]
      | _ => ()
      end
  | _ => ()
  end.
  Show Existentials. (* Existential 1 = ?Goal : [ |- False] (shelved) *)

view this post on Zulip Rodolphe Lepigre (May 02 2023 at 21:45):

Having discussed this with Janno last week, it seems to us that this is an Ltac2 bug. Can anyone confirm?

view this post on Zulip Gaëtan Gilbert (May 02 2023 at 21:55):

(deleted)

view this post on Zulip Janno (Jun 03 2024 at 17:16):

I'd still like to get to the bottom of this. We always have one spurious shelved goal around because of this bug and it's a little annoying, especially when people are trying to watch out for truly shelved goals.

view this post on Zulip Gaëtan Gilbert (Jun 03 2024 at 18:17):

pretyping _ : False puts the evar in the "future goal" in the evar map
Proof.run_tactic puts the future goals in the shelf without checking if they're already focused somewhere
I guess new_goal should do Evd.remove_future_goal on the given evar or run_tactic should check focus status

also doing

  let t := unshelve open_constr:(_ : False) in
  Control.extend [fun () => Control.shelve()] (fun () => ()) [];

to put the goal in the shelf instead of the future goals (unshelve makes new goals from both the shelf and the future goals produced during the given tactic) doesn't help, so any removal from or checking of future goals must also be done on shelved goals

view this post on Zulip Gaëtan Gilbert (Jun 03 2024 at 18:19):

not sure why we have separate shelf and future goals tbh, not that it seems to matter for this issue

view this post on Zulip Gaëtan Gilbert (Jun 03 2024 at 18:20):

BTW maybe worth reporting an issue instead of just a zulip thread

view this post on Zulip Janno (Jun 04 2024 at 07:17):

Thanks for the explanation! This should be enough to find a workaround. I also opened an issue: https://github.com/coq/coq/issues/19138


Last updated: Jul 13 2024 at 04:02 UTC