iris-tutorial-lean/lakefile.toml at main · logsem/iris-tutorial-lean · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
name = "textbook"
# Build the `textbook` executable by default; it transitively pulls in the
# book root (`IrisTutorialBook`), every chapter (`IrisTutorial.*`), and the
# generation machinery (`BookGen.*`). Listing the libs by name here does not
# work because `BookGen` has no root `BookGen.lean` module.
defaultTargets = ["textbook"]

[[require]]
name = "verso"
git = "https://github.com/leanprover/verso"
rev = "v4.32.0"

# Pin iris-lean to upstream HEAD as of 2026-09-05.
[[require]]
name = "iris"
git = "https://github.com/leanprover-community/iris-lean.git"
subDir = "Iris"
rev = "728a17140939e49af9236f7cb0d037da9ec52435"

# Book generation machinery inherited from the Verso textbook template
# (savedLean/savedImport elaborators, bibliography helpers). No root module
# file of its own, so glob its submodules explicitly.
[[lean_lib]]
name = "BookGen"
globs = ["BookGen.*"]

# The book root: the `#doc` document with front matter and chapter includes.
[[lean_lib]]
name = "IrisTutorialBook"

[[lean_lib]]
name = "IrisTutorial"

[[lean_exe]]
name = "textbook"
root = "BookGenMain"