Stream: Coq devs & plugin devs

Topic: Change of case representation


view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:10):

I am opening a topic here for the discussion of https://github.com/coq/coq/pull/13563.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:11):

This is also a call for help to understand the failures in the CI.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:12):

Elpi and Mtac2 seem to break the case invariants, because merely porting their code using the expand / contract wrappers doesn't pass their tests.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:12):

I'll probably need a bit of support from @Enrico Tassi and @Janno thus.

view this post on Zulip Janno (Dec 11 2020 at 15:13):

It is possible that our handling of matches is.. suspect.

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:13):

For elpi we need to change the HOAS...

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:13):

For Mtac2 I get

File "./tests/bugs.v", line 18, characters 10-37:
Error: decompose_lam_n_decls: not enough abstractions

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:14):

Suspicious at best.

view this post on Zulip Janno (Dec 11 2020 at 15:14):

I think we rely on there being a certain number of lambdas in every case branch.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:14):

Re elpi, it's not necessary to change the representation, it depends on what you want to expose to the user.

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:14):

most of the elpi code builds a match via a function call, so it's easy to port.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:14):

Ltac2 doesn't change the representation (yet) for instance.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:15):

Then, there is the case of bedrock2.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:16):

Some stuff is broken because the inference doesn't behave exactly the same, which I managed to debug by side-by-side checking and fix with a trivial annotation.

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:16):

I think I'd prefer to expose the new match in elpi

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:16):

But, suddenly, a proof super far away into the dev is broken because "something".

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:16):

Merely compiling until there is putting my laptop on its knees.

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:17):

buy a new one ;-)

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:17):

What about "saving the planet"?

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:17):

from what exactly...

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:17):

from academics!

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:17):

From me detonating a nuclear weapon when I start ragequitting the debug.

view this post on Zulip Enrico Tassi (Dec 11 2020 at 15:18):

I don't have time now, but I can look at it next week

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:18):

Thanks.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:18):

The good thing about bedrock2 is that I am discovering a festival of slowness issues.

view this post on Zulip Janno (Dec 11 2020 at 15:29):

I am afraid you have reached the evil parts of the Mtac2 source code.. excerpt from the backtrace:

Called from file "src/run.ml", line 666, characters 40-346

view this post on Zulip Janno (Dec 11 2020 at 15:36):

It seems we are creating evars for branches whose type is the correct function type (i.e. taking the constructor's arguments) but we don't create lambdas to take these arguments. I don't suppose that is a valid way of going about it in the new representation, is it?

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 15:41):

Nope, you have to η-expand explicitly.

view this post on Zulip Janno (Dec 11 2020 at 15:42):

Too bad :(

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 16:28):

There are helper functions in evarutil to refine product-typed evars to lambdas, I guess Pierre-Marie can provide an even better help to expand n products/let-ins

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 16:28):

No problem in Equations?

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

Now that you're asking for it...

File "./fin.v", line 315, characters 0-42:
Error: decompose_lam_n_decls: not enough abstractions

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

https://gitlab.com/coq/coq/-/jobs/905684401

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

bedrock2 is driving me crazy in the meantime.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

I haven't even reached the point where it breaks.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:35):

There is so much delirium until there that I have to stop on every nonsense I witnessed on the path.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:35):

I have seen things beyond the veil of reality.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:35):

Like, why does Tacinterp.interp_evaluable calls externalization????

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:39):

Ouch. Error printing.

view this post on Zulip Gaëtan Gilbert (Dec 11 2020 at 16:44):

where's that happening?

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:44):

Taccoerce.error_ltac_variable

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:44):

I'll write a patch.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:44):

I have a list of 10 items or so that Kami hits right where it hurts.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:46):

Regarding error printing, I know that @Emilio Jesús Gallego Arias has a bug opened somewhere but I don't find it.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:47):

There may be even several @Pierre-Marie Pédrot , what is worrying you exactly?

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:47):

What is worrying me? Well, that we have a tactic invocation that passes 50% of its time in term printing.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:48):

Not to mention that the printed result is never displayed.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:49):

Bah that's nothing, I just hacked make so we have hybrid dune / make builds :p That's _scary_

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:49):

Let me have a look

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

Yup, we want an exception here,

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Yeah, I'm writing the PR.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

indeed there is an issue to deprecate user_err

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

pity we didn't discuss about it in the CUDW

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Should we register the handler in Taccoerce or somewhere else?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

but there's even a PR

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Is there?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

