port to coq-elpi 1.10

[gares]

Here the fix, and also an example showing a bug in Coq-Elpi.

In Coq-Elpi master I made coq.error raise an error catch by Ltac, and you have a new coq.abort to raise a fatal one. I'm still not 100% convinced it is the right default, since std.assert! uses coq.error and not abort, unless you add @fatal! => .... In your code I'd say that all current errors are not fatal in this sense, at least not in the standard ring tactic, so it seems the right default.

Btw, I think we should update the other error messages using the strings from the Coq manual (see https://coq.inria.fr/refman/addendum/ring.html#coq:exn.Not-a-valid-ring-equation)

Fixes #1

[gares]

maybe std.time( std.assert! (coq.ltac1.call ...) "Not a valid ring equation." ) ReflTime is a better code then the one I wrote.

[pi8027]

In Coq-Elpi master I made coq.error raise an error catch by Ltac, and you have a new coq.abort to raise a fatal one. I'm still not 100% convinced it is the right default, since std.assert! uses coq.error and not abort, unless you add @fatal! => .... In your code I'd say that all current errors are not fatal in this sense, at least not in the standard ring tactic, so it seems the right default.

IMO, it is better to have a new one that can be caught by Ltac and can also take a failure level as an argument.

Btw, I think we should update the other error messages using the strings from the Coq manual (see https://coq.inria.fr/refman/addendum/ring.html#coq:exn.Not-a-valid-ring-equation)

Sure. Will do.

[gares]

IMO, it is better to have a new one that can be caught by Ltac and can also take a failure level as an argument.

So you are suggesting to go the other way? I mean make it so that std.assert! is fatal, unless you pass @ltacfail! Level => ? I like the code that has a lot of assert!, I'd like to keep this style.

[pi8027]

So you are suggesting to go the other way? I mean make it so that std.assert! is fatal, unless you pass @ltacfail! Level => ? I like the code that has a lot of assert!, I'd like to keep this style.

@ltacfail! Level => std.assert! ... seems sensible to me.

[gares]

OK, you convinced me https://github.com/LPCIC/coq-elpi/commit/e97eb21674ae991172d5e47b175b7167ae8287f1

I've one item left before releasing 1.10 (make refine use Coq's refine by default).

[pi8027]

OK, you convinced me LPCIC/coq-elpi@e97eb21

I've one item left before releasing 1.10 (make refine use Coq's refine by default).

Thanks. That seems to work now. I will wait for 1.10.

[gares]

@amahboubi I've rebased this PR on master and I found the diverging example, thanks for sharing that. (This PR is about better interfacing the tactic with Coq using the to-be-released-tomorrow version of Coq-Elpi).

I did try, by hand, the idea I shared on zulip, and it seems to work, see commit 9274f07. I think one could enhance the reification procedure by detecting and abstracting out large constants. The code of Enzo should almost implement the have/rewrite thing, and the current tactic is already able to deal with equations.

[pi8027]

FYI, I plan to propose a solution to the performance issue after merging this PR. My solution will also add support for morphisms at the same time. (There is an issue opened for that: #4.)

[gares]

Another thing, maybe the tactic notation should be ring: H1 H2..., it's more MC like. I did not try, but we should be able to do

Tactic Notation "ring" := ...
Tactic Notation "ring" ":" ne_constr_list(L) := ....

(edit, the ne_ things makes the list non-empty, see https://coq.inria.fr/distrib/current/refman/user-extensions/syntax-extensions.html#tactic-notations)

[gares]

We could also try ne_hyp_list (not sure it works, if so I'll fix coq-elpi before releasing)

[gares]

no, hyp does not work.

[pi8027]

Since we sometimes want to write a proof term as an argument, ne_constr_list would be appropriate here. No?

[gares]

the dev job needs https://github.com/coq/coq/pull/14357

[pi8027]

Let's remove dev for now and merge.

[pi8027]

Also, I made algebra-tactics public. Thanks, @gares!