### Prepare Build Environment Source: https://github.com/leanprover/verso/blob/main/README.md This script is used to set up the build environment by installing necessary OS-level dependencies. ```shell # deploy/prep.sh # Installs OS-level dependencies. ``` -------------------------------- ### Install uv Package Manager (Homebrew) Source: https://github.com/leanprover/verso/blob/main/README.md Install the uv package manager using Homebrew. This is an alternative method for installing uv. ```bash $ brew install uv ``` -------------------------------- ### Install uv Package Manager Source: https://github.com/leanprover/verso/blob/main/README.md Install the uv package manager using a curl script. This is a prerequisite for running some browser tests. ```bash $ curl -LsSf https://astral.sh/uv/install.sh | sh ``` -------------------------------- ### Install Playwright Browser Engines Source: https://github.com/leanprover/verso/blob/main/README.md In the browser-tests directory, install the browser testing engines used by Playwright. This command uses uv to manage the installation. ```bash $ cd browser-tests $ uv run --extra test playwright install chromium firefox ``` -------------------------------- ### Install Tippy.js via npm or Yarn Source: https://github.com/leanprover/verso/blob/main/vendored-js/tippy/README.md Use npm or Yarn to add Tippy.js to your project dependencies. ```bash # npm npm i tippy.js # Yarn yarn add tippy.js ``` -------------------------------- ### Serve Verso Manual Locally Source: https://github.com/leanprover/verso/blob/main/README-html.md Use Python's built-in HTTP server to host the HTML documentation. Ensure you are in the directory containing the documentation files before running this command. ```bash python3 -m http.server 8080 ``` -------------------------------- ### Build and Test Verso Usersguide Source: https://github.com/leanprover/verso/blob/main/static-web/search/README.txt Commands to rebuild the Verso usersguide with updated components and run browser tests to confirm Unicode input functionality. ```bash 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 ``` ```bash uv run --project browser-tests --extra test pytest browser-tests/test_search.py -v ``` -------------------------------- ### Run Browser Tests with Existing Server Source: https://github.com/leanprover/verso/blob/main/README.md Run browser tests and connect to an existing local web server by providing its URL with the --server-url option. ```bash $ uv run --project browser-tests --extra test pytest browser-tests --server-url=http://localhost:4000 -v ``` -------------------------------- ### HTML Starter Template for KaTeX Source: https://github.com/leanprover/verso/blob/main/vendored-js/katex/README.md Include this HTML structure in your project to set up KaTeX with its CSS and JavaScript files, including the auto-render extension for automatic math detection. Ensure the HTML5 doctype is used for proper rendering. ```html ... ``` -------------------------------- ### Generate Manual and Package Assets Source: https://github.com/leanprover/verso/blob/main/README.md This script builds the manual, saves the output in '_out/html-multi', and packages the release assets. ```shell # deploy/generate.sh # Builds the manual, saving it in '_out/html-multi' and packaging release assets. ``` -------------------------------- ### Build Literate HTML Site Source: https://github.com/leanprover/verso/blob/main/test-projects/literate-config/README.md Run the full pipeline to generate the literate site. This command writes the resulting site to `.lake/build/literate-html/`. ```shell lake build :literateHtml ``` -------------------------------- ### Build Verso Executable Source: https://github.com/leanprover/verso/blob/main/README.md This script is responsible for building the executable program that generates the user's manual. ```shell # deploy/build.sh # Builds the executable that generates the manual. ``` -------------------------------- ### Import Tippy.js and CSS Source: https://github.com/leanprover/verso/blob/main/vendored-js/tippy/README.md Import the tippy constructor and the core CSS file when using a module bundler. ```javascript import tippy from 'tippy.js'; import 'tippy.js/dist/tippy.css'; ``` -------------------------------- ### Run Browser Tests with Custom Site Directory Source: https://github.com/leanprover/verso/blob/main/README.md Run browser tests and specify a custom output directory for the site using the --site-dir option. ```bash $ uv run --project browser-tests --extra test pytest browser-tests --site-dir=dist -v ``` -------------------------------- ### Run Overlay Script Locally Source: https://github.com/leanprover/verso/blob/main/README.md Execute the overlay.py script from the repository's main branch in a clean working directory. This command generates the postdeploy content based on the deploy branch. ```shell python3 -B deploy/overlay.py . deploy postdeploy ``` -------------------------------- ### Run Browser Tests (browser-tests Directory) Source: https://github.com/leanprover/verso/blob/main/README.md Run the browser tests from within the browser-tests directory. The --project flag is not needed here. ```bash $ cd browser-tests $ uv run --extra test pytest . -v ``` -------------------------------- ### Include Tippy.js via CDN Source: https://github.com/leanprover/verso/blob/main/vendored-js/tippy/README.md Include Tippy.js and Popper.js using CDN links in your HTML. ```html ``` -------------------------------- ### Run Browser Tests (Project Root) Source: https://github.com/leanprover/verso/blob/main/README.md Run the browser tests from the project root directory. This command uses uv to execute pytest and specifies the browser-tests project. ```bash $ uv run --project browser-tests --extra test pytest browser-tests -v ``` -------------------------------- ### Inspect Postdeploy Content (Latest Version) Source: https://github.com/leanprover/verso/blob/main/README.md View the content of the index.html file in the latest version of the postdeploy branch. This helps confirm that certain overlays, like the 'noindex' meta tag, are not applied to the latest version. ```shell git show postdeploy:latest/index.html ``` -------------------------------- ### Inspect Postdeploy Content (Specific Version) Source: https://github.com/leanprover/verso/blob/main/README.md View the content of a specific file within the postdeploy branch, such as an index.html file for version 4.29.0-rc1. This is useful for verifying changes made by the overlay script. ```shell git show postdeploy:4.29.0-rc1/index.html ``` -------------------------------- ### Generate HTML from Literate Program Data Source: https://github.com/leanprover/verso/blob/main/README.md Generate HTML from the literate program data. The HTML will be placed in the specified directory (e.g., 'html'). ```bash lake exe verso-html .lake/build/literate html ``` -------------------------------- ### Fetch and Minify Unicode Input Library Source: https://github.com/leanprover/verso/blob/main/static-web/search/README.txt Fetches the minified ESM bundle for the `@leanprover/unicode-input` package from esm.sh and removes the source map comment. This is used to update `unicode-input.min.js`. ```bash $ curl -sS https://esm.sh/@leanprover/unicode-input@0.1.9/es2022/unicode-input.mjs \ | sed '/^\/\/# sourceMappingURL=/d' \ > static-web/search/unicode-input.min.js ``` -------------------------------- ### Process Deploy Branch to Postdeploy Branch Source: https://github.com/leanprover/verso/blob/main/README.md This script processes changes from the 'deploy' branch to create the 'postdeploy' branch, handling overlays and desired state. ```python # deploy/overlay.py # Processes 'deploy' -> 'postdeploy'. ``` -------------------------------- ### Verso Remote Sources Configuration Source: https://github.com/leanprover/verso/blob/main/README.md This JSON configuration file defines remote Verso documentation sources. It specifies the root URL, update frequency, and display names for each remote. Ensure this file is named `verso-sources.json` and placed alongside your `lean-toolchain` file. ```json { "version": 0, // Version specifier for the configuration file format // Configured remotes. Keys are their internal names, used by the author. "sources": { "manual": { // The root of the source. xref.json should be here, and all // links will be relative to this: "root": "https://lean-lang.org/doc/reference/latest/", // How often should it be updated? // * "manual" means only when running verso sync, // * {"days": N} means every N days "updateFrequency": "manual", // Ultra-short name shown to readers to disambiguate link texts // (e.g. when linking to multiple versions of the same document) "shortName": "latest", // Longer name shown to readers to explain links "longName": "Lean Language Reference" } } } ``` -------------------------------- ### Add Verso Package Dependency (lakefile.toml) Source: https://github.com/leanprover/verso/blob/main/README.md Add Verso as a package dependency in your lakefile.toml configuration. ```toml [[require]] name = "verso" git = "https://github.com/leanprover/verso.git" rev = "latest" ``` -------------------------------- ### Add Verso Package Dependency (lakefile.lean) Source: https://github.com/leanprover/verso/blob/main/README.md Add Verso as a package dependency in your lakefile.lean configuration. ```lean4 require verso from git "https://github.com/leanprover/verso.git"@"latest" ``` -------------------------------- ### Run Browser Tests with Specific Port Source: https://github.com/leanprover/verso/blob/main/README.md Run browser tests and force a specific port for the local web server using the --port option. This is useful if the default port selection fails. ```bash $ uv run --project browser-tests --extra test pytest browser-tests --port=3000 -v ``` -------------------------------- ### Format Code with Prettier Source: https://github.com/leanprover/verso/blob/main/README.md Format all eligible files (HTML, CSS, JavaScript, and Markdown) in the project using Prettier from the command line. This command writes the formatted code back to the files. ```bash npx prettier --write . ``` -------------------------------- ### Build Literate Program Data Source: https://github.com/leanprover/verso/blob/main/README.md Generate literate program data from your Lean libraries or modules by building their 'literate' facet. This command generates files in the .lake/build/literate directory. ```bash lake build MyLib:literate ``` -------------------------------- ### Initialize Plausible Analytics Source: https://github.com/leanprover/verso/blob/main/doc/stats.html This JavaScript code initializes Plausible Analytics. It ensures the plausible object and its methods are available, and then calls the init method. ```javascript window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}}; plausible.init() ``` -------------------------------- ### Rewrite Import and Compile Unicode Input Component Source: https://github.com/leanprover/verso/blob/main/static-web/search/README.txt Fetches the TypeScript source for the unicode input component, rewrites the import statement to use the local `unicode-input.min.js` file, and then compiles it using esbuild. The local dependency is marked as external to prevent inlining. ```bash curl -sS https://raw.githubusercontent.com/leanprover/vscode-lean4/master/lean4-unicode-input-component/src/index.ts \ | sed "s|from '@leanprover/unicode-input'|from './unicode-input.min.js'|g" \ > /tmp/index.ts ``` ```bash $ npm install --save-dev esbuild @leanprover/unicode-input@0.1.9 $ npx esbuild /tmp/index.ts \ --bundle --format=esm --minify \ --external:'./unicode-input.min.js' \ --outfile=static-web/search/unicode-input-component.min.js ``` -------------------------------- ### Run Browser Tests with Single Browser Engine Source: https://github.com/leanprover/verso/blob/main/README.md Run browser tests using only a specific browser engine (e.g., 'chromium') by using the -k option to filter tests. ```bash $ uv run --project browser-tests --extra test pytest browser-tests -v -k "chromium" ``` -------------------------------- ### KaTeX Rendering API Source: https://github.com/leanprover/verso/blob/main/vendored-js/katex/README.md Provides methods for rendering LaTeX math expressions into HTML. ```APIDOC ## KaTeX Rendering API ### Description This section details the primary JavaScript functions provided by the KaTeX library for rendering mathematical expressions. ### Methods #### `katex.render(expression, element, options)` * **Description**: Renders a LaTeX math expression directly into a specified DOM element. * **Parameters**: * `expression` (string) - The LaTeX string to render. * `element` (HTMLElement) - The DOM element to render the math into. * `options` (object) - Optional configuration object for rendering. ### Request Example ```javascript katex.render("c = \\pm\\sqrt{a^2 + b^2}", element, { throwOnError: false }); ``` #### `katex.renderToString(expression, options)` * **Description**: Generates an HTML string of the rendered math, suitable for server-side rendering or other uses where a DOM element is not directly available. * **Parameters**: * `expression` (string) - The LaTeX string to render. * `options` (object) - Optional configuration object for rendering. * **Returns**: A string containing the HTML representation of the rendered math. ### Request Example ```javascript var html = katex.renderToString("c = \\pm\\sqrt{a^2 + b^2}", { throwOnError: false }); // html will be '

