Lookup abstracted terms using unification

[Tragicus]

When quote.ring finds a term that it can not translate, it looks it up in a list of terms it has already abstracted and if it does not find it adds it to the list. This is not robust to composition of coercions however, since it uses equality of terms instead of unification.

[pi8027]

In my opinion, it has to be done by keyed matching: we first compare the head symbols, and perform conversion only when the head symbols are the same. I also wish to have a mechanism to cache the results of conversion. See #18.

[pi8027]

Error: Failed to get sources of coq-mathcomp-algebra.2.2.0, coq-mathcomp-character.2.2.0, coq-mathcomp-field.2.2.0, coq-mathcomp-fingroup.2.2.0, coq-mathcomp-solvable.2.2.0, coq-mathcomp-ssreflect.2.2.0 (https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz): Bad checksum

Is this one of the unexpected consequences of what we did this morning? @CohenCyril

[Tragicus]

I would not think it is on the critical path for performance, this is only for terms that can not be translated, and I would have thought that the costlier part is the decision procedure. Do we have any benchmark?

[pi8027]

Do we have any benchmark?

examples/from_sander.v and Apery.

[pi8027]

According to https://inria.hal.science/hal-00984057v1/, one call of ring in Apery handles 18,602 occurrences of variables. If there are 10 variables, we probably call coq.unify-eq about 100,000 times.

[Tragicus]

+3% in from_sanders.v

[CohenCyril]

Error: Failed to get sources of coq-mathcomp-algebra.2.2.0, coq-mathcomp-character.2.2.0, coq-mathcomp-field.2.2.0, coq-mathcomp-fingroup.2.2.0, coq-mathcomp-solvable.2.2.0, coq-mathcomp-ssreflect.2.2.0 (https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz): Bad checksum

Is this one of the unexpected consequences of what we did this morning? @CohenCyril

Yes, most probably, so I revert for now

[Tragicus]

Would that be better (+1% in from_sanders.v)? Unfortunately, I can not test if it solves my issue, so I can not be absolutely sure, but I would be very surprised it does not. Nevermind, I could test it and it works.

[pi8027]

+1% sounds ok for me. What about Apery? (I suggest to insert time before the three heavy calls of ring field. There are two in the recAperyB lemma and one in the P_eq_Delta_Q lemma.)

[pi8027]

Looks ok to me. Performance evaluation is needed.

[Tragicus]

I get +.1%, -1% and -2% for the three field; ring_lia that are marked as slow in ops_for_b.v.

[pi8027]

FTR: I still wish to see the overall performance change of Apery. To do so, you probably need to use Coq 8.20.

[Tragicus]

-.07% on Apery.