Stream: Coq devs & plugin devs

Topic: Change of case representation

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.

Pierre-Marie Pédrot (Dec 11 2020 at 15:11):

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

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.

Pierre-Marie Pédrot (Dec 11 2020 at 15:12):

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

Janno (Dec 11 2020 at 15:13):

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

Enrico Tassi (Dec 11 2020 at 15:13):

For elpi we need to change the HOAS...

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

Pierre-Marie Pédrot (Dec 11 2020 at 15:14):

Suspicious at best.

Janno (Dec 11 2020 at 15:14):

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

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.

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.

Pierre-Marie Pédrot (Dec 11 2020 at 15:14):

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

Pierre-Marie Pédrot (Dec 11 2020 at 15:15):

Then, there is the case of bedrock2.

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.

Enrico Tassi (Dec 11 2020 at 15:16):

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

Pierre-Marie Pédrot (Dec 11 2020 at 15:16):

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

Pierre-Marie Pédrot (Dec 11 2020 at 15:16):

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

Enrico Tassi (Dec 11 2020 at 15:17):

buy a new one ;-)

Pierre-Marie Pédrot (Dec 11 2020 at 15:17):

What about "saving the planet"?

Enrico Tassi (Dec 11 2020 at 15:17):

from what exactly...

Enrico Tassi (Dec 11 2020 at 15:17):

from academics!

Pierre-Marie Pédrot (Dec 11 2020 at 15:17):

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

Enrico Tassi (Dec 11 2020 at 15:18):

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

Pierre-Marie Pédrot (Dec 11 2020 at 15:18):

Thanks.

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.

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

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?

Pierre-Marie Pédrot (Dec 11 2020 at 15:41):

Nope, you have to η-expand explicitly.

Janno (Dec 11 2020 at 15:42):

Too bad :(

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

Matthieu Sozeau (Dec 11 2020 at 16:28):

No problem in Equations?

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

bedrock2 is driving me crazy in the meantime.

Pierre-Marie Pédrot (Dec 11 2020 at 16:34):

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

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.

Pierre-Marie Pédrot (Dec 11 2020 at 16:35):

I have seen things beyond the veil of reality.

Pierre-Marie Pédrot (Dec 11 2020 at 16:35):

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:39):

Ouch. Error printing.

Gaëtan Gilbert (Dec 11 2020 at 16:44):

where's that happening?

Pierre-Marie Pédrot (Dec 11 2020 at 16:44):

Taccoerce.error_ltac_variable

Pierre-Marie Pédrot (Dec 11 2020 at 16:44):

I'll write a patch.

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.

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.

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?

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.

Pierre-Marie Pédrot (Dec 11 2020 at 16:48):

Not to mention that the printed result is never displayed.

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_

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:49):

Let me have a look

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

Yup, we want an exception here,

Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Yeah, I'm writing the PR.

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

indeed there is an issue to deprecate user_err

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

pity we didn't discuss about it in the CUDW

Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Should we register the handler in Taccoerce or somewhere else?

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:50):

but there's even a PR

Pierre-Marie Pédrot (Dec 11 2020 at 16:50):

Is there?

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

Proof of concetps

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

actually stuck on the design for errors that need env

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

but doable I think

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

let me grab it

Pierre-Marie Pédrot (Dec 11 2020 at 16:51):

Store it into the error like everybody does?

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:51):

You'd like to have a bit of generic interface

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:52):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:52):

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:52):

What's the problem with that function?

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.

Pierre-Marie Pédrot (Dec 11 2020 at 16:53):

It's just a matter of grepping.

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:53):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:54):

No problem in going ahead now

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:54):

as not to do the work twice

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:55):

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

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

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

Pierre-Marie Pédrot (Dec 11 2020 at 16:56):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:56):

Last time I looked we were missing something

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:57):

we -> it was

Pierre-Marie Pédrot (Dec 11 2020 at 16:57):

I even had a POC patch at some point.

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:57):

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

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...

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:58):

it helps sometimes [script is in StackOverflow]

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.

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:59):

once you get the commits, you can easily grep them

Emilio Jesús Gallego Arias (Dec 11 2020 at 16:59):