Proof of concetps

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

actually stuck on the design for errors that need env

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

but doable I think

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

let me grab it

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:51):

Store it into the error like everybody does?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

https://github.com/coq/coq/pull/12602

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

You'd like to have a bit of generic interface

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

but yeah it is doable, would have been a nice chat to finish it in a physical CUDW

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:52):

I don't really see the point if we already have CErrors.register_handler.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:52):

but I spend all my time figthing with build systems...

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:52):

What's the problem with that function?

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:52):

I mean, we can use it in the meantime and port it to whatever richer infrastructure later on.

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:53):

It's just a matter of grepping.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:53):

Sure, but I'd prefer to have the thing a bit more encapsulated

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:54):

No problem in going ahead now

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:54):

But before removing all user_err, I wanted to have a bit of nicer API

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:54):

as not to do the work twice

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:55):

I have been looking at best practices for this kind of stuff upstream

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:55):

actually if we could do printing a bit differently that would be amazing, pity we can't rebind the syntax used in Format yet

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:56):

Regarding where to register the handler, hopefully we can introduce a bit better plugin setup, but that requires to have findlib first, which requires to have dune first, which requires a black mass akelarre on the day of 21-12-2112

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:56):

Can't we? The GADT has been around for a long time already.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:56):

Last time I looked we were missing something

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:57):

we -> it was

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:57):

I even had a POC patch at some point.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:57):

Oh please open an issue / PR if you made it work

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:58):

If I find this patch. I've an ocean of random branches which is not searchable...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:58):

There is a trick that actually displays all the commits that are in your branches but not for example in master

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:58):

it helps sometimes [script is in StackOverflow]

view this post on Zulip Pierre-Marie Pédrot (Dec 11 2020 at 16:58):

Just today I was looking for stuff around reduce_to_quantified_ind I knew I already wrote, to no avail.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:59):

once you get the commits, you can easily grep them

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 16:59):

it almost works for me

view this post on Zulip Janno (Dec 11 2020 at 17:07):

Okay, I've played around with the changes that are necessary in Mtac2 and it's pretty ugly. We were abusing the fact that we could get away with not introducing the necessary lambdas. And all our examples/tests rely on this to get subgoals from our destruct tactic in which the constructor's arguments have not been introduced yet.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:09):

By the way @Pierre-Marie Pédrot , something I tried when I removed linkall was to enforce more static deps

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:09):

For example, with dune is very easy to forbid access to printing

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:09):

etc...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

that could be worth exploring, even if requires a bit of refactroing

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

but ideally the error printing registration could be actually open on the printers

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

I dunno, there are many possibilities

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

but if you play a bit with the components we have today you can do better invariants

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

use of Dune already prevented sneaking zartih in the kernel

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2020 at 17:11):

and while not perfect you can do interesting stuff [like using a library but hiding the transitive dependencies]

view this post on Zulip Pierre-Marie Pédrot (Dec 14 2020 at 11:11):

Any idea why VST has wildly changing compilation times? e.g. https://gitlab.com/coq/coq/-/jobs/907343321 (134 min) vs https://gitlab.com/coq/coq/-/jobs/907220359 (> 180 min, timeout)

view this post on Zulip Pierre-Marie Pédrot (Dec 14 2020 at 11:12):

I have changed essentially nothing between the two runs, except maybe for the turning of submatch into a tailrec function.

view this post on Zulip Enrico Tassi (Dec 14 2020 at 11:25):

One is pyrolise and the othe one is a shared runner with 4G ram

view this post on Zulip Pierre-Marie Pédrot (Dec 14 2020 at 11:38):

Aha.

view this post on Zulip Beta Ziliani (Dec 14 2020 at 18:38):

Janno said:

Okay, I've played around with the changes that are necessary in Mtac2 and it's pretty ugly. We were abusing the fact that we could get away with not introducing the necessary lambdas. And all our examples/tests rely on this to get subgoals from our destruct tactic in which the constructor's arguments have not been introduced yet.

Quick update, we just had a chat with @Janno and the fix is the eta-expansion that was proposed before.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 12:27):

I am getting weird errors when trying to compile VST with this branch, see e.g. https://gitlab.com/coq/coq/-/jobs/912196799

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 12:27):

it looks like a problem with perennial, but the latter compiles fine on master ?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 12:28):

[NOTE] No package definition found for coq-perennial.dev: please complete the template
Error opening terminal: unknown.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:07):

