Port to Hierarchy Builder

[proux01]

C.f. https://github.com/math-comp/math-comp/pull/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 https://github.com/math-comp/algebra-tactics/blob/d4de5a2d05ab500017b272d9d37af7a05818d01e/examples/zmodule.v#L246-L247 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]

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]

Not the issue introduced by this PR, but CI recompiles the entire MathComp.

[proux01]

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.

Ok, removed it from the current PR for now.

[proux01]

Not the issue introduced by this PR, but CI recompiles the entire MathComp.

Yes this is the painful result of frequent edits to already released packages in the OCaml OPAM repo. Pinging the poor @erikmd but he already knows.

[pi8027]

Also, I wish to have an option to maintain a branch for MathComp 1 and to make it easier. For this reason, may I move changes indepondent of MathComp 2 (e.g., obvious fixes of typos) to #84 and then rebase this PR on top of #84?

[proux01]

Also, I wish to have an option to maintain a branch for MathComp 1 and to make it easier. For this reason, may I move changes indepondent of MathComp 2 (e.g., obvious fixes of typos) to #84 and then rebase this PR on top of #84?

Sure, feel free to.

Unrelated to this PR: we should probably consider merging the reification of expression between ring and lra, the current situation looks like almost duplicated code (even if it incurs an additional postprocessing in lra, it would probably be cheap enough).

[pi8027]

Unrelated to this PR: we should probably consider merging the reification of expression between ring and lra, the current situation looks like almost duplicated code (even if it incurs an additional postprocessing in lra, it would probably be cheap enough).

PExpr used in ring and lra are two different inductive data types, and divisions are restricted to divisions by constants in lra. So merging these two reification procedures is not straightforward. But, I have a mid- or long-term plan of mitigating the situation in a different way. We can discuss it during CUDW.

[erikmd]

Not the issue introduced by this PR, but CI recompiles the entire MathComp.

Yes this is the painful result of frequent edits to already released packages in the OCaml OPAM repo. Pinging the poor @erikmd but he already knows.

Yes, thanks @proux01.

This can be "easily" solved manually by triggering a rebuild (FWIW: one such rebuild is on-going)

In any case, we'll discuss this issue with @himito soonish, to try to (devise semi-automatic ways to) mitigate the issue.

[erikmd]

Above all, do not hesitate to ping me about this kind of issue anytime, in a github issue comment or on Zulip; I don't mind at all to receive more pings as soon as you notice some unsatisfactory slow-down in a Docker CI build, because of an [upstream or system changes] event; this kind of transient issue should be fixed quickly, if we can.

[proux01]

@pi8027 now that we have Docker images for mathcomp-dev, CI is green. I think it would be nice to merge this soon, so that it gets tested in MathComp CI and we don't break it again without noticing (like we just did with math-comp/math-comp#1031 ).

[pi8027]

I'm working on a fix. Please do not push anything.

[pi8027]

To share the brief idea of what I want to do, I pushed the new reflexive preprocessor. But, I don't have enough concentration to fix the reification procedure right now. I will retry tomorrow.

[pi8027]

I fixed the ring tactic. Now it should support commutative semirings, but I did not test it. We should fix the lra tactic (or reimplement it in the same way as ring if possible), but I have something more urgent to do now.

[proux01]

I'll have a look

[pi8027]

Thanks. Adding more tests would be an easy yet very helpful thing to do.

[pi8027]

Now it should support commutative semirings

As a consequence, we should be able to close #40.

[proux01]

I fixed the ring tactic. Now it should support commutative semirings, but I did not test it. We should fix the lra tactic (or reimplement it in the same way as ring if possible), but I have something more urgent to do now.

@pi8027 lra is now reusing the expression parser of ring (with minor tweaks to handle inverse of constants)

[pi8027]

@proux01 Thanks a lot! I may still have to fix my shortcoming regarding homomorphisms and variables. (For an application of homomorphism whose codomain is nat, N, int, or Z, we can discard accumulated homomorphism and replace it with thing like GRing.natmul 1. I need more constructors for homomorphism applications to properly implement this. On the other hand, we should be able to get rid of RnatX, RNX, RintX, and RZX.)

