I am opening a topic here for the discussion of https://github.com/coq/coq/pull/13563.
This is also a call for help to understand the failures in the CI.
Elpi and Mtac2 seem to break the case invariants, because merely porting their code using the expand / contract wrappers doesn't pass their tests.
I'll probably need a bit of support from @Enrico Tassi and @Janno thus.
It is possible that our handling of matches is.. suspect.
For elpi we need to change the HOAS...
For Mtac2 I get
File "./tests/bugs.v", line 18, characters 10-37:
Error: decompose_lam_n_decls: not enough abstractions
Suspicious at best.
I think we rely on there being a certain number of lambdas in every case branch.
Re elpi, it's not necessary to change the representation, it depends on what you want to expose to the user.
most of the elpi code builds a match via a function call, so it's easy to port.
Ltac2 doesn't change the representation (yet) for instance.
Then, there is the case of bedrock2.
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.
I think I'd prefer to expose the new match in elpi
But, suddenly, a proof super far away into the dev is broken because "something".
Merely compiling until there is putting my laptop on its knees.
buy a new one ;-)
What about "saving the planet"?
from what exactly...
from academics!
From me detonating a nuclear weapon when I start ragequitting the debug.
I don't have time now, but I can look at it next week
Thanks.
The good thing about bedrock2 is that I am discovering a festival of slowness issues.
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
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?
Nope, you have to η-expand explicitly.
Too bad :(
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
No problem in Equations?
Now that you're asking for it...
File "./fin.v", line 315, characters 0-42:
Error: decompose_lam_n_decls: not enough abstractions
https://gitlab.com/coq/coq/-/jobs/905684401
bedrock2 is driving me crazy in the meantime.
I haven't even reached the point where it breaks.
There is so much delirium until there that I have to stop on every nonsense I witnessed on the path.
I have seen things beyond the veil of reality.
Like, why does Tacinterp.interp_evaluable calls externalization????
Ouch. Error printing.
where's that happening?
Taccoerce.error_ltac_variable
I'll write a patch.
I have a list of 10 items or so that Kami hits right where it hurts.
Regarding error printing, I know that @Emilio Jesús Gallego Arias has a bug opened somewhere but I don't find it.
There may be even several @Pierre-Marie Pédrot , what is worrying you exactly?
What is worrying me? Well, that we have a tactic invocation that passes 50% of its time in term printing.
Not to mention that the printed result is never displayed.
Bah that's nothing, I just hacked make so we have hybrid dune / make builds :p That's _scary_
Let me have a look
Yup, we want an exception here,
Yeah, I'm writing the PR.
indeed there is an issue to deprecate user_err
pity we didn't discuss about it in the CUDW
Should we register the handler in Taccoerce or somewhere else?
but there's even a PR
Is there?
Proof of concetps
actually stuck on the design for errors that need env
but doable I think
let me grab it
Store it into the error like everybody does?
https://github.com/coq/coq/pull/12602
You'd like to have a bit of generic interface
but yeah it is doable, would have been a nice chat to finish it in a physical CUDW
I don't really see the point if we already have CErrors.register_handler.
but I spend all my time figthing with build systems...
What's the problem with that function?
I mean, we can use it in the meantime and port it to whatever richer infrastructure later on.
It's just a matter of grepping.
Sure, but I'd prefer to have the thing a bit more encapsulated
No problem in going ahead now
But before removing all user_err
, I wanted to have a bit of nicer API
as not to do the work twice
I have been looking at best practices for this kind of stuff upstream
actually if we could do printing a bit differently that would be amazing, pity we can't rebind the syntax used in Format
yet
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
Can't we? The GADT has been around for a long time already.
Last time I looked we were missing something
we -> it was
I even had a POC patch at some point.
Oh please open an issue / PR if you made it work
If I find this patch. I've an ocean of random branches which is not searchable...
There is a trick that actually displays all the commits that are in your branches but not for example in master
it helps sometimes [script is in StackOverflow]
Just today I was looking for stuff around reduce_to_quantified_ind I knew I already wrote, to no avail.
once you get the commits, you can easily grep them
it almost works for me
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.
By the way @Pierre-Marie Pédrot , something I tried when I removed linkall was to enforce more static deps
For example, with dune is very easy to forbid access to printing
etc...
that could be worth exploring, even if requires a bit of refactroing
but ideally the error printing registration could be actually open on the printers
I dunno, there are many possibilities
but if you play a bit with the components we have today you can do better invariants
use of Dune already prevented sneaking zartih
in the kernel
and while not perfect you can do interesting stuff [like using a library but hiding the transitive dependencies]
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)
I have changed essentially nothing between the two runs, except maybe for the turning of submatch into a tailrec function.
One is pyrolise and the othe one is a shared runner with 4G ram
Aha.
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.
I am getting weird errors when trying to compile VST with this branch, see e.g. https://gitlab.com/coq/coq/-/jobs/912196799
it looks like a problem with perennial, but the latter compiles fine on master ?
[NOTE] No package definition found for coq-perennial.dev: please complete the template
Error opening terminal: unknown.
Anybody knows how to debug bedrock2? @Samuel Gruetter maybe?
Merely getting to the point of the failure is a hell.
My browser tabs keep crashing because Coq eats up my RAM.
I don't even want to imagine if I have to tweak Coq code and recompile everything.
@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
Fine.
Assuming I didn't throw my laptop through the window in the meantime.
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.
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.
I even crafted a quite small test, see https://github.com/coq/coq/pull/13563#issuecomment-745404598
Judging from the contents of the test, I should really publicly state that it's a miracle that bedrock2 goes through.
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.
Could you explain how? I wrote this code while completely oblivious about the dark corners in question.
I suspect it's working because the change is somehow messing with the internal representation of the branches of some if.
This gets the subsequent rewrite confuse.
As a matter of fact, copy-pasting the goal after the change with Set Printing All makes the rewrite go through.
(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
.
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))
Indeed, on master the change is performing forbidden magic on the case branches.
@Andres Erbsen did I manage to convince you that you basically invoked nasal demons in this pattern-matching?
The if-then-else you don't see actually live in the hidden branches of the pattern matching.
this tactic has seen things it should never have seen.
I think so; I definitely never intended to do change
s whose effects wouldn't be visible
the funny thing is that it makes the rewrite work for some reason.
are hidden branches like the cases for left and right, the types of the bound variables, or something else?
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
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.
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)|])
I am not even starting to mention the problems with let-bindings sneaking in there.
Could you expand match x return option nat with inl a => Some a | inr _ => None
for my understanding?
So in this example it's likely that there is an if-then-else appearing in the types.
What's the type of x ?
sum A B ?
nat + string
ok, so you'll get in master case (x, (fun (_ : nat + string) => option nat), [| (fun (a : nat) => Some a); (fun (_ : string) => None) |])
Thanks!
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.
the new representation essentially drops the types from this representation.
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.
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.
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 match
es? Do most developments not have match
es lying around in the goal?
matches in goal are rare, but there is indeed a speedup expected.
Just consider hashconsing.
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.
Cool!
See https://github.com/coq/coq/pull/13563#issuecomment-745404598 for the current status.
I saw the benchmark results but they didn't look like a straightforward performance boost to me
Well, a 7% speedup counts as nice to me.
Right, but then there's perennial.. :D
Yeah, yeah. Couldn't debug it yet since it doesn't generate the timing diffs so I'll have to hack it myself.
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.
I am genuinely surprised that we currently see a speed up at all.
Regenerating case annotations is not free, and we do it quite a lot.
I suspect that simpl has gone from catastrophic to galactic collapse in term of efficiency, for instance.
So the way that simpl
finds occurrences has already been patched to no longer give the "spurious" ones?
Well, it's going to perform useless reductions in branches, that will be dropped when reconstructing the term.
So, not ideal.
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 simpl
s reduced garbage in branches?
I meant the contrary, it has probably become slower.
Oh, I misread what you wrote above.
We have to regenerate branch annotations, we still reduce in them, and then we drop the result.
I don't know how often we reduce cases in goals though. Rewriter is probably doing that.
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
Yes, that's true.
But I think it's incomparable in terms of performances.
Likely conversion / unification are going to be faster on average, but you might still have big terms around.
Although it's probably not very common to have stuff that reduces a lot in branches.
The new representation exposes the parameters and those ones are reduced, so somehow you'll still get some reduced type.
Ah, perennial doesn't compile anymore because the opam file was removed two days ago by @Tej Chajed
OK, the plot thickens: now perennial is faster with the change of case representation. https://gitlab.com/coq/coq/-/jobs/914731905
Do you understand the bug in bedrock2 in the end?
Not in detail, but it's clear from the example that it shouldn't succeed on master.
Well, I'd like to understand that :) You think the rewrite should fail?
I mean understand the example
The rewrite should be a no-op.
The bug seems pretty involved though, because the two rewrites can't be splitted.
I am trying to minimize it further so that we get something readable in the end.
In any case, it really looks like we need an astral conjunction to observe this bug.
@Matthieu Sozeau any idea why rewrite foo, ?bar
doesn't behave as rewrite foo
when bar doesn't apply?
I'd suspect some evar mayhem, but I don't want to jump into the debugger yet.
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.
@Matthieu Sozeau I have posted a simpler test, I think it makes the situation clearer.
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.
I wonder if we can break SR with that...
Interesting. So you're saying that potentially the proof term built for this proof should be ill-typed?
I have no idea how multi-rewrite could do that, IIRC when you have multiple lemmas they are rewritten independently
Nah, I think it's a bug in my PR in the end.
Somehow, change
should have replaced a term that appears hidden in the parameters of the match.
It didn't, not sure why, I have to dive in horrible code now
At least there's not let-ins in this example :)
it's horrible enough...
Arg, I think I got it: it's match goal that is not finding the right subterm because it's using the old representation.
Well, more precisely it finds it but the subsequent change fails.
Yay, bug fixed!
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.
:)
You can always simulate the previous behavior no? By making the let-expanded branch not depend on the "implicit" lets that are reconstructed
Yes, but now it's breaking in other parts of VST.
Ha.... good luck ;)
It looks like on master, sometimes let-bindings in branches are expanded upfront.
Ha. Don't you love it, sometimes :)
so far I've only found one instance late in VST where this happens.
with a small nudge the apply goes through.
@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 ?
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
every second gained in these horrible compilation chains is a blessing.
@Matthieu Sozeau what case have you in mind?
most tactics also perform zeta, so we should be fine.
That's the problem, I've never seen this used.
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.
I am not sure I understand your use case.
The old representation was hiding let-bindings as an implementation detail.
So, I believe it should be considered as a bug if somebody ever relied on observable differences there.
In the old representation, the branch containted already a let (x := t) in ...
in the representation, right?
Yep.
Without any way to display it.
OK, the VST slowdowns seem to be fixed by preserving let-bindings in Reductionops path for branches.
Hopefully this has not introduced other slowdowns in the process.
... but now bedrock2 is broken again.
This means that bedrock2 does changes/reductions in lets in branches / predicates and we don't preserve those, right?
I'm wondering if it's not too agressive to not keep around the let bodies.
Even if they don't appear in the user-level syntax
(yet)
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.
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.
(You can remove Georges from this generic statement.)
These are really corner cases of unification and tactics.
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).
Georges commented on the old PR.
I think that the bedrock2 failure hits right where it hurts.
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.
@Matthieu Sozeau see my small example on the PR
WTH !
simpl; rewrite <- k_unsigned_byte_split1
works with your PR right?
Yes.
simpl performs the delta.
The difference of behaviour is quite simple to understand actually.
With the old representation, cbv normalizes the let in the branch, which makes rewrite unification succeed
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?
The let breaks unification.
After the fix for efficiency of VST to retrieve the old behaviour, let bindings persist in blabla_for_iotastate
so this example works only on master because it relies on let-bindings in branch being expanded away by cbv
on my PR without the let tweaking, it works because unification is not sensitive to let-expansion in branches
on my PR with the let tweaking, it breaks because there are lets wreaking havoc with unification
So essentially this example works on master by mere chance
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
But the let gtu := tt in ...
has no relation to the rewrite no?
wdym? It breaks pattern recognition
rewrite relies on unification to match stuff
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?
For this subterm to match, I would think that the unification is just reducing the term here, and that it includes zeta
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.
But indeed after cbv
let bound variables in branches should not be referenced. (If they are still present but unreferenced that seems fine.)
@Matthieu Sozeau unification calls whd_betaiota_deltazeta_for_iota_state so you're out of luck
@Jason Gross in my PR cbv behaves as per your spec (i.e. let expanded but variables still in the context)
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
.
or @CAST ?ev[] XXX
as the evar does not depend on the let
I don't know, you're the expert. Please tell me what's expected here...
As highlighted in the PR comments, there is a delta step involved.
Doing it by hand makes the example go through.
I mean that this could be considered a bug of setoid_rewrite if it's not able to reduce the let.
But that's a zeta not a delta step
Not only setoid rewrite, apply has the same quirk.
No no, there is a delta in KamiWord_word
.
You need to unfold that definition for the case to reduce.
To unfold KamiWord you mean
Yes.
Sure, is it the step that is failing now?
Define what you call step, but indeed this delta is necessary to break the example, so I'd call it failing.
for_iota doesn't reduce there
which is the whole point of the tweak somehow.
(gtg but we can discuss at some later time)
Ok. setoid_rewrite
does use delta reduction to unify the left-hand size, so I didn't see how it could come from there
Ok. We'll get there :)
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 ->
So full delta on constants is used to unify the lhs of the lemma
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
@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?
I think you can carry on
Will do.
Done, with a backwards compatible fix.
So now the ball is essentially in the court of Elpi, Mtac2 and Equations devs.
@Enrico Tassi I've made some progress in the Elpi overlay, now it seems that let-bindings in branches are wreaking havoc.
I get an error on the zeta inductive type for derive and other similar problems
where conspicuously
Inductive zeta (Sender : Type) (Receiver : Type := Sender) : Type :=
Envelope : forall a : Sender,
let ReplyTo := a in Sender -> zeta Sender
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.
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.
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?
The let-bindings need to be part of the branch, it's an invariant of the representation.
Also, even through the user-facing API the pretyper adds dummy let-bindings in all match branches.
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.
ok, I'll fix the code: all match
are built via an API, it should be enough to patch it.
@Matthieu Sozeau I think I managed to fix equations, at least make ci
goes through.
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).
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.
Similarly a head let in the branches was also causing an exception
The type of the inductive is forall A, let B := A in Type
I was generating an out type let B := A in fun i : zeta Z => bool
(anomaly) and a branch let B := A in ...
(anomaly).
Where do parameters stop?
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)
Eh eh, it's Coq that decides. And it says 1.
is it 1 "forall" and 0 "lets"?
is it 1 "forall" and all following lets?
you tell me ;-)
Here the beast:
Inductive zeta Sender (Receiver := Sender) := Envelope (a : Sender) (ReplyTo := a) (c : Receiver).
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).
And I go trough the backward compat code, FYI. anyway, I did push the commits.
Indeed, the Receiver variable is a parameter so it appears neither in the return clause nor in the branches.
@Matthieu Sozeau now I am having DeBruijn delusions about let-binders in parameters
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
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.
My brain is melting.
OK, bug (mostly) fixed and Mtac2 overlay written, so this is in a quite good shape.
@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.
It's official: this PR is now ready. Time for a roaring tsunami of pouces bleus.
https://github.com/coq/coq/pull/13563
@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.
@Gaëtan Gilbert Actually I don't think we should check that relevances match in expansion.
this defeats the whole point of having the kernel decide to set them correctly when tactics silently ignore them
we should fix them in typeops I guess
they are fixed by expansion AFAIU
we expand them using the data provided by the case node, at that point they might be wrong
Is this business of fixing wrong relevance marks supposed to stay like this, or it is a temporary hack?
I really hope it'll go away
but then we type-check the expanded form, resetting the expected annotations
when we deconstruct it again we're fine
so I guess that we should fix this when removing the expansion phase in Typeops
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
also we're not running the off-by-default warning
I think this is dead code now
because at least p
will always be expanded away
??
It can never be the case that p
is left untouched by expansion
that's wrong
and I don't understand the "wrong on case data part"
p is the result of expansion
(If you have a few minutes we can make a visio)
and I don't understand the "wrong on case data part"
ie not in subterms
sure make a visio room
https://rdv4.rendez-vous.renater.fr/e2mpv-7to1n-0jnmz
oh right p is the result of expansion so if the relevance was wrong it will be changed by execute
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.
@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.
January is quite busy for me. Don't hesitate to ping me back in a few weeks.
@Pierre-Marie Pédrot it's only in the proof terms right?
yep
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
the fact that the CI didn't reveal any issue with that change is comforting though
Last updated: Oct 13 2024 at 01:02 UTC