Verso

Stream: mathlib4

[Antoine Chambert-Loir]

I have just tried to install Verso and to follow the instructions in the README.md file.
I wanted to have a preview of the demo text book, hence I entered lake build as indicated, and I got an error message

(15:25) pro-acl > lake build
ℹ [255/276] Replayed DemoTextbook
info: examples/textbook/DemoTextbook.lean:6:0: 15
✖ [274/276] Building DemoTextbookMain
trace: .> LEAN_PATH=/Users/chambert/Documents/Lean4/Verso/.lake/packages/subverso/.lake/build/lib/lean:/Users/chambert/Documents/Lean4/Verso/.lake/packages/MD4Lean/.lake/build/lib/lean:/Users/chambert/Documents/Lean4/Verso/.lake/build/lib/lean /Users/chambert/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean /Users/chambert/Documents/Lean4/Verso/examples/textbook/DemoTextbookMain.lean -R /Users/chambert/Documents/Lean4/Verso/examples/textbook -o /Users/chambert/Documents/Lean4/Verso/.lake/build/lib/lean/DemoTextbookMain.olean -i /Users/chambert/Documents/Lean4/Verso/.lake/build/lib/lean/DemoTextbookMain.ilean -c /Users/chambert/Documents/Lean4/Verso/.lake/build/ir/DemoTextbookMain.c --load-dynlib /Users/chambert/Documents/Lean4/Verso/.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.dylib --plugin /Users/chambert/Documents/Lean4/Verso/.lake/packages/MD4Lean/.lake/build/lib/libMD4Lean.dylib --plugin /Users/chambert/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/lib/lean/libLake_shared.dylib --json
error: examples/textbook/DemoTextbookMain.lean:16:5: unknown namespace 'DemoTextbook'
error: examples/textbook/DemoTextbookMain.lean:37:25: unknown constant 'Block.savedLean'
error: examples/textbook/DemoTextbookMain.lean:44:25: unknown constant 'Block.savedImport'
error: examples/textbook/DemoTextbookMain.lean:69:29: unknown identifier 'DemoTextbook.«the canonical document object name»'
error: Lean exited with code 1
Some required builds logged failures:
- DemoTextbookMain
error: build failed

[Shreyas Srinivas]

I think it is easier to clone @Pim Otte 's analysis-book repository at the moment

[Shreyas Srinivas]

It is also possible that this error comes from mistamtched toolchains

[Pim Otte]

In particular, if you want play with the Manual genre, look at this commit. The later versions are based on the Site genre, because we wanted to use the Literate Lean page.

[Antoine Chambert-Loir]

I think I cloned the last version, and something doesn't work in my setup. The first step already breaks :

(22:10) pro-acl > cd analysis
(22:10) pro-acl > lake exe Analysis:docs
error: unknown executable Analysis:docs

and the second one missed mathlib, that is not present in lakefile.toml…

[Pim Otte]

I think you want to run a lake build first then

[Antoine Chambert-Loir]

I ended doing that, using the documentation from Tao's book…

[Pim Otte]

If you're building the latest version, you might want to build from his repo in any case. It has some improvements that are not in my repo. The reason I linked to an old commit of mine is because that's the last time I did something with the Manual genre, which is also what's used for the demo textbook

[Shreyas Srinivas]

Is there a stable tag for verso, similar to mathlib?