Anybody knows how to debug bedrock2? @Samuel Gruetter maybe?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:07):

Merely getting to the point of the failure is a hell.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:08):

My browser tabs keep crashing because Coq eats up my RAM.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:09):

I don't even want to imagine if I have to tweak Coq code and recompile everything.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:14):

@Pierre-Marie Pédrot can we fix a call for thursday or friday for Elpi? I have a few questions before I fix the HOAS

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:15):

Fine.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:16):

Assuming I didn't throw my laptop through the window in the meantime.

view this post on Zulip Samuel Gruetter (Dec 15 2020 at 14:44):

I see frustration caused by bedrock2 in this thread...
I build it regularly on my 7-years old laptop with 16GB of RAM. I think the biggest files take ~8GB but that's a very rough estimate. I remember that some time ago, on the same laptop but with an older Linux, running out of memory was a problem: If I enabled swap, it would swap out my most important UI pages and my whole system became unusably slow, and when I disabled swap, the system crashed once it hit the memory limit. At that time, using cgroups to confine Coq into a predefined amount of RAM helped. In the meantime, I enabled swap again, have a newer Linux (5.9.8 with Fedora 32), and use nice -n 10 in front of make, and somehow things have become better, I haven't run out of memory anymore for months, and don't need to use cgroups any more.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:35):

In the end, I managed to survive amongst the death of thousands of Chrome tabs and a PC that was visibly chugging with all of its might.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:35):

I even crafted a quite small test, see https://github.com/coq/coq/pull/13563#issuecomment-745404598

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:36):

Judging from the contents of the test, I should really publicly state that it's a miracle that bedrock2 goes through.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:37):

I haven't decided yet whether the change of behaviour is intended, but I am quite afraid it's really relying on dark corners of the representation of case.

view this post on Zulip Andres Erbsen (Dec 15 2020 at 16:39):

Could you explain how? I wrote this code while completely oblivious about the dark corners in question.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:41):

I suspect it's working because the change is somehow messing with the internal representation of the branches of some if.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:42):

This gets the subsequent rewrite confuse.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:43):

As a matter of fact, copy-pasting the goal after the change with Set Printing All makes the rewrite go through.

view this post on Zulip Andres Erbsen (Dec 15 2020 at 16:49):

(tinkering with it) when I put idtac G in the repeat-match, I get lines that don't say ?CONTEXT-HOLE in them even with Set Printing All.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:51):

on my branch I only get one (myP (fun w : word => if weq w (if ?CONTEXT-HOLE then Y else Y) then tt else tt))

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 16:53):

Indeed, on master the change is performing forbidden magic on the case branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:01):

@Andres Erbsen did I manage to convince you that you basically invoked nasal demons in this pattern-matching?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:01):

The if-then-else you don't see actually live in the hidden branches of the pattern matching.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:02):

this tactic has seen things it should never have seen.

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:03):

I think so; I definitely never intended to do changes whose effects wouldn't be visible

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:04):

the funny thing is that it makes the rewrite work for some reason.

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:04):

are hidden branches like the cases for left and right, the types of the bound variables, or something else?

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:04):

If I had the PR branch built, I would try replacing the rewrite with https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/rewr.v#L83-L87 as a possible solution/experiment

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:06):

Since ancient times, pattern-matching has been represented essentially as Case (x, p, br), where x is the scrutinee, p is the return clause and br the array of branches. Both p and br are implemented as plain lambdas.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:07):

For instance, if you write fst : A * B -> B, you'll get something like fun (s : A * B) => Case (s, (fun (_ : A * B) => A), [|(fun (x : A) (y : B) => x)|])

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:08):

I am not even starting to mention the problems with let-bindings sneaking in there.

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:09):

Could you expand match x return option nat with inl a => Some a | inr _ => None for my understanding?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:09):

So in this example it's likely that there is an if-then-else appearing in the types.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:09):

What's the type of x ?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:09):

sum A B ?

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:09):

nat + string

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:11):

ok, so you'll get in master case (x, (fun (_ : nat + string) => option nat), [| (fun (a : nat) => Some a); (fun (_ : string) => None) |])

view this post on Zulip Andres Erbsen (Dec 15 2020 at 17:11):

Thanks!

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:11):

Parameters are inlined and don't appear in the case, but you'll see the indices + as clause in the return type, and the arguments in the branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:12):

the new representation essentially drops the types from this representation.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:12):

