Updates available but manual intervention required

[github-actions]

Try lake update and then investigate why this update causes lake build, lake test, or lake lint to fail.
Files changed in update:

• lake-manifest.json
• lean-toolchain

Build Output

✖ [182/339] Building Mathlib.Util.AddRelatedDecl (2.2s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Util/AddRelatedDecl.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/AddRelatedDecl.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/AddRelatedDecl.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/AddRelatedDecl.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/AddRelatedDecl.setup.json --json
error: Mathlib/Util/AddRelatedDecl.lean:43:26: Unknown constant `Lean.Meta.TransparencyMode.implicit`

Note: Inferred this name from the expected resulting type of `.implicit`:
  TransparencyMode
error: Lean exited with code 1
✖ [184/339] Building Mathlib.Tactic.Core (2.1s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Tactic/Core.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Core.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Core.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Core.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Core.setup.json --json
error: Mathlib/Tactic/Core.lean:36:18: Type mismatch
  newDoc
has type
  Option (TSyntax `Lean.Parser.Command.docComment)
but is expected to have type
  Option (TSyntax `Lean.Parser.Command.docComment × Bool)
error: Lean exited with code 1
✖ [361/842] Building Batteries.Tactic.Alias (2.4s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/Batteries/Tactic/Alias.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.setup.json --json
error: Batteries/Tactic/Alias.lean:177:6: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  177:45 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Batteries/Tactic/Alias.lean:209:4: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  209:43 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Lean exited with code 1
✖ [442/842] Building Mathlib.Util.CompileInductive (2.4s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Util/CompileInductive.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/CompileInductive.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/CompileInductive.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/CompileInductive.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/CompileInductive.setup.json --json
error: Mathlib/Util/CompileInductive.lean:264:0: Failed to find LCNF signature for Float.val
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float._sizeOf_1✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: Failed to find LCNF signature for Float32.val
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32._sizeOf_1✝', which is 'noncomputable'
error: Lean exited with code 1
Some required targets logged failures:
- Mathlib.Util.AddRelatedDecl
- Mathlib.Tactic.Core
- Batteries.Tactic.Alias
- Mathlib.Util.CompileInductive
error: build failed

Test Output

✖ [185/343] Building Mathlib.Util.AddRelatedDecl (2.0s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Util/AddRelatedDecl.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/AddRelatedDecl.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/AddRelatedDecl.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/AddRelatedDecl.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/AddRelatedDecl.setup.json --json
error: Mathlib/Util/AddRelatedDecl.lean:43:26: Unknown constant `Lean.Meta.TransparencyMode.implicit`

Note: Inferred this name from the expected resulting type of `.implicit`:
  TransparencyMode
error: Lean exited with code 1
✖ [187/343] Building Mathlib.Tactic.Core (1.0s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Tactic/Core.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Core.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/Core.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Core.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Tactic/Core.setup.json --json
error: Mathlib/Tactic/Core.lean:36:18: Type mismatch
  newDoc
has type
  Option (TSyntax `Lean.Parser.Command.docComment)
but is expected to have type
  Option (TSyntax `Lean.Parser.Command.docComment × Bool)
error: Lean exited with code 1
✖ [399/1128] Building Batteries.Tactic.Alias (2.4s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/Batteries/Tactic/Alias.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.setup.json --json
error: Batteries/Tactic/Alias.lean:177:6: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  177:45 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Batteries/Tactic/Alias.lean:209:4: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  209:43 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Lean exited with code 1
✖ [480/1128] Building Mathlib.Util.CompileInductive (2.3s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/Mathlib/Util/CompileInductive.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/CompileInductive.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Util/CompileInductive.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/CompileInductive.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/ir/Mathlib/Util/CompileInductive.setup.json --json
error: Mathlib/Util/CompileInductive.lean:264:0: Failed to find LCNF signature for Float.val
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float._sizeOf_1✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: Failed to find LCNF signature for Float32.val
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32.rec✝', which is 'noncomputable'
error: Mathlib/Util/CompileInductive.lean:264:0: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Float32._sizeOf_1✝', which is 'noncomputable'
error: Lean exited with code 1
Some required targets logged failures:
- Mathlib.Util.AddRelatedDecl
- Mathlib.Tactic.Core
- Batteries.Tactic.Alias
- Mathlib.Util.CompileInductive
error: build failed

Lint Output

✖ [46/52] Building Batteries.Tactic.Alias (1.3s)
trace: .> LEAN_PATH=/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/geb-mathlib/geb-mathlib/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/Batteries/Tactic/Alias.lean -o /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.olean -i /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Alias.ilean -c /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.c --setup /home/runner/work/geb-mathlib/geb-mathlib/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.setup.json --json
error: Batteries/Tactic/Alias.lean:177:6: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  177:45 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Batteries/Tactic/Alias.lean:209:4: overloaded, errors 
  Function expected at
    Parser.Command.addDocString
  but this term has type
    Parser.Parser
  
  Note: Expected a function because this term is being applied to the argument
    declName
  
  209:43 Application type mismatch: The argument
    doc
  has type
    TSyntax `Lean.Parser.Command.docComment × Bool
  but is expected to have type
    TSyntax `Lean.Parser.Command.docComment
  in the application
    Lean.addDocString declName (mkNullNode #[]) doc
error: Lean exited with code 1
Some required targets logged failures:
- Batteries.Tactic.Alias
error: build failed

[rokopt]

Fixed by #113 .