❌ Latest Build Failed: PrimeNumberTheoremAnd

docvb build failed

Build Log

✔ [7/160] Built UnicodeBasic/UnicodeCLib (118ms)
✔ [8/160] Built MD4Lean/md4c.static (451ms)
✔ [10/160] Built md4c.static:shared (41ms)
✖ [12/160] Building UnicodeBasic.CharacterDatabase (361ms)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/LeanArchitect/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/checkdecls/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/leancert/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/docvb/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.28.0-rc1/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/UnicodeBasic/CharacterDatabase.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/lib/lean/UnicodeBasic/CharacterDatabase.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/lib/lean/UnicodeBasic/CharacterDatabase.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/CharacterDatabase.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/CharacterDatabase.setup.json --json
error: UnicodeBasic/CharacterDatabase.lean:42:26: Invalid field `posGT`: The environment does not contain `Unicode.UCDStream.posGT`, so it is not possible to project the field `posGT` from an expression
  stream
of type `UCDStream`
error: Lean exited with code 1
✔ [15/160] Built BibtexQuery.Xml (374ms)
✔ [16/160] Built DocVerificationBridge.Compatibility (346ms)
✔ [17/160] Built BibtexQuery.ParsecExtra (470ms)
✔ [18/160] Built BibtexQuery.String (497ms)
✔ [19/160] Built BibtexQuery.Xml:c.o (106ms)
✔ [20/160] Built UnicodeBasic.Hangul (562ms)
✔ [21/160] Built DocVerificationBridge.Compatibility:c.o (164ms)
✔ [22/160] Built UnicodeBasic.Hangul:c.o (199ms)
✔ [23/160] Built UnicodeBasic.Hangul:dynlib (43ms)
✔ [24/160] Built BibtexQuery.String:c.o (307ms)
✔ [25/160] Built BibtexQuery.ParsecExtra:c.o (453ms)
✔ [26/160] Built DocGen4.Output.ToHtmlFormat (1000ms)
✔ [27/160] Built BibtexQuery.Entry (446ms)
✔ [28/160] Built DocGen4.Output.SourceLinker (1.1s)
✔ [29/160] Built DocGen4.Process.Hierarchy (1.2s)
✖ [30/160] Building DocGen4.Process.Attributes (1.2s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/LeanArchitect/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/checkdecls/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/leancert/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/docvb/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.28.0-rc1/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/DocGen4/Process/Attributes.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/lib/lean/DocGen4/Process/Attributes.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/lib/lean/DocGen4/Process/Attributes.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Attributes.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Attributes.setup.json --json
error: DocGen4/Process/Attributes.lean:85:6: Unknown constant `Lean.ReducibilityStatus.instanceReducible`

Note: Inferred this name from the expected resulting type of `.instanceReducible`:
  ReducibilityStatus
error: DocGen4/Process/Attributes.lean:172:4: Unknown constant `Lean.ReducibilityStatus.instanceReducible`

Note: Inferred this name from the expected resulting type of `.instanceReducible`:
  ReducibilityStatus
error: Lean exited with code 1
✔ [32/160] Built BibtexQuery.Entry:c.o (228ms)
✔ [33/160] Built DocGen4.Output.SourceLinker:c.o (98ms)
✔ [34/160] Built DocGen4.Process.Base (1.3s)
✔ [53/160] Built MD4Lean (966ms)
✔ [80/160] Built DocGen4.Process.Base:c.o (140ms)
✔ [81/160] Built BibtexQuery.Parser (497ms)
✔ [82/160] Built DocGen4.Process.Hierarchy:c.o (396ms)
✔ [83/160] Built UnicodeBasic.Types (1.7s)
✔ [125/160] Built DocVerificationBridge.Types (1.6s)
✔ [126/160] Built DocGen4.Output.ToHtmlFormat:c.o (1.2s)
✔ [127/160] Built MD4Lean:c.o (952ms)
✔ [128/160] Built MD4Lean:shared (45ms)
✔ [129/160] Built BibtexQuery.Parser:c.o (961ms)
✔ [130/160] Built DocVerificationBridge.Types:c.o (834ms)
✔ [131/160] Built UnicodeBasic.Types:c.o (1.8s)
✔ [133/160] Built UnicodeBasic.Types:dynlib (45ms)
✔ [134/160] Built DocVerificationBridge.Cache (1.5s)
✔ [135/160] Built DocVerificationBridge.Attributes (1.6s)
✔ [136/160] Built DocVerificationBridge.Inference (1.9s)
✔ [149/160] Built DocVerificationBridge.Attributes:c.o (590ms)
✔ [150/160] Built DocVerificationBridge.Cache:c.o (719ms)
✔ [151/160] Built DocVerificationBridge.Inference:c.o (1.4s)
✔ [152/160] Built Cli.Basic (6.6s)
✔ [153/160] Built Cli.Extensions (451ms)
✔ [154/160] Built Cli (296ms)
✔ [157/160] Built Cli:c.o (50ms)
✔ [158/160] Built Cli.Extensions:c.o (578ms)
✔ [159/160] Built Cli.Basic:c.o (4.7s)
Some required targets logged failures:
- UnicodeBasic.CharacterDatabase
- DocGen4.Process.Attributes
error: build failed

📋 View full command log (YAML)

← Back to Summary