Also, in master nothing prevents people from wreaking havoc with the η-expansion, so that you can get weird shapes where you know that they are convertible to some lambda, but not syntactically equal to it.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:14):

There are fun performance bugs where there is a simpl that doesn't change anything even with Set Printing All, but makes the time explode because the types in the branches have changed.

view this post on Zulip Janno (Dec 15 2020 at 17:14):

the new representation essentially drops the types from this representation.

I don't want to distract from the actual discussion but I was wondering about this. Should a change like that not translate into a measurable speedup for any tactic that does term traversal on terms that contain matches? Do most developments not have matches lying around in the goal?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:14):

matches in goal are rare, but there is indeed a speedup expected.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:14):

Just consider hashconsing.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:15):

Most of the code is not taking advantage of the representation right now, so we have a small speedup. Worse, we pay for the back-and-forth change of representation so some devs can be slower. But in the long run, yes, there will be a clear gain.

view this post on Zulip Janno (Dec 15 2020 at 17:15):

Cool!

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:15):

See https://github.com/coq/coq/pull/13563#issuecomment-745404598 for the current status.

view this post on Zulip Janno (Dec 15 2020 at 17:16):

I saw the benchmark results but they didn't look like a straightforward performance boost to me

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:17):

Well, a 7% speedup counts as nice to me.

view this post on Zulip Janno (Dec 15 2020 at 17:17):

Right, but then there's perennial.. :D

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:17):

Yeah, yeah. Couldn't debug it yet since it doesn't generate the timing diffs so I'll have to hack it myself.

view this post on Zulip Janno (Dec 15 2020 at 17:19):

Hehe, I wasn't complaining. I understand that you expected there to be more debugging/benchmarking work. I was just looking at the current results but you have a much better idea of what is possible.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:20):

I am genuinely surprised that we currently see a speed up at all.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:20):

Regenerating case annotations is not free, and we do it quite a lot.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:21):

I suspect that simpl has gone from catastrophic to galactic collapse in term of efficiency, for instance.

view this post on Zulip Janno (Dec 15 2020 at 17:24):

So the way that simpl finds occurrences has already been patched to no longer give the "spurious" ones?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:24):

Well, it's going to perform useless reductions in branches, that will be dropped when reconstructing the term.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:24):

So, not ideal.

view this post on Zulip Janno (Dec 15 2020 at 17:26):

Hmm.. how does it become faster, then? Something to do with the proof term? Or Is the speedup in the next tactic that will not have to deal with simpls reduced garbage in branches?

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:26):

I meant the contrary, it has probably become slower.

view this post on Zulip Janno (Dec 15 2020 at 17:27):

Oh, I misread what you wrote above.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:27):

We have to regenerate branch annotations, we still reduce in them, and then we drop the result.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:27):

I don't know how often we reduce cases in goals though. Rewriter is probably doing that.

view this post on Zulip Janno (Dec 15 2020 at 17:27):

but it is true that the next tactic gets fresh annotations which may be less reduced than they would otherwise be, right? Maybe that doesn't have a whole lot of effect on performance, though

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

Yes, that's true.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

But I think it's incomparable in terms of performances.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

Likely conversion / unification are going to be faster on average, but you might still have big terms around.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

Although it's probably not very common to have stuff that reduces a lot in branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 17:29):

The new representation exposes the parameters and those ones are reduced, so somehow you'll still get some reduced type.

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 19:21):

Ah, perennial doesn't compile anymore because the opam file was removed two days ago by @Tej Chajed

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 12:01):

OK, the plot thickens: now perennial is faster with the change of case representation. https://gitlab.com/coq/coq/-/jobs/914731905

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 13:10):

Do you understand the bug in bedrock2 in the end?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 13:13):

Not in detail, but it's clear from the example that it shouldn't succeed on master.

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 13:39):

Well, I'd like to understand that :) You think the rewrite should fail?

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 13:39):

I mean understand the example

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 13:44):

The rewrite should be a no-op.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 13:47):

The bug seems pretty involved though, because the two rewrites can't be splitted.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:15):

I am trying to minimize it further so that we get something readable in the end.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:16):

In any case, it really looks like we need an astral conjunction to observe this bug.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:37):

@Matthieu Sozeau any idea why rewrite foo, ?bar doesn't behave as rewrite foo when bar doesn't apply?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:38):

I'd suspect some evar mayhem, but I don't want to jump into the debugger yet.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:40):

In the current bug on master, removing ?bar makes the rewrite fail even if bar never matches. As a matter of fact, writing bar instead of ?bar does fail.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:55):

