Stream: Ltac2

Topic: Error in Qed after using Ltac2 Eval in proof context


view this post on Zulip Michael Soegtrop (Jan 28 2022 at 17:58):

@Pierre-Marie Pédrot : I have a weird effect with Ltac2 Eval. When I use it in a proof context, I get errors during Qed like

The variable X was not found in the current environment.

where X is a variable defined in the proof context.

Is this expected? Can one safely use Ltac2 Eval in a proof context? I do this sometimes to debug tactics which return a value.

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 18:04):

example?

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 18:54):

@Gaëtan Gilbert : a few 1000 lines of Ltac2 code - I first wanted to have an assesment if this is expected or not before I boild it down to something I can share.

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 19:07):

Ltac2 Eval doc says it's supposed to be without side effect so not expected

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 19:07):

not sure why it's not classified query tbh

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 19:58):

OK, let me see if I can construct a short example

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 20:41):

Here is a short example - it seems to have to do with mutable records:

Require Import Ltac2.Ltac2.

Ltac2 Type state := { mutable data : constr }.

Example Ex1: forall a : nat, True.
  intros a.
  Ltac2 Eval { data := 'a }.
  exact I.
Qed.

Should I file a bug report?

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 20:41):

Hmm - when I remove the mutable it is still the same error.

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 20:42):

this is probably the replay of side effect commands

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 20:43):

What side effects would there be without the mutable?

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 20:43):

eg

Require Import Ltac2.Ltac2.

Ltac2 Type state := { data : constr }.

Example Ex1: forall a : nat, True.
  intros a.
  Hint Resolve 0. (* outputs some warnings *)
  exact I.
Qed. (* get the warnings again *)

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 20:44):

Michael Soegtrop said:

What side effects would there be without the mutable?

there are no side effects, it's misclassified in the stm
open an issue
fix should be easy

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 20:44):

OK, I will create an issue. Thanks!

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 20:47):

even simpler example:

Require Import Ltac2.Ltac2.

Example Ex1: forall a : nat, True.
  intros a.
  Ltac2 Eval 'a.
  exact I.
Qed.

view this post on Zulip Michael Soegtrop (Jan 28 2022 at 20:48):

Thanks, I will update the issue! (https://github.com/coq/coq/issues/15569)

view this post on Zulip Gaëtan Gilbert (Jan 28 2022 at 20:49):

https://github.com/coq/coq/pull/15570


Last updated: Jan 31 2023 at 09:01 UTC