Stream: Coq devs & plugin devs

Topic: holidays


view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 11:44):

I will be on vacation for 2 weeks after today
I may still do some things but don't wait for me

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 19:49):

I leave you with a new inconsistency ;)

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:05):

I claim prior art on this one.

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:05):

it was breaking a test in https://github.com/coq/coq/pull/15908 but I didn't dig deeper

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:06):

(I thought let bindings were always expanded or something)

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:08):

they're not expanded in your fast path

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:10):

not in the version pushed, but with an intermediate one

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:11):

it was precisely breaking a (A : Type := Type) in the test-suite

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:11):

but well it doesn't really matter

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:11):

we know have an inconsistency to fix, yay

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:12):

I see

@ppedrot ppedrot force-pushed the template-invariant-cumul branch from 281ca0d to 9889dd5 2 days ago

281ca0d has no test suite failures
9889dd5 has the broken fast path

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:13):

Pierre-Marie Pédrot said:

but well it doesn't really matter

it matters if we have multiple related but not quite the same bugs
then if we fix one the other might survive

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:14):

we seem to have more tests for template poly than for cumulative

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:14):

we've been burned more with the former...

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:15):

so if we fix it and the PR using inferCumul for template is still broken we'll know

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:15):

I removed your fast path in the merge commit I pushed btw (it conflicted)

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:22):

there are two ways to fix the bug, either we make the section universe invariant or we recheck the variance when closing a section

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:22):

what's the more reasonable design?

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:22):

(given that you can't specify cumulativity per universe / inductive pair)

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:35):

Pierre-Marie Pédrot said:

(given that you can't specify cumulativity per universe / inductive pair)

we do though
mind_sec_variance in the mutual_inductive_body

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 20:42):

section universes are likely to be irrelevant as typically they're the universe of a parameter
so for a quick fix we may be better of rechecking

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:51):

but we have no syntax for this, I mean

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:51):

in general you can't even do that because cumulativity only makes sense for arities

view this post on Zulip Pierre-Marie Pédrot (Apr 08 2022 at 20:52):

reinferring at section closing goes against the no-inference-rule in the kernel


Last updated: Oct 13 2024 at 01:02 UTC