Does the coq-elpi -> Ltac1 bridge support `abstract`

? In particular, in `Defined`

blocks, `abstract`

has side effects defining global constants, and those don't seem to work correctly — they produce axioms, but when used manually they produce proofs. (This is with coq-elpi 1.14.0).

Here are the (non-minimized) symptoms:

```
Ltac solve_finite_nodup := vm_decide.
Ltac solve_finite_total := case; vm_decide.
Ltac solve_finite Fields :=
refine (@Build_Finite _ _ Fields _ _);
[ abstract solve_finite_nodup
| abstract solve_finite_total ].
Variant t := A | B | C.
#[global] Instance: EqDecision t.
Proof. solve_decision. Defined.
Definition t_finite2 : Finite t.
solve_finite [A; B; C].
Defined.
(* new elpi command producing `t_finite` using `solve_finite [A; B; C].` *)
Print t_finite2.
Print t_finite.
Print t_finite2_subproof.
Print t_finite2_subproof0.
Print elpi_subproof.
Print elpi_subproof0.
(*
t_finite2 =
{|
enum := [A; B; C];
NoDup_enum := t_finite2_subproof;
elem_of_enum := t_finite2_subproof0
|}
: Finite t
t_finite =
{|
enum := [A; B; C];
NoDup_enum := elpi_subproof;
elem_of_enum := elpi_subproof0
|}
: Finite t
t_finite2_subproof = (* ... defined correctly *)
t_finite2_subproof0 = (* ... defined correctly *)
*** [ elpi_subproof : NoDup [A; B; C] ]
*** [ elpi_subproof0 : ∀ x : t, x ∈ [A; B; C] ]
Arguments elpi_subproof0 x
*)
```

Forgot to add: it's likely I'm doing some naive mistake, but everything else _seems_ to work. Is there some way _I_ can screw up `abstract`

?

It is a bug, I did assume ltac1 tactics do not change the global environment...

Thanks a lot for confirming despite my incomplete example :-)

And I should say: I expected Coq-Elpi to be pretty good. In fact, getting started was even better, and Elpi was pretty forgiving :-)

The bad news is that it is not easy to fix... I'll sleep on it.

Good luck!

https://github.com/coq/coq/pull/16328 (it will work in 8.17, before it is too much work)

Thanks! That's unfortunate, but it's easy enough to avoid `abstract`

meanwhile thanks to elpi. As a sanity check, would the change let one reimplement `abstract`

or pieces thereof in coq-elpi — say if you need `abstract`

but aren't using ltac otherwise?

Filed as https://github.com/LPCIC/coq-elpi/issues/376, just for tracking (= to mention in our TODOs)

Last updated: Apr 14 2024 at 11:02 UTC