❌ Latest Build Failed: MRiscX

docvb build failed

Build Log

✔ [7/160] Built md4c.static:shared (40ms)
✖ [12/160] Building UnicodeBasic.CharacterDatabase (338ms)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/docvb/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.28.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/UnicodeBasic/CharacterDatabase.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/.lake/build/lib/lean/UnicodeBasic/CharacterDatabase.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/.lake/build/lib/lean/UnicodeBasic/CharacterDatabase.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/CharacterDatabase.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.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 (354ms)
✔ [16/160] Built DocVerificationBridge.Compatibility (331ms)
✔ [17/160] Built UnicodeBasic.Hangul (542ms)
✔ [18/160] Built BibtexQuery.ParsecExtra (446ms)
✔ [19/160] Built BibtexQuery.String (465ms)
✔ [20/160] Built BibtexQuery.Xml:c.o (105ms)
✔ [21/160] Built DocVerificationBridge.Compatibility:c.o (162ms)
✔ [22/160] Built UnicodeBasic.Hangul:c.o (206ms)
✔ [23/160] Built UnicodeBasic.Hangul:dynlib (39ms)
✔ [24/160] Built BibtexQuery.String:c.o (297ms)
✔ [25/160] Built BibtexQuery.Entry (425ms)
✔ [26/160] Built BibtexQuery.ParsecExtra:c.o (433ms)
✔ [27/160] Built DocGen4.Output.ToHtmlFormat (985ms)
✔ [28/160] Built MD4Lean (938ms)
✔ [29/160] Built DocGen4.Process.Hierarchy (1.1s)
✔ [30/160] Built DocGen4.Output.SourceLinker (1.0s)
✔ [31/160] Built BibtexQuery.Entry:c.o (225ms)
✔ [32/160] Built DocGen4.Process.Base (1.3s)
✖ [33/160] Building DocGen4.Process.Attributes (1.2s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/docvb/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.28.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.lake/packages/doc-gen4/DocGen4/Process/Attributes.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/MRiscX/.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/MRiscX/.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/MRiscX/.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/MRiscX/.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
✔ [78/160] Built DocGen4.Output.SourceLinker:c.o (99ms)
✔ [80/160] Built BibtexQuery.Parser (468ms)
✔ [81/160] Built DocGen4.Process.Base:c.o (140ms)
✔ [82/160] Built DocGen4.Process.Hierarchy:c.o (383ms)
✔ [83/160] Built UnicodeBasic.Types (1.6s)
✔ [125/160] Built MD4Lean:c.o (863ms)
✔ [126/160] Built MD4Lean:shared (46ms)
✔ [127/160] Built DocVerificationBridge.Types (1.5s)
✔ [128/160] Built DocGen4.Output.ToHtmlFormat:c.o (1.1s)
✔ [129/160] Built BibtexQuery.Parser:c.o (821ms)
✔ [130/160] Built DocVerificationBridge.Types:c.o (729ms)
✔ [131/160] Built UnicodeBasic.Types:c.o (1.5s)
✔ [132/160] Built UnicodeBasic.Types:dynlib (43ms)
✔ [134/160] Built DocVerificationBridge.Cache (1.3s)
✔ [135/160] Built DocVerificationBridge.Attributes (1.4s)
✔ [136/160] Built DocVerificationBridge.Inference (1.6s)
✔ [149/160] Built DocVerificationBridge.Attributes:c.o (502ms)
✔ [150/160] Built DocVerificationBridge.Cache:c.o (627ms)
✔ [151/160] Built DocVerificationBridge.Inference:c.o (1.2s)
✔ [152/160] Built Cli.Basic (5.8s)
✔ [153/160] Built Cli.Extensions (398ms)
✔ [154/160] Built Cli (238ms)
✔ [157/160] Built Cli:c.o (46ms)
✔ [158/160] Built Cli.Extensions:c.o (477ms)
✔ [159/160] Built Cli.Basic:c.o (3.8s)
Some required targets logged failures:
- UnicodeBasic.CharacterDatabase
- DocGen4.Process.Attributes
error: build failed

📋 View full command log (YAML)

← Back to Summary