Stream: Ltac2

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

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.

Gaëtan Gilbert (Jan 28 2022 at 18:04):

example?

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.

Gaëtan Gilbert (Jan 28 2022 at 19:07):

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

Gaëtan Gilbert (Jan 28 2022 at 19:07):

not sure why it's not classified query tbh

Michael Soegtrop (Jan 28 2022 at 19:58):

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

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?

Michael Soegtrop (Jan 28 2022 at 20:41):

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

Gaëtan Gilbert (Jan 28 2022 at 20:42):

this is probably the replay of side effect commands

Michael Soegtrop (Jan 28 2022 at 20:43):

What side effects would there be without the mutable?

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 *)

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

Michael Soegtrop (Jan 28 2022 at 20:44):

OK, I will create an issue. Thanks!

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.

Michael Soegtrop (Jan 28 2022 at 20:48):

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

Gaëtan Gilbert (Jan 28 2022 at 20:49):

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

Last updated: Apr 19 2024 at 23:02 UTC