@Matthieu Sozeau I have posted a simpler test, I think it makes the situation clearer.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:56):

By breaking the case representation invariants, the rewrite on master is able to preserve the well-typedness of the conclusion, but this fails after the change of representation.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 15:07):

I wonder if we can break SR with that...

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 19:37):

Interesting. So you're saying that potentially the proof term built for this proof should be ill-typed?

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 19:37):

I have no idea how multi-rewrite could do that, IIRC when you have multiple lemmas they are rewritten independently

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:02):

Nah, I think it's a bug in my PR in the end.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:02):

Somehow, change should have replaced a term that appears hidden in the parameters of the match.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:03):

It didn't, not sure why, I have to dive in horrible code now

view this post on Zulip Matthieu Sozeau (Dec 16 2020 at 20:07):

At least there's not let-ins in this example :)

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:09):

it's horrible enough...

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:11):

Arg, I think I got it: it's match goal that is not finding the right subterm because it's using the old representation.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:11):

Well, more precisely it finds it but the subsequent change fails.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 20:36):

Yay, bug fixed!

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:07):

I am diving into unification issues with eager let-expansion of case branches in whd_betaiota_deltazeta_for_iota_state. If I am not back in two days, please call the police.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 12:17):

:)

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 12:18):

You can always simulate the previous behavior no? By making the let-expanded branch not depend on the "implicit" lets that are reconstructed

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:18):

Yes, but now it's breaking in other parts of VST.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 12:18):

Ha.... good luck ;)

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:49):

It looks like on master, sometimes let-bindings in branches are expanded upfront.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 13:04):

Ha. Don't you love it, sometimes :)

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:09):

so far I've only found one instance late in VST where this happens.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:09):

with a small nudge the apply goes through.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:15):

@Matthieu Sozeau while you're at it don't you want to assign https://github.com/coq/coq/pull/13628 and https://github.com/coq/coq/pull/13622 ?

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 13:15):

I'm wondering still if the idea is really reasonable. In principle the user might want to reduce a let in a branch to a specific reduct. How do we justify that we don't want to let this happen

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:15):

every second gained in these horrible compilation chains is a blessing.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:15):

@Matthieu Sozeau what case have you in mind?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:16):

most tactics also perform zeta, so we should be fine.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 13:16):

That's the problem, I've never seen this used.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 13:17):

In principle, one could always do match c with ci x (* := t *) => let x := x in ... and massage the x in the branch instead, so the new representation is equi-expressive I agree.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:17):

I am not sure I understand your use case.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:18):

The old representation was hiding let-bindings as an implementation detail.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:19):

So, I believe it should be considered as a bug if somebody ever relied on observable differences there.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 13:19):

In the old representation, the branch containted already a let (x := t) in ... in the representation, right?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:19):

Yep.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:20):

Without any way to display it.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:54):

OK, the VST slowdowns seem to be fixed by preserving let-bindings in Reductionops path for branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 13:55):

Hopefully this has not introduced other slowdowns in the process.

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

... but now bedrock2 is broken again.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 14:49):

This means that bedrock2 does changes/reductions in lets in branches / predicates and we don't preserve those, right?

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 14:50):

I'm wondering if it's not too agressive to not keep around the let bodies.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 14:50):

Even if they don't appear in the user-level syntax

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 14:50):

(yet)

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:06):

Not necessarily, there was an instance of apply in VST that was broken, and it had little to do with explicit manipulation of let bindings.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:06):

I really think that people just write stuff that works by trial and error, and if by miracle it happens to work then they're happy with that.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:06):

(You can remove Georges from this generic statement.)

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:07):

These are really corner cases of unification and tactics.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 15:57):

Actually, I'd like to know the opinion of Georges or @Enrico Tassi , @Hugo Herbelin and @Jason Gross on this one :) I am fine with handling lets in contructors / the return predicate the way proposed by the PR, I just want to make sure that we all agree it's ok and better to not let the user fiddle with those (or the "implict" abstraction types).

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 16:15):

Georges commented on the old PR.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 16:19):

I think that the bedrock2 failure hits right where it hurts.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 16:19):

It's a cbv messing with a let-in in a branch immediately followed by a rewrite that performs a pattern extraction through the old unif.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 17:49):

@Matthieu Sozeau see my small example on the PR

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 17:55):

WTH !

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 17:58):

