isClass? panic!

Stream: lean4

[Henrik Böving]

I'm currently seeing a panic in the mathlib4_docs CI that looks like this:

stderr:
PANIC at DocGen4.Process.InstanceInfo.ofDefinitionVal DocGen4.Process.InstanceInfo:31:41: unreachable code has been reached
backtrace:
./lake-packages/doc-gen4/build/bin/doc-gen4(lean_panic_fn+0x9e)[0x564ad37b71ce]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_DocGen4_Process_InstanceInfo_ofDefinitionVal+0x5c4)[0x564ad0beb694]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_DocGen4_Process_DocInfo_ofConstant___lambda__1+0x1b6a)[0x564ad0bf673a]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_DocGen4_Process_DocInfo_ofConstant+0x155)[0x564ad0bf6ae5]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_List_forIn_loop___at_DocGen4_Process_process___spec__14___lambda__1+0xa00)[0x564ad0bfbbc0]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_List_forIn_loop___at_DocGen4_Process_process___spec__14+0x3d0)[0x564ad0bfecf0]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_DocGen4_Process_process+0x4ee)[0x564ad0c0058e]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_DocGen4_load+0x3a7)[0x564ad0c04427]
./lake-packages/doc-gen4/build/bin/doc-gen4(l_runSingleCmd+0x166)[0x564ad0bcab66]

It occurs after updating doc-gen from leanprover/lean4:v4.0.0 to leanprover/lean4:v4.1.0-rc1

The confusing thing about this is that it hits this unreachable: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/InstanceInfo.lean#L31 and as the doc-string of isClass? says:

/--
  `isClass? type` return `some ClsName` if `type` is an instance of the class `ClsName`.
  Example:
  ```
  #eval do
    let x ← mkAppM ``Inhabited #[mkConst ``Nat]
    IO.println (← isClass? x)
    -- (some Inhabited)
  ```
-/

So this should always return some if v is an instance and if you go up to the call site here: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process/DocInfo.lean#L161 you will see it only gets called if isInstance is true. So I claim that there is no reason this unreachable! should ever get hit and this is a regression.

I'll add a panic mentioning the name of the instance to create an MWE, just putting this out here in case someone might have an idea for how this regressed already.

[Henrik Böving]

CategoryTheory.Factorisation.instIsTerminalFactorisationInstCategoryFactorisationTerminal this seems to be one of the offending instances, which corresponds to this one: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Category/Factorisation.lean#L119 I don't know how people effectively minimize things that are so deep within mathlib? If someone wants to try the litmus test would be a meta program of the form:

#eval show MetaM _ from do
  let type ← inferType (← mkConstWithFreshMVarLevels ``CategoryTheory.Factorisation.instIsTerminalFactorisationInstCategoryFactorisationTerminal)
  isClass? type

as long as this shows none the instance is still breaking the invariant.

[Alex J. Best]

I think that doc-gen is right, docs#IsTerminal isn't a class even after unfolding, so the problem isn't the lean upgrade but simply the new content in mathlib. I have made #7245 to fix this. We should also add a linter so that this type of mistake is caught by mathlib CI and not docgen.

[Henrik Böving]

In that case I have a second question now if you look here: https://github.com/leanprover-community/mathlib4_docs/actions build times dropped from around 1h15min to 30min, did we change the machines that doc-gen is running on? Alternatively it must be skipping some work now due to a bug I guess.

[Alex J. Best]

And I made #7250 for the linter, there is one other failure that I might expect would show up in doc gen. And another internal declaration that should be skipped anyway. So hopefully isinstance -> type is a class holds going forward

[Alex J. Best]

Henrik Böving said:

In that case I have a second question now if you look here: https://github.com/leanprover-community/mathlib4_docs/actions build times dropped from around 1h15min to 30min, did we change the machines that doc-gen is running on? Alternatively it must be skipping some work now due to a bug I guess.

I'm not sure about that, the artifact on github is the same size as previously, so if it is skipping something it doesn't seem to be skipping something that forms a lot of the output

[Henrik Böving]

Alex J. Best said:

And I made #7250 for the linter, there is one other failure that I might expect would show up in doc gen. And another internal declaration that should be skipped anyway. So hopefully isinstance -> type is a class holds going forward

Maybe we want this to be an error in the compiler instead of just a linter in mathlib? Doing an instance for a non class doesn't ever seem useful to me.

[Henrik Böving]

Alex J. Best said:

Henrik Böving said:

In that case I have a second question now if you look here: https://github.com/leanprover-community/mathlib4_docs/actions build times dropped from around 1h15min to 30min, did we change the machines that doc-gen is running on? Alternatively it must be skipping some work now due to a bug I guess.

I'm not sure about that, the artifact on github is the same size as previously, so if it is skipping something it doesn't seem to be skipping something that forms a lot of the output

That's a good heuristic indeed. Who controls the machines that this runs on? / who can we ask about whether the machines changed? I dont think a ~2x speedup can be justified by optimizations that we did on the compiler overnight.

[Alex J. Best]

Henrik Böving said:

Alex J. Best said:

And I made #7250 for the linter, there is one other failure that I might expect would show up in doc gen. And another internal declaration that should be skipped anyway. So hopefully isinstance -> type is a class holds going forward

Maybe we want this to be an error in the compiler instead of just a linter in mathlib? Doing an instance for a non class doesn't ever seem useful to me.

I think that is a reasonable thing to do, though presumably it will require a little bit of thought as to how to handle the one exception to the linter there (a mutual block of inductives). So it might not be a 1-line fix in core

[Kyle Miller]

Interesting, I didn't realize that the instance attribute didn't check that the type was a class. I think I remember that in Lean 3 it was an error making instances for non-classes.

structure Foo where

instance : Foo := {}

inductive Foo' | mk

instance : Foo' := Foo'.mk

attribute [instance] Foo'.mk

instance : Nat := 0

[Kyle Miller]

You can't use non-classes for instance arguments at least:

example [Nat] : True := trivial
/-
invalid binder annotation, type is not a class instance
  Nat
-/

[Anne Baanen]

In Lean 3 it's indeed an error:

structure Foo

instance : Foo := {} -- error: `Foo' is not a class

[Anne Baanen]

In fact, Lean 3 and Lean 4 swapped behaviour precisely:

structure Foo : Type

instance : Foo := ⟨⟩
-- Lean 3 error: `Foo' is not a class
-- Lean 4: no problem

example [Foo] : true := ⟨⟩
-- Lean 3: no problem
-- Lean 4 error: invalid binder annotation, type is not a class instance