Stream: Coq devs & plugin devs

Topic: Looking for reviewer for AAC Tactics universe fix


view this post on Zulip Karl Palmskog (Mar 13 2022 at 14:14):

Since 8.10, AAC Tactics had a universe constraint issue when reasoning over lists with elements in Type (and presumably other parameterized datatypes). Tactics like aac_reflexivity succeeded but Qed failed with universe mismatch error (described here).

By experimentation, I came up with a solution that makes the main test case with lists pass. However, it uses monomorphic universes nontrivially, and I don't know if there is a more general solution (if I use explicit universe polymorphism I get Anomaly "new_monomorphic_global raised an error ...").

Any chance some universe expert could review the PR? https://github.com/coq-community/aac-tactics/pull/112

view this post on Zulip Pierre-Marie Pédrot (Mar 13 2022 at 14:38):

At best this is a workaround, tactics should never generate ill-typed terms.

view this post on Zulip Pierre-Marie Pédrot (Mar 13 2022 at 14:38):

Most probably the OCaml code of AAC forgets some constraints

view this post on Zulip Karl Palmskog (Mar 13 2022 at 15:11):

sure, the best fix would be at the OCaml level, but this code was originally written 10+ years ago and is likely not known very well by anyone anymore... I just try to solve the worst issues for users when I can.

view this post on Zulip Karl Palmskog (Mar 13 2022 at 15:14):

so if we can agree on that the PR at least doesn't make anything worse or is fundamentally broken, I think it's reasonable to merge. Recall that AAC is in Coq's CI and the Platform, so everyone will have to live with it for a while.

view this post on Zulip Karl Palmskog (Mar 13 2022 at 16:01):

one effect of the PR is that this can become Type again...

view this post on Zulip Hugo Herbelin (Mar 14 2022 at 10:58):

Could it be the lift_reflexivity which is missing a tclRETYPE so that its inner universe constraints are propagated?

view this post on Zulip Karl Palmskog (Mar 14 2022 at 10:59):

@Hugo Herbelin possibly. Fabian wrote about tclRETYPE before (https://github.com/coq-community/aac-tactics/issues/36):

The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?). This seems very fishy and like an ugly hack.

view this post on Zulip Karl Palmskog (Mar 14 2022 at 11:00):

if you give an example how to add tclRETYPE to lift_reflexivity I can try that in a new PR

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 11:09):

every time you build an application in OCaml you should check that the universe constraints are properly handled

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 11:10):

it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)

view this post on Zulip Karl Palmskog (Mar 14 2022 at 13:39):

I tried Hugo's advice and it seems to work: https://github.com/coq-community/aac-tactics/pull/113

view this post on Zulip Hugo Herbelin (Mar 14 2022 at 13:47):

Good that it works.
Pierre-Marie Pédrot said:

it's a bit violent to type every thing at sight (I've been removing a lot of useless retyping last week for performance reasons, it doesn't scale at all)

Yes, it is a lot of useless retyping, as what we only need here a priori is to ensure that the first argument in Type infers a constraint. The advantage is that it is easy to do fix with the current AAC architecture. (Case by case, we could work on each different mkApp(Coq.get_efresh ..., carrier) pattern and infer the constraint on the carrier, but that would require more time.)

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 13:48):

In the case of AAC I don't think it's the major source of performance issues, so probably not very important in first approximation

view this post on Zulip Karl Palmskog (Mar 14 2022 at 13:50):

am I reading it right that tclRETYPE could potentially do wasteful work? Worth opening an issue in AAC to remember?

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 13:52):

Yes, this function retypes the whole term. So if you call it recursively, expect some blowups on big terms

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 13:53):

but last time I had a look, AAC was struggling orders of magnitudes worse with TC resolution

view this post on Zulip Pierre-Marie Pédrot (Mar 14 2022 at 13:53):

(anyone up to reimplementing AAC with CS?)

view this post on Zulip Karl Palmskog (Mar 14 2022 at 13:54):

the better approach may be to reimplement AAC using Enrico's planned tabled TC resolution?

view this post on Zulip Karl Palmskog (Mar 14 2022 at 13:55):

I think https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v solves an important part of what AAC does already using CS

view this post on Zulip Karl Palmskog (Mar 14 2022 at 13:56):

that is, I think many applications don't require the full "modulo AC" so "with AC" suffices

view this post on Zulip Hugo Herbelin (Mar 14 2022 at 15:55):

In the same vein, there is applys_eq from TLC, which, combined with ring should give something similar. Would be good if someone can make a synthesis of these ideas.


Last updated: Oct 13 2024 at 01:02 UTC