Port to Hierarchy Builder

[proux01]

C.f. math-comp/math-comp#733

[proux01]

So, here is a version that is compatible with both MathComp 1 and 2, that should avoid having to manage multiple versions and means, provided CI is green, we could merge this without waiting for MathComp 2.

[proux01]

So, CI almost green. I removed mathcomp:1.15.0-coq-dev because 1.15 doesn't compile anymore on Coq master.

But, with the coq-master branch of elpi, we have a

Anomaly "Uncaught exception Not_found."

on that line

algebra-tactics/examples/zmodule.v

Lines 246 to 247 in d4de5a2

	coq.ltac.call "poly_zmodule_reflection"
	[trm V, trm VarMap, trm ZE1, trm ZE2] G GS.

even if I replace the body of the ltac tactic above with idtac.
This is not specific to that PR and also happens on master. @gares, does that ring a bell?

[gares]

no idea

[proux01]

Here is a reduced example:

From elpi Require Export elpi.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Ltac ltac_foo := idtac.

Elpi Tactic fail_foo.
Elpi Accumulate lp:{{

pred solve i:goal, o:list sealed-goal.
solve (goal _ _ _ _ [_] as G) GS :-
  coq.ltac.call "ltac_foo" [] G GS.

}}.
Elpi Typecheck.

Goal True.
Proof.
elpi fail_foo ([the Equality.type of unit : Type]).
Qed.

According to the backtrace:

Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
Raised at file "clib/int.ml", line 39, characters 14-29
Called from file "src/coq_elpi_HOAS.ml", line 1183, characters 41-59
Called from file "src/coq_elpi_HOAS.ml", line 2068, characters 4-57

pointing to https://github.com/LPCIC/coq-elpi/blob/c245284c3bc5ffa6fba6935253b4110c8b9360c6/src/coq_elpi_HOAS.ml#L1183 it could be a missing evar, but no idea why.

[gares]

I see, I guess it is the same here: https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/Error.20.60Not.20a.20variable.20after.20goal.60

[gares]

I guess first I'll move coq-master to point to a recent coq-elpi, and then I'll re run the job

[pi8027]

@proux01 I'm mostly done fixing the lra tactic in the master branch (see #73 for TODOs). I think now you may rebase this branch without making many conflicts.

[proux01]

@pi8027 thanks! This might take me a few days, being pretty busy currently.

[gares]

I'm recompiling it, there is a zmodType in lra.elpi which needs to be replaced with the new name

[pi8027]

@gares Sorry for the mess. Fixed.

[gares]

I did the fix myself here and uploaded a new jscoq yesterday night, lesson8 works

[proux01]

@pi8027 thanks for the rebase! Looks to me like this works with the HB branch of MathComp and is backward compatible (the issue with coq-dev seems unrelated) so this can probably be merged whenever you want.

[pi8027]

@proux01 For the above reason, I cannot merge this PR for the moment. Since the issue is independent of Algebra Tactics, I will produce a smaller example explaining the issue.

[proux01]

@pi8027 should this be merged now?

[pi8027]

Sorry for the late response. I'm still hesitating to merge this PR for the following reasons. But, I can propose a "compromise plan".

[pi8027]

Also, I don't think we want to merge the workaround specific to jsCoq in the master branch. In theory, it has to be fixed in somewhere else.

[pi8027]

algebra-tactics/theories/common.elpi

Lines 425 to 433 in 90979f3

	irquote Inv C {{ @GRing.add lp:U lp:In1 lp:In2 }}
	{{ @RAdd lp:R lp:OutM1 lp:OutM2 }} Out' VM :-
	can-inv Inv,
	coq.unify-eq { rmorphism->nmod C } U ok,
	rmorphism->sring C R, !,
	rquote C In1 OutM1 Out1 VM, !,
	rquote C In2 OutM2 Out2 VM, !,
	quote.expr.add Out1 Out2 Out,
	quote.expr.cond-inv Inv Out Out'.

When we see (x + y)^-1, we should not reify x and y because we do not have the multiplicative inverse in the reified syntax for the lra tactic. This rule should apply only when Inv = ff, as it is the case in the master branch:

algebra-tactics/theories/lra.elpi

Lines 195 to 199 in eeea906

	quote.expr ff R F TR TUR Morph {{ @GRing.add lp:U lp:In1 lp:In2 }}
	{{ @RAdd lp:R lp:OutM1 lp:OutM2 }} {{ PEadd lp:Out1 lp:Out2 }} VM :-
	ring->zmod R U, !,
	quote.expr ff R F TR TUR Morph In1 OutM1 Out1 VM, !,
	quote.expr ff R F TR TUR Morph In2 OutM2 Out2 VM.

Again, I'm working on it.

[proux01]

When we see (x + y)^-1, we should not reify x and y because we do not have the multiplicative inverse in the reified syntax for the lra tactic. This rule should apply only when Inv = ff

