Stream: Coq devs & plugin devs

Topic: Finding differences in identical proof terms


view this post on Zulip Janno (Oct 08 2020 at 18:22):

(Sorry for the click-bait topic title!) I have two seemingly identical proof terms, one generated through Ltac2 and one through Mtac2, that have very different Qed performance behavior: the one from Mtac2 (let's call that term M) exhibits quadratic scaling (w.r.t. to my work factor) whereas the term generated via Ltac2 (let's call that L) scales linearly (or close to it). They print identically. How do I figure out what the actual difference is?
Here are some things that might help people point me in the right direction:

view this post on Zulip Enrico Tassi (Oct 08 2020 at 18:28):

IIRC Set Printing All does not print the type of variables bound by match branches. Each branch starts with as many lambdas as constructor arguments. I would try to print all match branches in isolation to rule out this.

view this post on Zulip Janno (Oct 08 2020 at 18:34):

Interesting. Do I have to write my own printing code to print those branches or is there a function for that somewhere?

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2020 at 18:35):

What about the usual suspects, i.e. universes?

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2020 at 18:35):

They might get printed the same but the underlying representation can be different if they haven't been normalized upfront

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2020 at 18:36):

sweep_slice is just the GC btw, the relevant data would be the callers of that function

view this post on Zulip Janno (Oct 08 2020 at 18:43):

Oh, I had forgotten about universes. Indeed, they use different universe assignments and (as usual) Mtac2 generates a gazillion universes, of which almost none end up in the proof term. In fact, Mtac2 re-uses a bunch of global universes in the proof term whereas Ltac2 generates fresh ones. Sadly, universe-related functions basically don't show up in the profile.

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2020 at 18:47):

If you give here the callers of sweep_slice we might get an idea of the culprit(s)

view this post on Zulip Janno (Oct 08 2020 at 18:49):

I am trying but OCaml is defeating me.. this is the best I can do: https://share.firefox.dev/30I6j1m

view this post on Zulip Janno (Oct 08 2020 at 18:50):

I don't think there is anything useful in that flame chart.. The stack samples are almost all broken because the stack is far too large for the maximum stack size of perf :(

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2020 at 18:50):

it's not loading :/

view this post on Zulip Janno (Oct 08 2020 at 18:51):

Yeah, it's rather big.. In any case, it seems the firefox profiler discards broken samples so this won't help much

view this post on Zulip Janno (Oct 08 2020 at 18:51):

Let's see what I can do locally

view this post on Zulip Janno (Oct 08 2020 at 18:52):

Oh, this explains a lot: sweep_slice only shows up in my initial profile but it doesn't show up any more :(

view this post on Zulip Janno (Oct 08 2020 at 18:55):

Yeah, depending on how I backtrack through the file either the Ltac2 or the Mtac2 version ends up with a sizeable GC item in perf (mark_slice or sweep_slice). Is it worth investigating this?

view this post on Zulip Janno (Oct 09 2020 at 09:02):

I am still trying to learn anything from these (broken) perf profiles. One thing that seems interesting is that the Mtac2 version of the proof term spends a lot of time in Typeops.execute_is_type and Typeops.check_cast whereas the Ltac2 version doesn't seem to be calling either function enough for it to show up in the perf samples. Does this point to anything?

view this post on Zulip Janno (Oct 09 2020 at 09:04):

Neither version of the term has any casts as far as I can tell from printing it with Set Printing All. (They really look 100% identical when printed except for universes.)

view this post on Zulip Enrico Tassi (Oct 09 2020 at 09:12):

check_cast is also used for let-ins and primitive types. Do you have let-ins holding a term in Type? (I just discovered the type of that term is not always printed)

view this post on Zulip Enrico Tassi (Oct 09 2020 at 09:12):

I mean the term contructor for let holds a type. if its sort is Type, then Coq pretty printer may hide it.

view this post on Zulip Janno (Oct 09 2020 at 09:13):

I think I there is not a single let binding in that proof term

view this post on Zulip Janno (Oct 09 2020 at 09:14):

Or, rather, in its type

view this post on Zulip Enrico Tassi (Oct 09 2020 at 09:14):

grep for yourself https://github.com/coq/coq/blob/master/kernel/typeops.ml check_cast ;-)

view this post on Zulip Janno (Oct 09 2020 at 09:14):

Yeah it's only casts and let-ins :(

view this post on Zulip Janno (Oct 09 2020 at 09:15):

I could see how casts could sneak in with one tactic language versus the other.. but let bindings? in a term that prints identically for both tactic languages?

view this post on Zulip Janno (Oct 09 2020 at 09:25):

