I can't build doc-gen4 (main)

Stream: lean4

[Bulhwi Cha]

✖ [125/125] Building «doc-gen4»
trace: .> /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/clang -o /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/Main.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Base.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Hierarchy.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Attributes.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/NameInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/AxiomInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/TheoremInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/OpaqueInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/DefinitionInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/InstanceInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/StructureInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/InductiveInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/ClassInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/DocInfo.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Analyze.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Load.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ToHtmlFormat.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Base.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Navbar.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Template.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Index.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Arg.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/MD4Lean/.lake/build/ir/MD4Lean.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/Types.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/CharacterDatabase.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/Hangul.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/TableLookup.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/DocString.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Inductive.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Structure.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Class.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Definition.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Instance.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ClassInductive.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Module.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/NotFound.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Find.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/References.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/ParsecExtra.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/String.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Entry.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Parser.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/TexDiacritics.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Name.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Format.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Bibtex.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/SourceLinker.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Search.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ToJson.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/FoundationalTypes.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/doc-gen4/.lake/build/ir/DocGen4.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/Cli/.lake/build/ir/Cli/Basic.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/Cli/.lake/build/ir/Cli/Extensions.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/Cli/.lake/build/ir/Cli.c.o.export /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.a -rdynamic -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib/lean --sysroot /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5 -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread
info: stderr:
ld.lld: error: undefined symbol: lean_alloc_small
>>> referenced by wrapper.c
>>>               wrapper.o:(lean_alloc_ctor_memory) in archive /home/chabulhwi/lean-projects/tpil-solutions/.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/clang' exited with code 1
Some required builds logged failures:
- «doc-gen4»
error: build failed

[Bulhwi Cha]

Since I'm unable to build doc-gen4, I can't generate the documents for my project.

[Kevin Buzzard]

I don't know much about doc-gen4 but maybe this is the same problem as discussed in this thread ?

[Bulhwi Cha]

Correction: I tried to build the current main branch of doc-gen4, not v4.20.0-rc5. Currently, there's no tag for it.

[Kim Morrison]

Working fine for me.

[Bulhwi Cha]

I also failed to build the v4.19.0 release of doc-gen4:

✖ [125/125] Building «doc-gen4»
trace: .> /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/bin/clang -o ././../.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 ././../.lake/packages/doc-gen4/.lake/build/ir/Main.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Base.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Hierarchy.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Attributes.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/NameInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/AxiomInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/TheoremInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/OpaqueInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/DefinitionInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/InstanceInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/StructureInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/InductiveInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/ClassInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/DocInfo.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process/Analyze.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Process.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Load.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ToHtmlFormat.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Base.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Navbar.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Template.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Index.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Arg.c.o.export ././../.lake/packages/MD4Lean/.lake/build/ir/MD4Lean.c.o.export ././../.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/Types.c.o.export ././../.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/CharacterDatabase.c.o.export ././../.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/Hangul.c.o.export ././../.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic/TableLookup.c.o.export ././../.lake/packages/UnicodeBasic/.lake/build/ir/UnicodeBasic.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/DocString.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Inductive.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Structure.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Class.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Definition.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Instance.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ClassInductive.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Module.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/NotFound.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Find.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/References.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/ParsecExtra.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/String.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Entry.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Parser.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/TexDiacritics.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Name.c.o.export ././../.lake/packages/BibtexQuery/.lake/build/ir/BibtexQuery/Format.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Bibtex.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/SourceLinker.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/Search.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/ToJson.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output/FoundationalTypes.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4/Output.c.o.export ././../.lake/packages/doc-gen4/.lake/build/ir/DocGen4.c.o.export ././../.lake/packages/Cli/.lake/build/ir/Cli/Basic.c.o.export ././../.lake/packages/Cli/.lake/build/ir/Cli/Extensions.c.o.export ././../.lake/packages/Cli/.lake/build/ir/Cli.c.o.export ././../.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.a -rdynamic --sysroot /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0 -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/lib -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/lib/glibc /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/lib/glibc/libc_nonshared.a /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread
info: stderr:
ld.lld: error: undefined symbol: lean_alloc_small
>>> referenced by wrapper.c
>>>               wrapper.o:(lean_alloc_ctor_memory) in archive ././../.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.19.0/bin/clang' exited with code 1
Some required builds logged failures:
- «doc-gen4»
error: build failed

[Bulhwi Cha]

Kim Morrison said:

Working fine for me.

Is anyone having the same issue as mine?

[Bulhwi Cha]

Bulhwi Cha said:

Let me try removing the .lake subdirectory and rebuilding it.

After removing .lake, I can build doc-gen4.

[Bulhwi Cha]

Do I have to remove it every time I encounter a build error?

[Sebastian Ullrich]

@Mac Malone This seems to be a dependency tracking issue with the MD4Lean FFI code. Should it be updated to the recent FFI additions, would that plausibly have helped?

[Jz Pan]

Sebastian Ullrich said:

Mac Malone This seems to be a dependency tracking issue with the MD4Lean FFI code. Should it be updated to the recent FFI additions, would that plausibly have helped?

Oops. In current MD4Lean no FFI related package is used. So I don't know what happens. PRs welcome.