8.3.1. Targets🔗

By default, all libraries and executables that are default build targets are included. To override this, specify explicit targets using [[targets]] entries. When targets is specified, only the listed libraries and modules are included, replacing the default targets entirely.

Each [[targets]] entry has the following keys:

• library — the name of a library; all modules belonging to it are included

• module — the name of a single module

An entry may specify library alone, module alone, or both (in which case the module must belong to the named library).

# Include all modules in a library
[[targets]]
library = "MyLib"

# Include a specific module
[[targets]]
module = "MyLib.Special.Page"

8.3.2. Exclusion🔗

Modules can be excluded from the site. Exclusion is recursive: the named module and all its children are removed.

exclude = ["MyLib.Internal", "MyLib.Deprecated"]

If both targets and exclude are specified, exclusion further narrows the target set.

8.3.3. Ordering🔗

By default, modules appear in the navigation bar in hierarchical alphabetical order. The order key specifies an ordering for top-level siblings: listed modules appear first in the given order, and unlisted modules follow alphabetically.

order = ["MyLib.Introduction", "MyLib.Core"]

To order children within a namespace, use [order_children]:

[order_children]
"MyLib.Core" = ["MyLib.Core.Basic", "MyLib.Core.Syntax"]

This is safe by default: newly added modules appear automatically in the alphabetical tail without requiring configuration changes.

8.3.4. Landing Page🔗

By default, the landing page is an auto-generated table of contents listing all included modules. To replace it with the rendered content of a specific module:

landing_page = "MyLib.Introduction"

The module remains in its normal position in the navigation bar.

8.3.5. Command Visibility🔗

Commands are identified by their leading keywords. Each pattern is matched against the first keyword tokens that appear in the command; for example, "def" matches def commands and "#eval" matches #eval commands. Multi-word patterns like "#print axioms" match commands whose leading keywords start with that sequence. By default, everything except the module header is shown (the module header is present but collapsed by default).

hide_commands = ["import", "open", "set_option"]

Because matching uses only the leading keywords, #eval and #eval in are both matched by the pattern "#eval".

This can be scoped per module prefix via [modules] (see Per-Module Configuration below).

8.3.6. Command Output🔗

Some commands produce output (e.g., #eval, #check). To make the output visible, the generated HTML will display this output immediately after the command that produced it. A configurable list controls which commands have their output displayed in the rendered code box. The default list includes #eval, #check, #print, and #reduce.

show_output = ["#eval", "#check", "#print", "#reduce"]

This can be scoped per module prefix via [modules].

8.3.7. Imports List🔗

Each page shows a collapsible list of imports, collapsed by default. Imports whose modules are included in the site appear as links; the rest appear as plain text. To disable the imports list:

show_imports = false

This can be scoped per module prefix via [modules].

8.3.8. Declaration Docstrings🔗

By default, declaration docstrings (/-- ... -/) are shown in code boxes alongside the definitions they document. If the docstrings are part of the API of the program but are not intended to be shown to readers, then they can be removed. This can be controlled globally and overridden per declaration:

# Hide all declaration docstrings
show_docstrings = false

# ...but still show these specific ones
show_docstrings_for = ["MyLib.Core.mainFunction"]

Alternatively, docstrings can be shown by default with specific exceptions hidden:

# Show all (this is the default)
show_docstrings = true

# ...but hide these
hide_docstrings_for = ["MyLib.Internal.helper"]

docstrings_as_text = true

8.3.9. Per-Module Configuration🔗

Any top-level setting that controls content rendering can be scoped to a module prefix using [modules]. The most specific matching prefix wins. Unset keys inherit from the global defaults.

# Global defaults
hide_commands = ["import", "open", "set_option"]
show_docstrings = true

# Override for the tutorial subtree
[modules."MyLib.Tutorial"]
hide_commands = ["import"]
show_docstrings = false
show_docstrings_for = ["MyLib.Tutorial.mainExample"]

# Further override for a child module
[modules."MyLib.Tutorial.Namespaces"]
hide_commands = ["import", "set_option"]

Per-module entries can also set a page title and URL slug:

[modules."MyLib.Core.Basic"]
title = "Getting Started"
url = "getting-started"

The full set of keys available under [modules."..."]:

title

Page title and navbar label. The default value is the module's name.

url

URL path for this module's page. The default is derived from the module name (e.g., MyLib.Data.Basic is served at MyLib/Data/Basic/). When a url override is set on a parent module, child modules inherit it as a prefix. For example, if MyLib.Data has url = "data-docs", then MyLib.Data.Basic is served at data-docs/Basic/ rather than MyLib/Data/Basic/. To override a child independently, give it its own [modules] entry.

hide_commands

Commands to hide in the output.

show_output

Commands whose output is shown.

show_imports

Whether to show the collapsible imports list.

show_docstrings

Whether to show declaration docstrings

show_docstrings_for

Declarations whose docstrings should be shown regardless of the show_docstrings setting.

hide_docstrings_for

Declarations whose docstrings should be hidden regardless of the show_docstrings setting.

docstrings_as_text

Wender declaration docstrings as prose text. The default is false, causing them to be visually grouped with the code.

Module names are quoted as strings because TOML dot-separated keys would otherwise be ambiguous with config key names.

8.3.10. Site Metadata🔗

Defaults are discovered from the Lake configuration. Override them in literate.toml:

[metadata]
title = "My Library"
description = "A Lean library for ..."
favicon = "images/favicon.png"

No favicon is included by default. If favicon is set, the file is copied to the output directory and linked from every page.

8.3.11. Theming🔗

CSS variables can be overridden under [theme]. Keys are the variable names without the --verso- prefix, with hyphens replaced by underscores:

[theme]
text_font_family = "Georgia, serif"
code_font_family = "'Fira Code', monospace"
background_color = "#fefefe"
link_color = "#1a6b47"

Dark-mode overrides are specified under [theme.dark]:

[theme.dark]
background_color = "#1a1a2e"
link_color = "#5cb89a"

Any variable not overridden retains its default value.

8.3.12. Extra CSS and JavaScript🔗

Additional CSS or JavaScript files can be included. Paths are relative to the project root. CSS files are added as <link> tags and JS files as <script> tags in every page:

extra_css = ["custom/style.css", "custom/print.css"]
extra_js = ["custom/analytics.js"]

These files are copied into the output directory and linked after the default Verso styles, so custom CSS can override any built-in rules.

8.4.1. GitHub Pages🔗

To enable deployment to GitHub Pages, run:

lake exe verso setup-literate

This generates a GitHub Actions workflow file at .github/workflows/verso-literate-pages.yml that automatically builds and deploys the site on every push to main.

After generating the workflow:

1. Go to the repository's Settings → Pages → Source and select GitHub Actions.

2. Commit and push the generated workflow file.

As usual, make sure that lake-manifest.json is committed to the repository.

The first build may be slow because it compiles the full Lean project. Subsequent builds are faster thanks to .lake caching.

When Verso is upgraded, lake build :literateHtml will warn if the workflow file is outdated. Re-running lake exe verso setup-literate updates it, saving the previous version as a .bak file so that any manual customizations can be merged by hand.