Ugh.. as usual, the problem is me. There was a difference between the proof terms (one innocent little ') and I just didn't see it yesterday. I'll report back if the difference persists after I fix this. Thanks for your help!

view this post on Zulip Janno (Oct 09 2020 at 09:43):

Okay, so the proof terms were different but fixing the difference doesn't change anything. In fact even if I just skip Ltac2 altogether and simply use refine M (M being the proof term generated by Mtac2) in a fresh Goal I observe fast Qed performance (as with Ltac2). But in the goal where I take M from (via Show Proof) Qed is slow.

view this post on Zulip Janno (Oct 09 2020 at 09:45):

Even if I execute the Mtac2 tactic on a freshly generated evar (i.e. not on the current goal) to litter the proof state with universes and then solve the goal with refine M I get fast Qed..

view this post on Zulip Gaëtan Gilbert (Oct 09 2020 at 09:51):

does Show Universes say there are a lot of universes just before Qed?

view this post on Zulip Janno (Oct 09 2020 at 09:52):

Yes, both when calling the Mtac2 tactic without using the result and when calling it on the actual goal.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:52):

@Enrico Tassi was maybe right then, it could well be some hidden stuff in the branches. Do you use inductive types with let-bindings in them?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:53):

Pattern-matching branches are highly redundant so if you're unlucky enough to reduce the type of their arguments you're going to have a bad time.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:54):

(see e.g. https://github.com/coq/coq/pull/9710)

view this post on Zulip Janno (Oct 09 2020 at 09:55):

No let bindings as far as I can tell; neither in the proof term nor its type nor in the (inductive) types it uses.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:55):

Not even in the return type of a pattern-matching?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:56):

I've had a similar problem once and it's infuriating, because there is literally no way to see the difference from user land

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:56):

you have to dump the term in OCaml

view this post on Zulip Janno (Oct 09 2020 at 09:57):

Oh, there actually is a let binding hidden in a fun '{|..|}.

view this post on Zulip Janno (Oct 09 2020 at 09:57):

should I write that out manually as a match to make sure the match is annotated in the simplest way possible?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 09:59):

You may definitely try.

view this post on Zulip Janno (Oct 09 2020 at 10:01):

No difference.. I suppose OCaml it is then.

view this post on Zulip Janno (Oct 09 2020 at 10:01):

(No difference as in: there is still a difference.)

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:02):

just load the debugger and set a breakpoint in Typeops

view this post on Zulip Janno (Oct 09 2020 at 10:03):

I don't think I have a coqtop.byte available in this switch :(

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 10:06):

(deleted)

view this post on Zulip Janno (Oct 09 2020 at 10:22):

Okay, I used Termops.Internal.debug_print_constr_env to get a slightly more detailed view at the proof term and it really is 100% identical to what I feed to refine. I think that means the slowdown has to come from something that happens during Mtac2 tactic execution but only when the result of the tactic is actually used to solve the goal.

view this post on Zulip Janno (Oct 09 2020 at 10:23):

Although that doesn't explain difference in the perf profiles (if those still exist; I need to make new profiles).

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:23):

That's the printer that outputs the horrendous stuff, right?

view this post on Zulip Janno (Oct 09 2020 at 10:24):

Yes :)

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:24):

Like, bound variables are written #0 and the like?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:25):

(This printer can be overloaded IIRC, so you better be sure it's giving you full debug info)

view this post on Zulip Janno (Oct 09 2020 at 10:25):

I don't know about bound variables but it outputs Constr(Coq.Init.Datatypes.nat,0,2) instead of S.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:25):

Yes, looks like it.

view this post on Zulip Janno (Oct 09 2020 at 10:27):

Ah right I see the variables now. Indeed it uses #.

view this post on Zulip Janno (Oct 09 2020 at 10:30):

Oh, actually, maybe I do see something in the debug output. I thought it had printed the type of the term but maybe there is actually a cast in there. casts don't have nodes like Constr, do they?

view this post on Zulip Janno (Oct 09 2020 at 10:33):

Okay, the code tells me that casts are printed as (_ : _). It seems there really is a cast hiding in my proof term.

view this post on Zulip Janno (Oct 09 2020 at 10:33):

That's good news.. or, rather, it is at least consistent with the perf profile

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:33):

Yes, this debug printer is a bit too unstructured

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 10:34):

It'd be nice to belch sexprs for diffing

view this post on Zulip Janno (Oct 09 2020 at 10:34):

I think I was just too careless.. "big thing at the end of the term that follows a :? must be the type of the whole thing!"

view this post on Zulip Janno (Oct 09 2020 at 10:35):

I suppose I am not very good a counting parentheses :D

view this post on Zulip Janno (Oct 09 2020 at 14:35):

The casts are gone and the proof term is now checked as fast as it should be! :) Thanks so much for everyone's help!


Last updated: Oct 16 2021 at 03:02 UTC