simpl; rewrite <- k_unsigned_byte_split1 works with your PR right?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 17:59):

Yes.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 17:59):

simpl performs the delta.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:00):

The difference of behaviour is quite simple to understand actually.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:00):

With the old representation, cbv normalizes the let in the branch, which makes rewrite unification succeed

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:00):

I'm not sure I follow the example. Presumably in

 (match KamiWord_word return (forall _ : unit, BYTE) with
   | Build_word unsigned0 _ _ => unsigned0
   end XXX)

there's a let in the branch for gtu := tt but what has it got to do with anything?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:00):

The let breaks unification.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:01):

After the fix for efficiency of VST to retrieve the old behaviour, let bindings persist in blabla_for_iotastate

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:02):

so this example works only on master because it relies on let-bindings in branch being expanded away by cbv

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:02):

on my PR without the let tweaking, it works because unification is not sensitive to let-expansion in branches

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:03):

on my PR with the let tweaking, it breaks because there are lets wreaking havoc with unification

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:03):

So essentially this example works on master by mere chance

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:04):

given that without the tweak VST takes 3 times as much time to compile, I don't think we can afford to not do it this way

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:04):

But the let gtu := tt in ... has no relation to the rewrite no?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:04):

wdym? It breaks pattern recognition

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:04):

rewrite relies on unification to match stuff

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:06):

But here clearly the left-hand-side that is matched is the whole match .. end XXX term, so how come it doesn't unify even with the tweaked version?

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:08):

For this subterm to match, I would think that the unification is just reducing the term here, and that it includes zeta

view this post on Zulip Jason Gross (Dec 18 2020 at 18:12):

My inclination would be to move away from pervasive eager inlining of let binders, and so to avoid inlining them eagerly in branches of match when possible.

view this post on Zulip Jason Gross (Dec 18 2020 at 18:14):

But indeed after cbv let bound variables in branches should not be referenced. (If they are still present but unreferenced that seems fine.)

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:22):

@Matthieu Sozeau unification calls whd_betaiota_deltazeta_for_iota_state so you're out of luck

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:23):

@Jason Gross in my PR cbv behaves as per your spec (i.e. let expanded but variables still in the context)

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:26):

I'm sorry but why? Even if the match reduces to let gtu := tt in @CAST 8 XXX I would expect it to unify with @CAST 8 XXX.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:27):

or @CAST ?ev[] XXX as the evar does not depend on the let

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:29):

I don't know, you're the expert. Please tell me what's expected here...

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:29):

As highlighted in the PR comments, there is a delta step involved.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:29):

Doing it by hand makes the example go through.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:30):

I mean that this could be considered a bug of setoid_rewrite if it's not able to reduce the let.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:30):

But that's a zeta not a delta step

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

Not only setoid rewrite, apply has the same quirk.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

No no, there is a delta in KamiWord_word.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

You need to unfold that definition for the case to reduce.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:30):

To unfold KamiWord you mean

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:31):

Yes.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:31):

Sure, is it the step that is failing now?

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:31):

Define what you call step, but indeed this delta is necessary to break the example, so I'd call it failing.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

for_iota doesn't reduce there

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

which is the whole point of the tweak somehow.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

(gtg but we can discuss at some later time)

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:34):

Ok. setoid_rewrite does use delta reduction to unify the left-hand size, so I didn't see how it could come from there

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:35):

Ok. We'll get there :)

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:37):

setoid_rewrite 's delta reduction can be configured using the rewrite HintDb. Which by default is:

Discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: all
Cut: emp
For any goal ->

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:37):

So full delta on constants is used to unify the lhs of the lemma

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 18:48):

I guess I see your problem, if a let appears at the head of the branch, we might be hitting an incompleteness bug of unification. Maybe it can't handle (let _ := foo in f x) y = f x y

view this post on Zulip Pierre-Marie Pédrot (Dec 19 2020 at 12:45):

@Matthieu Sozeau what's the best course of action? Should I wait for the unification bug to be solved, or simply fix the one failing line in bedrock2 and carry on?

view this post on Zulip Matthieu Sozeau (Dec 24 2020 at 17:25):

I think you can carry on

view this post on Zulip Pierre-Marie Pédrot (Dec 24 2020 at 17:44):

Will do.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 11:28):

Done, with a backwards compatible fix.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 11:33):

So now the ball is essentially in the court of Elpi, Mtac2 and Equations devs.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 16:36):

@Enrico Tassi I've made some progress in the Elpi overlay, now it seems that let-bindings in branches are wreaking havoc.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 16:37):