it almost works for me

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.

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:09):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:09):

etc...

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

I dunno, there are many possibilities

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

Emilio Jesús Gallego Arias (Dec 11 2020 at 17:10):

use of Dune already prevented sneaking zartih in the kernel

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]

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)

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.

Enrico Tassi (Dec 14 2020 at 11:25):

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

Pierre-Marie Pédrot (Dec 14 2020 at 11:38):

Aha.

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.

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

Pierre-Marie Pédrot (Dec 15 2020 at 12:27):

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

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.

Pierre-Marie Pédrot (Dec 15 2020 at 13:07):

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

Pierre-Marie Pédrot (Dec 15 2020 at 13:07):

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

Pierre-Marie Pédrot (Dec 15 2020 at 13:08):

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

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.

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

Pierre-Marie Pédrot (Dec 15 2020 at 13:15):

Fine.

Pierre-Marie Pédrot (Dec 15 2020 at 13:16):

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

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.

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.

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

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.

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.

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.

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.

Pierre-Marie Pédrot (Dec 15 2020 at 16:42):

This gets the subsequent rewrite confuse.

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.

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.

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))

Pierre-Marie Pédrot (Dec 15 2020 at 16:53):

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

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?

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.

Pierre-Marie Pédrot (Dec 15 2020 at 17:02):

this tactic has seen things it should never have seen.

Andres Erbsen (Dec 15 2020 at 17:03):

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

Pierre-Marie Pédrot (Dec 15 2020 at 17:04):

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

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?

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

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.

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)|])

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.

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?

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.

Pierre-Marie Pédrot (Dec 15 2020 at 17:09):

What's the type of x ?

Pierre-Marie Pédrot (Dec 15 2020 at 17:09):

sum A B ?

Andres Erbsen (Dec 15 2020 at 17:09):

nat + string

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) |])

Andres Erbsen (Dec 15 2020 at 17:11):

Thanks!

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.

Pierre-Marie Pédrot (Dec 15 2020 at 17:12):

the new representation essentially drops the types from this representation.

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.

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.

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?

Pierre-Marie Pédrot (Dec 15 2020 at 17:14):

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

Pierre-Marie Pédrot (Dec 15 2020 at 17:14):

Just consider hashconsing.

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.

Janno (Dec 15 2020 at 17:15):

Cool!

Pierre-Marie Pédrot (Dec 15 2020 at 17:15):

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

Janno (Dec 15 2020 at 17:16):

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

Pierre-Marie Pédrot (Dec 15 2020 at 17:17):

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

Janno (Dec 15 2020 at 17:17):

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

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.

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.

Pierre-Marie Pédrot (Dec 15 2020 at 17:20):

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

Pierre-Marie Pédrot (Dec 15 2020 at 17:20):

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

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.

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?

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.

Pierre-Marie Pédrot (Dec 15 2020 at 17:24):

So, not ideal.

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?

Pierre-Marie Pédrot (Dec 15 2020 at 17:26):

I meant the contrary, it has probably become slower.

Janno (Dec 15 2020 at 17:27):

Oh, I misread what you wrote above.

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.

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.

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

Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

Yes, that's true.

Pierre-Marie Pédrot (Dec 15 2020 at 17:28):

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

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.

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.

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.

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

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

Matthieu Sozeau (Dec 16 2020 at 13:10):

Do you understand the bug in bedrock2 in the end?

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.

Matthieu Sozeau (Dec 16 2020 at 13:39):

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

Matthieu Sozeau (Dec 16 2020 at 13:39):

I mean understand the example

Pierre-Marie Pédrot (Dec 16 2020 at 13:44):

The rewrite should be a no-op.

Pierre-Marie Pédrot (Dec 16 2020 at 13:47):

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

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.

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.

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?

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.

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.

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.

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.

Pierre-Marie Pédrot (Dec 16 2020 at 15:07):

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

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?

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

Pierre-Marie Pédrot (Dec 16 2020 at 20:02):

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

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.

Pierre-Marie Pédrot (Dec 16 2020 at 20:03):

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

Matthieu Sozeau (Dec 16 2020 at 20:07):

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

