`aac_normalize` throws despite `try`

[aa755]

Lemma foo: forall X:Prop, X->X.
try aac_normalise.
(* Error: [aac_tactics] The goal is not an applied relation *)

I would like to call try aac_normalise on all goals but this prevents me from doing so. Is there a workaround?

Also, the exception that aac_normalise throws seems wierd: once it threw when it was called in a deep ltac2 stack, but the ltac2 backtrace was empty. (I can produce a minimal example if that helps.) Does it discard the entire stack?

Can aac_normalise just not fail? A user can check whether it did anything by wrapping it around progress. The missing call stack would make it hard to debug failures of complex tactics that call aac_normalise if that fails

[aa755]

aac_rewrite has the same behaviour:

Lemma foo: forall X:Prop, X->X.
try aac_rewrite Z.gcd_mod.
(* Error: [aac_tactics] The goal is not an applied relation *)

[aa755]

I cannot catch the exception even in ltac2:

Lemma foo: forall X:Prop, X->X.
  ltac2:(Control.plus (fun _ => ltac1:(aac_rewrite Z.gcd_mod)) (fun _ => ())).
  (* Error: [aac_tactics] The goal is not an applied relation *)

[SkySkimmer]

Ltac2 is not more capable of catching exceptions than ltac1 so that's normal.

[SkySkimmer]

Cannot reproduce with

From AAC_tactics Require Import AAC.

Lemma foo: forall X:Prop, X->X.
  try aac_normalise.
  (* succeeds doing nothing *)

on coq master, aac-tactics master

[aa755]

Thanks for investigating. I will try to reproduce it on coq master, aac-tactics master and report back. The errors above where from aac-tactics bf4e295d8edea5f27c2a532faa760effbff989c2 and coq 8.19.0 compiled with OCaml 4.14.1:

coq@7ca81cc6c350:~/aac-tactics$ git log           
commit bf4e295d8edea5f27c2a532faa760effbff989c2 (HEAD -> canonical-ordering, origin/canonical-ordering)
Author: Damien Pous <damien.pous@ens-lyon.fr>
Date:   Fri May 31 16:00:59 2024 +0200

    changelog
....
coq@7ca81cc6c350:~/aac-tactics$ coqc --version
The Coq Proof Assistant, version 8.19.0
compiled with OCaml 4.14.1
coq@7ca81cc6c350:~/aac-tactics$ coqtop
Welcome to Coq 8.19.0

Coq < From AAC_tactics Require Import AAC.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file aac_plugin.cmxs (using legacy method) ... done]

Coq < Lemma foo: forall X:Prop, X->X.
1 goal

  ============================
  forall X : Prop, X -> X

foo < try aac_normalise.
Toplevel input, characters 0-18:
> try aac_normalise.
> ^^^^^^^^^^^^^^^^^^
Error: [aac_tactics] The goal is not an applied relation

foo <

[aa755]

I can confirm that this issue does not occur with coq master: https://gist.github.com/aa755/a7ae663b196ee60f9ff4c601e76bc976#file-gistfile1-md

The implementation of aac tactics seem to have not changed since the version above where I can reproduce the issue. So it seems this got fixed by some changes in coq.

[palmskog]

@aa755 could you check if it occurs on Coq's v8.20 branch? If the issue is gone there, then this bug will be gone when I release AAC Tactics for 8.20, which will happen shortly after the release candidate for Coq 8.20.0 is out (which I think is in a few weeks).

[palmskog]

There is already a v8.20 branch of AAC Tactics, but currently it's identical to master: https://github.com/coq-community/aac-tactics/tree/v8.20

[SkySkimmer]

8.20 RC is expected tomorrow according to https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.20

[aa755]

@aa755 could you check if it occurs on Coq's v8.20 branch? If the issue is gone there, then this bug will be gone when I release AAC Tactics for 8.20, which will happen shortly after the release candidate for Coq 8.20.0 is out (which I think is in a few weeks).

There is already a v8.20 branch of AAC Tactics, but currently it's identical to master: https://github.com/coq-community/aac-tactics/tree/v8.20

So, there is nothing to test for now? If you want me to test something, let me know and I will be happy to.

[palmskog]

So, there is nothing to test for now? If you want me to test something, let me know and I will be happy to.

@aa755 I was suggesting you do the following:

• install the v8.20 branch of Coq, for example via the core-dev opam repository (coq.8.20.dev)
• checkout the v8.20 branch of AAC Tactics, and run make and make install (or you can pin the Git repo and install the in-repo opam package)
• try to reproduce the error like Gaëtan did here
• report back here

When 8.20+rc1 is packaged via opam (may be a few days) I can try reproducing with that, but the above would give us fast feedback.

[palmskog]

@aa755 I can confirm that the following works on Coq 8.20+rc1:

From AAC_tactics Require Import AAC.
From Coq Require Import ZArith.

Goal forall X:Prop, X->X.
Succeed (try aac_rewrite Z.gcd_mod).
Abort.

Goal forall X:Prop, X->X.
Succeed (try aac_normalise).
Abort.

So I will close this issue after I release AAC Tactics 8.20.0 (will happen soon). Please reopen if the problem reappears. Unfortunately, this will not be solved on Coq 8.19.

[palmskog]

Release for 8.20 is done and submitted to the Coq opam archive (extra-dev repo for the moment, but will be moved to released once 8.20.0 is out): https://github.com/coq/opam/pull/3059

[aa755]

Thanks. Sorry I was not able to help soon enough. I was planning to do it this weekend.