DOCSEARCHbyAlgolia
Submit Docs

Verso Documentation

repository·main·Indexed 18 days ago

https://github.com/leanprover/verso

An authoring tool for Lean that uses a Markdown-like syntax to create technical documentation, books, and API references. Verso leverages Lean's metaprogramming to provide extensible features and advanced rendering for Lean code, including interactive proof states and a Lean-to-HTML renderer with hovers and 'go to definition' links. It supports semantic cross-referencing between documents via domains and objects, and provides specialized genres for instructional materials and research papers.

Tokens
5.9K
Snippets
26
Records
32
Agent score
60%

What's inside Verso

  1. Understand Verso deployment overlays

    main

    The overlay.py script applies unified changes to all deployed versions in the postdeploy branch. This allows for global updates without modifying historical version tags.

    Current Overlays:

    • noindex meta tag: Injected into all HTML files in versioned directories except latest/ to prevent search engine indexing of old versions.
    • Canonical URL: Injected into all HTML files to point to the authoritative version under latest/.

    Best Practices for Overlays:

    • Overlays should ideally be monotonic (only adding data, not changing existing contracts).
    • Documents should fail gracefully if expected injected data is missing.

  2. How cross-document cross-references work

    main

    Verso allows semantic linking between documents using a cross-referencing database. Instead of linking to URLs, you link to objects within domains (namespaces).

    Key Concepts

    • Domains: Namespaces for organized information (e.g., "constant names", "chapters").
    • Objects: Entities within a domain identified by a canonical name (e.g., a fully-qualified constant name).
    • Remotes: External Verso sites that provide cross-reference data (similar to Git remotes).
    • xref.json: The file emitted by Verso genres that contains the cross-reference database.

    Workflow

    1. Define remotes in a verso-sources.json file in your project root (next to lean-toolchain).
    2. Sync the remote data locally using lake exe verso sync.
    3. Use the ref role in your markup to create links: {ref "canonicalName" (remote := "remoteName")}[link text].

    Downloaded data is stored in the .verso directory.

  5. Use the experimental Lean-to-HTML renderer

    main

    Verso provides a renderer that converts Lean code into interactive HTML featuring hovers, "go to definition" links, and rendered intermediate proof states.

    Step 1: Add Verso as a dependency

    For lakefile.toml:

    [[require]]
name = "verso"
git = "https://github.com/leanprover/verso.git"
rev = "v4.25.0" # Replace with your Lean version

    For lakefile.lean:

    require verso from git "https://github.com/leanprover/verso.git"@"v4.25.0"

    Step 2: Generate literate program data

    Build the literate facet for your library (e.g., MyLib):

    lake build MyLib:literate

    This creates files in .lake/build/literate.

    Step 3: Generate HTML

    Run the verso-html executable to convert the literate data into HTML in a target directory (e.g., html):

    lake exe verso-html .lake/build/literate html

    Step 4: Preview

    You can preview the output using a local Python server:

    python3 -m http.server 8000 -d html

    Note: To enable rendering of Verso docstrings and moduledocs in source files, set doc.verso to true.

    # 1. Build literate facet
lake build MyLib:literate

# 2. Generate HTML
lake exe verso-html .lake/build/literate html

# 3. Preview
python3 -m http.server 8000 -d html

  6. Verify Unicode input after updates

    main

    After updating the Unicode input libraries, you must rebuild the site and run the browser tests to ensure abbreviation input functionality remains intact.

    1. Rebuild the HTML documentation using lake exe usersguide.
    2. Run the browser tests using pytest via uv.
    # Rebuild documentation
lake exe usersguide --delay-html-multi multi.json --delay-html-single single.json
lake exe usersguide --resume-html-multi multi.json --resume-html-single single.json

# Run browser tests
uv run --project browser-tests --extra test pytest browser-tests/test_search.py -v

  8. Test deployment overlays locally

    main

    To verify overlay.py logic before pushing to GitHub, follow these steps:

    1. Sync deployment branches:

      git fetch
git checkout deploy
git reset --hard remotes/upstream/deploy
git checkout postdeploy
git reset --hard remotes/upstream/postdeploy

    2. Run the overlay script from the main branch:

      python3 -B deploy/overlay.py . deploy postdeploy

    3. Inspect results using git show to verify injected tags (e.g., checking for noindex in old versions vs latest):

      git show postdeploy:4.29.0-rc1/index.html
git show postdeploy:latest/index.html
    python3 -B deploy/overlay.py . deploy postdeploy

  10. Use test projects for Verso development

    main

    The test-projects directory contains projects specifically designed for the development and testing of Verso.

    Warning: These projects are tightly integrated with the Verso build process. They are not intended to be used as standalone projects; attempting to use them independently will require substantial modifications to their build processes.

  11. Deploy a new version of the manual

    main

    Deployment is automated via GitHub Actions triggered by pushing tags.

    Workflow:

    1. Push a tag in the format vX.Y.Z (e.g., v4.32.0) to the commit intended for release.
    2. GitHub Actions will trigger the deployment pipeline.

    Deployment Architecture:

    • deploy/prep.sh: Sets up OS dependencies.
    • deploy/build.sh: Builds the manual generator executable.
    • deploy/generate.sh: Builds the manual into _out/html-multi and packages assets.
    • deploy/release.py: Manages the deploy branch by copying HTML, stamping files with commit SHAs/timestamps, and updating latest/ and stable/ directories.
    • deploy/overlay.py: Triggered by pushes to deploy, this script computes the postdeploy branch by applying metadata overlays.
    • postdeploy branch: Pushing to this branch triggers the final Netlify publication.

  12. View the Verso Manual in HTML

    main

    The Verso user's guide is provided in HTML format. Because it is structured as a website, you cannot simply open the files in a browser from your file system; you must serve them using a local web server. You can use the built-in Python HTTP server to do this.

    ```bash
python3 -m http.server 8080

    After running the command, open http://localhost:8080 in your web browser to access the documentation.