...

' ``` ### Options Refer to the [API documentation](https://katex.org/docs/api.html), [options documentation](https://katex.org/docs/options.html), and [handling errors documentation](https://katex.org/docs/error.html) for a full list of available options, including `throwOnError`. ``` -------------------------------- ### Type Checking TypeScript Source: https://github.com/leanprover/verso/blob/main/static-web/search/README.txt Use this command to type check the TypeScript files for the project. ```bash tsc -p ./jsconfig.json ``` -------------------------------- ### Release HTML to Deployment Branch Source: https://github.com/leanprover/verso/blob/main/README.md This Python script places the generated HTML into the correct location on a new commit to the 'deploy' branch. ```python # deploy/release.py # Puts the generated HTML in the right place on a new commit on the 'deploy' branch. ``` -------------------------------- ### Fetch and Reset Git Branches Source: https://github.com/leanprover/verso/blob/main/README.md Commands to fetch the latest changes and reset local branches to match the upstream deploy and postdeploy branches. Ensure your working directory is clean before running. ```shell git fetch git checkout deploy git reset --hard remotes/upstream/deploy git checkout postdeploy git reset --hard remotes/upstream/postdeploy ``` -------------------------------- ### Render TeX to HTML String with KaTeX Source: https://github.com/leanprover/verso/blob/main/vendored-js/katex/README.md Utilize `katex.renderToString` to generate an HTML string representation of a TeX expression, suitable for server-side rendering. The `throwOnError: false` option is also available here. ```javascript var html = katex.renderToString("c = \pm\sqrt{a^2 + b^2}", { throwOnError: false }); // '