Pierre-Marie Pédrot (Dec 16 2020 at 20:09):

it's horrible enough...

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.

Pierre-Marie Pédrot (Dec 16 2020 at 20:11):

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

Pierre-Marie Pédrot (Dec 16 2020 at 20:36):

Yay, bug fixed!

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.

Matthieu Sozeau (Dec 18 2020 at 12:17):

:)

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

Pierre-Marie Pédrot (Dec 18 2020 at 12:18):

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

Matthieu Sozeau (Dec 18 2020 at 12:18):

Ha.... good luck ;)

Pierre-Marie Pédrot (Dec 18 2020 at 12:49):

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

Matthieu Sozeau (Dec 18 2020 at 13:04):

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

Pierre-Marie Pédrot (Dec 18 2020 at 13:09):

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

Pierre-Marie Pédrot (Dec 18 2020 at 13:09):

with a small nudge the apply goes through.

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 ?

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

Pierre-Marie Pédrot (Dec 18 2020 at 13:15):

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

Pierre-Marie Pédrot (Dec 18 2020 at 13:15):

@Matthieu Sozeau what case have you in mind?

Pierre-Marie Pédrot (Dec 18 2020 at 13:16):

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

Matthieu Sozeau (Dec 18 2020 at 13:16):

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

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.

Pierre-Marie Pédrot (Dec 18 2020 at 13:17):

I am not sure I understand your use case.

Pierre-Marie Pédrot (Dec 18 2020 at 13:18):

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

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.

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?

Pierre-Marie Pédrot (Dec 18 2020 at 13:19):

Yep.

Pierre-Marie Pédrot (Dec 18 2020 at 13:20):

Without any way to display it.

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.

Pierre-Marie Pédrot (Dec 18 2020 at 13:55):

Hopefully this has not introduced other slowdowns in the process.

Pierre-Marie Pédrot (Dec 18 2020 at 14:35):

... but now bedrock2 is broken again.

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?

Matthieu Sozeau (Dec 18 2020 at 14:50):

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

Matthieu Sozeau (Dec 18 2020 at 14:50):

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

Matthieu Sozeau (Dec 18 2020 at 14:50):

(yet)

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.

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.

Pierre-Marie Pédrot (Dec 18 2020 at 15:06):

(You can remove Georges from this generic statement.)

Pierre-Marie Pédrot (Dec 18 2020 at 15:07):

These are really corner cases of unification and tactics.

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).

Pierre-Marie Pédrot (Dec 18 2020 at 16:15):

Georges commented on the old PR.

Pierre-Marie Pédrot (Dec 18 2020 at 16:19):

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

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.

Pierre-Marie Pédrot (Dec 18 2020 at 17:49):

@Matthieu Sozeau see my small example on the PR

Matthieu Sozeau (Dec 18 2020 at 17:55):

WTH !

Matthieu Sozeau (Dec 18 2020 at 17:58):

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

Pierre-Marie Pédrot (Dec 18 2020 at 17:59):

Yes.

Pierre-Marie Pédrot (Dec 18 2020 at 17:59):

simpl performs the delta.

Pierre-Marie Pédrot (Dec 18 2020 at 18:00):

The difference of behaviour is quite simple to understand actually.

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

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?

Pierre-Marie Pédrot (Dec 18 2020 at 18:00):

The let breaks unification.

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

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

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

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

Pierre-Marie Pédrot (Dec 18 2020 at 18:03):

So essentially this example works on master by mere chance

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

Matthieu Sozeau (Dec 18 2020 at 18:04):

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

Pierre-Marie Pédrot (Dec 18 2020 at 18:04):

wdym? It breaks pattern recognition

Pierre-Marie Pédrot (Dec 18 2020 at 18:04):

rewrite relies on unification to match stuff

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?

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

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.

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.)

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

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)

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.

Matthieu Sozeau (Dec 18 2020 at 18:27):

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

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...

Pierre-Marie Pédrot (Dec 18 2020 at 18:29):

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

Pierre-Marie Pédrot (Dec 18 2020 at 18:29):

Doing it by hand makes the example go through.

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.