I agree, and that's exactly what the code does thanks to the can-inv test.

[pi8027]

I don't understand why you needed can-inv, because we should use the reification procedure from the ring tactic when the target of the lra tactic is not a field. Also, I don't understand why you call rquote inside irquote (which would have the consequence that we cannot handle things like 1^-1 + y correctly).

[proux01]

I don't understand why you needed can-inv,

To be able to share the reification procedure between all tactics (that's why it is in common.elpi).

because we should use the reification procedure from the ring tactic when the target of the lra tactic is not a field.

I haven't really considered the case of expressions containing ^-1 on a unitRing that is not a fielf, that might indeed fail. But that's probably a relatively uncommon use case (at least we don't have any test for it).

Also, I don't understand why you call rquote inside irquote (which would have the consequence that we cannot handle things like 1^-1 + y correctly).

rquoite is just a shortcur for irquote ff so I'm not sure I understand your concern. When reifying 1^-1 + y, the call to rquote 1^-1 will call irquote ff 1^-1 which will call irquote tt 1 eventually returning 1.

[pi8027]

I thought you implemented what I suggested, but that was not true. So never mind. I pushed my fix.

[pi8027]

zmodule.v is the running example for the paper "Reflexive tactics for algebra, revisited". So please try to keep the same structure as much as possible and do not rename things, e.g., MMorph. (It is also acceptable to just remove it for the moment, since it is available on Zenodo anyway.)

[proux01]

I thought you implemented what I suggested, but that was not true. So never mind. I pushed my fix.

No, sorry, I didn't catch all the details of what you wanted to do.

Thanks for the code! I had a careful look and it looks good to me.
I think that, modulo the discussion about all the *__canonical__* (without forgetting GRing_Zmodule__to__GRing_Nmodule in common.v that is only used in zmodule.v), it can be squashed, merged and released.

I still feel there is a massive amount of duplication in all this code though. But fixing that would probably require some major refactoring and definitely doesn't belong to the current PR.

zmodule.v is the running example for the paper [...]

Thanks for the explanation.

[pi8027]

Regarding the "duplication" between the reification procedures for field and lra, the reason to duplicate it is not only performance. For me, the preprocessors required for these two tactics are different enough to implement two different reification procedures.
Also, the preprocessors are becoming more and more difficult to maintain anyway. I believe that we should eventually generate the reification procedures automatically to address this maintainability issue (which is really a long-term goal).

[proux01]

I'm not sure I understand what you mean by "automatically generating the reification procedure"? I wonder whether we shouldn't completely change the parsing model with more intermediate languages, a reification procedure that would perform less work and could be shared, then a first simplification pass to a simpler intermediate language, finally the normalization procedures specific to each tactic (that would have to modify the variable map VM). But that's not a very precise idea and I agree about the "long-term goal" part.

[pi8027]

The functionality I need would be similar to the quote tactic bundled in some older versions of Coq. But, instead of just taking the interpretation function and performing reification, I'm thinking about translating the interpretation function to a set of Elpi rules that performs reification. This is not sufficient in our case since we have two kinds of reified terms, but I have another vague idea to overcome this difficulty.

[pi8027]

Apparently, coq.elpi.accumulate-clauses is available only from Coq-Elpi 1.18.0 that requires Coq 8.17. Is it ok to drop the support for Coq 8.16, or should we use coq.elpi.accumulate instead?

[proux01]

Apparently, coq.elpi.accumulate-clauses is available only from Coq-Elpi 1.18.0 that requires Coq 8.17. Is it ok to drop the support for Coq 8.16, or should we use coq.elpi.accumulate instead?

Since MC 2.0.0 supports 8.16, it would probably be nice to keep supporting it. Considering the number of clauses, the performance impact of using accumulate instead of accumulate-clauses is likely negligible.

[gares]

If you are not accumulating thousands of clauses, the new API provides no gain. In HB we accumulate like 60k clauses, grouping them changes the perf. If you are accumulating 100, you don't need the new API.

[pi8027]

Ok.

Considering the number of clauses, the performance impact of using accumulate instead of accumulate-clauses is likely negligible.

Also, the accumulation happens only when compiling Algebra Tactics. So I would say it is irrelevant to the performance from the user's perspective.

[proux01]

To be precise, it's also about the Elpi Accumulate Db canonicals.db. that happens at each tactic call. But again, considering the number of clauses, not an issue here.

[pi8027]

Shall we merge? Feel free to squash a bit but I'm not going to do that by myself.

[proux01]

Shall we merge?

Sure 🎉

Feel free to squash a bit

done

[proux01]

@pi8027 do you plan to do a release? (I can handle the OPAM and Nix packages)

[pi8027]

@proux01 I'm waiting for the green light here: coq-community/apery#16. Meanwhile, I drafted the release (I think you have access).