I get an error on the zeta inductive type for derive and other similar problems

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 16:38):

where conspicuously

Inductive zeta (Sender : Type) (Receiver : Type := Sender) : Type :=
    Envelope : forall a : Sender,
               let ReplyTo := a in Sender -> zeta Sender

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 17:04):

I suspect it's a bug in the logic program itself since it seems that by the time Coq receives the branches of the corresponding case, the let bindings are nowhere to be found. I can't be sure though since my elpi understanding is quite limited.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 17:05):

Either we fix that program, or I can hack a workaround in the reification step where dummy let-bindings can be reconstructed on the fly.

view this post on Zulip Enrico Tassi (Dec 26 2020 at 17:40):

I can look into that next week, but I'm a bit lost. The code probably generates a branch with 2 lambdas, how can it be wrong? In plain Coq, I can write a match branch which bound only 2 vars no?

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 20:12):

The let-bindings need to be part of the branch, it's an invariant of the representation.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 20:19):

Also, even through the user-facing API the pretyper adds dummy let-bindings in all match branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 26 2020 at 20:21):

So, in the case of zeta all branches should be of the form fun (a : Sender) (ReplyTo := a) (s : Sender) => BRANCH. Elpi is breaking that invariant.

view this post on Zulip Enrico Tassi (Dec 26 2020 at 21:47):

ok, I'll fix the code: all match are built via an API, it should be enough to patch it.

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2020 at 13:18):

@Matthieu Sozeau I think I managed to fix equations, at least make ci goes through.

view this post on Zulip Enrico Tassi (Dec 27 2020 at 15:43):

I fixed coq-elpi. Question: is there an invariant about "no lets" in the (used to be) return type? Eg, in the nasty zeta test, I was generating let dummy := .. in fun i : zeta A => something and that caused an anomaly. Note that Inductive zeta A (B := A) := ... has 1 parameter, and I was keeping the remainder of the arity for the return type (including the let).

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2020 at 15:45):

Let bindings that appear in an inductive signature, be it the arity or the constructor types, must appear in the corresponding term from the case node.

view this post on Zulip Enrico Tassi (Dec 27 2020 at 15:45):

Similarly a head let in the branches was also causing an exception

view this post on Zulip Enrico Tassi (Dec 27 2020 at 15:46):

The type of the inductive is forall A, let B := A in Type

view this post on Zulip Enrico Tassi (Dec 27 2020 at 15:54):

I was generating an out type let B := A in fun i : zeta Z => bool (anomaly) and a branch let B := A in ... (anomaly).

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2020 at 16:04):

Where do parameters stop?

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2020 at 16:04):

Parameters don't bind so they shouldn't appear in the case node (apart from the dedicated parameter array, which does not contain the let bindings)

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:04):

Eh eh, it's Coq that decides. And it says 1.

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:05):

is it 1 "forall" and 0 "lets"?

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:05):

is it 1 "forall" and all following lets?

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:05):

you tell me ;-)

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:07):

Here the beast:

Inductive zeta Sender (Receiver := Sender) := Envelope (a : Sender) (ReplyTo := a) (c : Receiver).

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:09):

BTW, I was just asking. I did not know one could have non-z-normal oty or branch prefixes. The anomalies made me think that Receiver is not to appear in the oty nor in the branches (makes sense).

view this post on Zulip Enrico Tassi (Dec 27 2020 at 16:10):

And I go trough the backward compat code, FYI. anyway, I did push the commits.

view this post on Zulip Pierre-Marie Pédrot (Dec 27 2020 at 17:25):

Indeed, the Receiver variable is a parameter so it appears neither in the return clause nor in the branches.

view this post on Zulip Pierre-Marie Pédrot (Dec 30 2020 at 16:14):

@Matthieu Sozeau now I am having DeBruijn delusions about let-binders in parameters

view this post on Zulip Pierre-Marie Pédrot (Dec 30 2020 at 16:15):

I started wondering whether the non-let binding part of the parameter instance is enough to reconstruct the part of the involved contexts in return clauses and branches that is not part of parameters

view this post on Zulip Pierre-Marie Pédrot (Dec 30 2020 at 16:16):

Also there are probably subtle bugs in the current implementation because inductive types can be referred by let bindings in parameters but AFAIK it's not possible to use this from userland.

view this post on Zulip Pierre-Marie Pédrot (Dec 30 2020 at 16:17):