...

' ``` -------------------------------- ### Shared Utilities for Release Scripts Source: https://github.com/leanprover/verso/blob/main/README.md Contains shared utility functions for Python scripts, including version parsing, version comparison, and Git helpers. ```python # deploy/release_utils.py # Contains shared utilities used by both Python scripts (version parsing, version comparison, git helpers). ``` -------------------------------- ### Render TeX to DOM Element with KaTeX Source: https://github.com/leanprover/verso/blob/main/vendored-js/katex/README.md Use the `katex.render` function to directly render a TeX expression into a specified DOM element. The `throwOnError: false` option prevents errors from stopping rendering and displays invalid input as red TeX source. ```javascript katex.render("c = \pm\sqrt{a^2 + b^2}", element, { throwOnError: false }); ``` -------------------------------- ### CSS for Responsive Book Title Display Source: https://github.com/leanprover/verso/blob/main/README.md This CSS snippet moves the book title from the header to the table of contents when the screen width is 1200px or less. Adjust the `1200px` value to control the threshold. This CSS should be included in a served static file and added to the `extraCss` field in the `config` parameter of `manualMain`. ```css /* Move the title from the header to the toc when there is not enough room. */ @media screen and (max-width: 1200px) { .toc-title { display: block; } .header-title { display: none; } } ``` === COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.