[CI] Remove paramcoq

[proux01]

The paramcoq plugin suffers universe issues on master that I'm not able to solve. This finally motivated me to port most of its few known users (that is, mostly CoqEAL) to elpi's derive.param2, which I hope will be easier to maintain. I'll do a last (buggy) release of the plugin for Rocq 9.0 before archiving it, so we no longer need to maintain it in the CI of the master branch here.

[SkySkimmer]

The paramcoq plugin suffers universe issues on master that I'm not able to solve.

Why are these issues not breaking master's CI?

[proux01]

The paramcoq plugin suffers universe issues on master that I'm not able to solve.

Why are these issues not breaking master's CI?

Because the test-suite of paramcoq was too weak and the issue only appeared in CoqEAL (which isn't in Coq's CI) (c.f. #19228 )

[proux01]

The mtac2 failure is unrelated, so CI green here.

[ppedrot]

I'm not actually convinced it's a good idea to let paramcoq rot. Even though there are corner cases, it's still useful to check that the code compiles, especially because the template mess is a transitory state. Hopefully with the algebraic universes around the corner it'll make things much smoother.

[proux01]

Well, it's now redundant with elpi derive, so we'd better maintain a single plugin rather than two.

[proux01]

But we could consider adding CoqEAL to the CI if we want to exercise those things more.

[palmskog]

Please consider keeping paramcoq in CI until its use cases can be accommodated by Trocq (and CoqEAL ported to Trocq), see for example rocq-community/trocq#40

[proux01]

Which use cases are you thinking about precisely?
Note that CoqEAL is already ported to Elpi derive.

[palmskog]

The obvious use case is: (1) generating parametricity theorems and (2) using those parametricity theorems in refinement proofs (and also type equality/isomorphism transfers). Does Elpi derive really provide this? I wouldn't consider it a "port" unless the proofs are done the same way.

[proux01]

It provides essentially the same thing as paramcoq.

[palmskog]

I think the following is completely incomprehensible to anyone who doesn't know Elpi:

Elpi derive.param2 expQnat'.
Definition expQnat_R := expQnat'_R.
Elpi Accumulate derive Db derive.param2.db.
Elpi Accumulate derive.param2.db "
:before ""param:fail""
param {{ @leq }} {{ @leq }} {{ @leq_R }}.
".
Elpi derive.param2 cast_ZQ.
Elpi derive.param2 cast_PQ.

And the port has lots of these. I still think the best is to keep Paramcoq's interface, rather than forcing Elpi on its users, with an eye towards a transition to Trocq.

[proux01]

That's just a syntactic detail that needs to be improved, I agree. But that should be trivial to do.

[proux01]

Closing this according to last Coq call discussion: https://github.com/coq/coq/wiki/Coq-Call-2025-01-28 (@ppedrot will keep maintaining paramcoq as a Coq API testcase, there will no longer be any release following 9.0 and we will warn potential users not to use it).