My brain is melting.

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2020 at 14:28):

OK, bug (mostly) fixed and Mtac2 overlay written, so this is in a quite good shape.

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2020 at 14:29):

@Janno I've hacked the Mtac2 reification by eta-expanding case branches on sight. It's probably not super faithful and should be handled in a cleaner way, but the set of tests seems to be fine.

view this post on Zulip Pierre-Marie Pédrot (Jan 01 2021 at 18:08):

It's official: this PR is now ready. Time for a roaring tsunami of pouces bleus.

view this post on Zulip Pierre-Marie Pédrot (Jan 01 2021 at 18:08):

https://github.com/coq/coq/pull/13563

view this post on Zulip Janno (Jan 04 2021 at 09:45):

@Pierre-Marie Pédrot sorry for not responding earlier. I took some time off and thought "surely I'll look at my computer at least once" but that didn't work out. Thanks for writing the MR. I have a a half-finished branch that fixes the root cause in Mtac2's destruct tactics. But I'll need some more time to finish that so I propose we merge your overlay when the coq MR is ready, then merge my branch when that is finished, and then undo the overlay afterwards. That should be the best of both worlds: your MR is not blocked and I (eventually) get the clean solution to this problem.

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:08):

@Gaëtan Gilbert Actually I don't think we should check that relevances match in expansion.

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:08):

this defeats the whole point of having the kernel decide to set them correctly when tactics silently ignore them

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:10):

we should fix them in typeops I guess

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:10):

they are fixed by expansion AFAIU

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:10):

we expand them using the data provided by the case node, at that point they might be wrong

view this post on Zulip Enrico Tassi (Jan 04 2021 at 12:11):

Is this business of fixing wrong relevance marks supposed to stay like this, or it is a temporary hack?

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

I really hope it'll go away

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

but then we type-check the expanded form, resetting the expected annotations

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

when we deconstruct it again we're fine

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:12):

so I guess that we should fix this when removing the expansion phase in Typeops

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:12):

when the relevance marks are wrong on the case data but nowhere else we return the original term

        let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:13):

also we're not running the off-by-default warning

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:13):

I think this is dead code now

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:13):

because at least p will always be expanded away

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:13):

??

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:14):

It can never be the case that p is left untouched by expansion

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:14):

that's wrong

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:14):

and I don't understand the "wrong on case data part"

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:14):

p is the result of expansion

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:15):

(If you have a few minutes we can make a visio)

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:15):

and I don't understand the "wrong on case data part"

ie not in subterms

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:15):

sure make a visio room

view this post on Zulip Pierre-Marie Pédrot (Jan 04 2021 at 12:16):

https://rdv4.rendez-vous.renater.fr/e2mpv-7to1n-0jnmz

view this post on Zulip Gaëtan Gilbert (Jan 04 2021 at 12:16):

oh right p is the result of expansion so if the relevance was wrong it will be changed by execute

view this post on Zulip Matthieu Sozeau (Jan 06 2021 at 11:49):

Pierre-Marie Pédrot said:

Also there are probably subtle bugs in the current implementation because inductive types can be referred by let bindings in parameters but AFAIK it's not possible to use this from userland.

No, typecheck inductive properly ensure that the parameter context is type-correct in the global environment and hence closed. At least that's what I read in the code, and it's quite essential in the MetaCoq formalization.

view this post on Zulip Pierre-Marie Pédrot (Jan 18 2021 at 14:27):

@Hugo Herbelin if you have a bit of time, could you try to get rid of the dummy β-cut in destruct? It's probably quite involved, but it'd be nice to get rid of this observable change before 8.14.

view this post on Zulip Hugo Herbelin (Jan 18 2021 at 14:34):

January is quite busy for me. Don't hesitate to ping me back in a few weeks.

view this post on Zulip Matthieu Sozeau (Jan 18 2021 at 17:21):

@Pierre-Marie Pédrot it's only in the proof terms right?

view this post on Zulip Pierre-Marie Pédrot (Jan 18 2021 at 17:23):

yep

view this post on Zulip Pierre-Marie Pédrot (Jan 18 2021 at 17:24):

it's a minor issue but if we can avoid changing the semantics of destruct between releases, even if only in the generated proof-term, it'd be better

view this post on Zulip Pierre-Marie Pédrot (Jan 18 2021 at 17:24):

the fact that the CI didn't reveal any issue with that change is comforting though


Last updated: Oct 16 2021 at 02:03 UTC