Matthieu Sozeau (Dec 18 2020 at 18:30):

But that's a zeta not a delta step

Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

Not only setoid rewrite, apply has the same quirk.

Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

No no, there is a delta in KamiWord_word.

Pierre-Marie Pédrot (Dec 18 2020 at 18:30):

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

Matthieu Sozeau (Dec 18 2020 at 18:30):

To unfold KamiWord you mean

Pierre-Marie Pédrot (Dec 18 2020 at 18:31):

Yes.

Matthieu Sozeau (Dec 18 2020 at 18:31):

Sure, is it the step that is failing now?

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.

Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

for_iota doesn't reduce there

Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

which is the whole point of the tweak somehow.

Pierre-Marie Pédrot (Dec 18 2020 at 18:32):

(gtg but we can discuss at some later time)

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

Matthieu Sozeau (Dec 18 2020 at 18:35):

Ok. We'll get there :)

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 ->

Matthieu Sozeau (Dec 18 2020 at 18:37):

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

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

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?

Matthieu Sozeau (Dec 24 2020 at 17:25):

I think you can carry on

Pierre-Marie Pédrot (Dec 24 2020 at 17:44):

Will do.

Pierre-Marie Pédrot (Dec 26 2020 at 11:28):

Done, with a backwards compatible fix.

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.

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.

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

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

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.

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.

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?

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.

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.

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.

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.

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.

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).

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.

Enrico Tassi (Dec 27 2020 at 15:45):

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

Enrico Tassi (Dec 27 2020 at 15:46):

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

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).

Pierre-Marie Pédrot (Dec 27 2020 at 16:04):

Where do parameters stop?

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)

Enrico Tassi (Dec 27 2020 at 16:04):

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

Enrico Tassi (Dec 27 2020 at 16:05):

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

Enrico Tassi (Dec 27 2020 at 16:05):

is it 1 "forall" and all following lets?

Enrico Tassi (Dec 27 2020 at 16:05):

you tell me ;-)

Enrico Tassi (Dec 27 2020 at 16:07):

Here the beast:

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

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).

Enrico Tassi (Dec 27 2020 at 16:10):

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

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.

Pierre-Marie Pédrot (Dec 30 2020 at 16:14):

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

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

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.

Pierre-Marie Pédrot (Dec 30 2020 at 16:17):

My brain is melting.

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.

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.

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.

Pierre-Marie Pédrot (Jan 01 2021 at 18:08):

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

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.

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.

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

Gaëtan Gilbert (Jan 04 2021 at 12:10):

we should fix them in typeops I guess

Pierre-Marie Pédrot (Jan 04 2021 at 12:10):

they are fixed by expansion AFAIU

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

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?

Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

I really hope it'll go away

Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

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

Pierre-Marie Pédrot (Jan 04 2021 at 12:11):

when we deconstruct it again we're fine

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

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

Gaëtan Gilbert (Jan 04 2021 at 12:13):

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

Pierre-Marie Pédrot (Jan 04 2021 at 12:13):

I think this is dead code now

Pierre-Marie Pédrot (Jan 04 2021 at 12:13):

because at least p will always be expanded away

Gaëtan Gilbert (Jan 04 2021 at 12:13):

??

Pierre-Marie Pédrot (Jan 04 2021 at 12:14):

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

Gaëtan Gilbert (Jan 04 2021 at 12:14):

that's wrong

Pierre-Marie Pédrot (Jan 04 2021 at 12:14):

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

Gaëtan Gilbert (Jan 04 2021 at 12:14):

p is the result of expansion

Pierre-Marie Pédrot (Jan 04 2021 at 12:15):

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

Gaëtan Gilbert (Jan 04 2021 at 12:15):

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

ie not in subterms

Gaëtan Gilbert (Jan 04 2021 at 12:15):

sure make a visio room

Pierre-Marie Pédrot (Jan 04 2021 at 12:16):

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

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

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.

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.

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.

Matthieu Sozeau (Jan 18 2021 at 17:21):

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

Pierre-Marie Pédrot (Jan 18 2021 at 17:23):

yep

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

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: Apr 19 2024 at 02:02 UTC