[proux01]

CI "green": the failures with MC2 are du to the Docker image not providing the master branch of mczify. Indeed, this will require a new release of mczify (for the semiring instances on nat) to work with MC2.

[proux01]

Another thing that seems a bit wasteful: constants like 42 being 42%:R, we end up with a lot of PEmul PE1 (PEc 42) in the reified term whereas we would expect PEc 42 to be enough.

[pi8027]

Another thing that seems a bit wasteful: constants like 42 being 42%:R, we end up with a lot of PEmul PE1 (PEc 42) in the reified term whereas we would expect PEc 42 to be enough.

I agree. I think we should do a proper benchmark on this. So I would like to fix that in another PR (after porting Apery if it is ok).

[proux01]

To be clear: I'm not really worried about the performance, the overhead is probably small. But this introduces complexity in the normalization function (in particular we wouldn't need that elaborate "push inverses below multiplication" just to parse constants in lra if the constant were normalized to PEc 42 rather than PEMul PE1 (PEc 42)). But I agree, the current thing is working and it would be nice to get a release for MC2 as soon as possible. Let's investigate that in another PR.

[pi8027]

Sharing Fnorm between field and lra seems to be a source of potential slowdown of field. I would rather split it into two.

[proux01]

I personally wouldn't do it without benchmarks showing a real slowdown (no "premature optimization"). But do as you prefer.

[pi8027]

I think reification of lra is completely broken because rquote does not have a flag corresponding to invb (otherwise I don't understand how it works yet). I also think sharing the normalization function and reification procedure between field and lra is really a bad idea because these two tactics need different preprocessors.

[proux01]

I think reification of lra is completely broken because rquote does not have a flag corresponding to invb (otherwise I don't understand how it works yet).

That's because invb is not a flag, contrary to push_inv. This is just an internal variable of Fnorm alway initialized to false. It's goal is just to push the inverses below multiplication, mirroring the behavior of quote.expr.inv in lra.elpi.

[pi8027]

Ok, I didn't see that, but:

1. The lra tactic in the master branch can treat (x * 10%:R)^-1 as x^-1 / 10%:R where x^-1 appears as a variable in the variable map. Pushing down the inverse by tweaking quote.expr.inv does not support this case.
2. I'm not so sure if I can maintain this code. For me, having a clearer correspondence between the interpretation/normalization functions and the reification procedure would be easier to understand.

[proux01]

1. The `lra` tactic in the master branch can treat `(x * 10%:R)^-1` as `x^-1 / 10%:R` where `x^-1` appears as a variable in the variable map. Pushing down the inverse by tweaking `quote.expr.inv` does not support this case.

I agree, that's a regression.

2. I'm not so sure if I can maintain this code. For me, having a clearer correspondence between the interpretation/normalization functions and the reification procedure would be easier to understand.

You're probably right that it would be better to have push_inv and invb booleans in rquote acting as in Fnorm. Are you doing it or do you want me to do it?

[pi8027]

Are you doing it or do you want me to do it?

I'm doing it but I'm slow. I also plan to duplicate the preprocessor so that I don't need push_inv (I hope it contributes to the "clearer correspondence").

[proux01]

I'm doing it but I'm slow. I also plan to duplicate the preprocessor so that I don't need push_inv (I hope it contributes to the "clearer correspondence").

Feel free to ask for help. I fear duplication would rather obfuscate the correspondence though but let's see the result (I would rather make push_inv a flag like field-mode and keep only invb as an actual argument of rquote).

[proux01]

@pi8027 here is what I would do: https://github.com/proux01/algebra-tactics/tree/hierarchy-builder-push-inv

[pi8027]

https://github.com/math-comp/algebra-tactics/blob/90979f3d1fd3cc9917c144a8263e39f6c967b5f8/theories/common.elpi#L425-L433 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: https://github.com/math-comp/algebra-tactics/blob/eeea90664e062d442b1e2123ee7b38f02fb33feb/theories/lra.elpi#L195-L199

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.