The Lurch command-line interface (CLI)

You can run this module from the command line via node cli.js (if you're in this folder, or with a different path if you're elsewhere), passing arguments as documented below. There are several use cases for this command-line interface.

NOTE: If you do not have Chromium installed so that the puppeteer module can find it, this CLI will not work. If you are using the development container for this repository as defined in its Dockerfile, Chromium is already installed for you.

Use case 1: Writing Lurch documents in Markdown

Some users prefer to write documents in Markdown, for (some subset of) the following reasons.

• They want to be able to edit the document in a text editor
• They type more quickly when they do not need to use menu items or dialog boxes to insert their content
• They want to check their source documents into version control in an easy, human-readable format

In addition, this command-line interface makes it easy to import one file into another as a dependency, which is a feature that (at the time this tool was invented, February 2024) has only partial support in the full Lurch web application. (One can embed dependencies, but cannot recursively refresh them when the dependencies change.) For that reason, this tool has some temporary benefits that the full Lurch app does not have.

To use the CLI in this way, just run it on a single input file, which can be a markdown file (ending in .md) or an HTML file (ending in .html) in either of two formats (simplified HTML or long-form HTML, described below).

node cli.js path/to/your-file.md

This mode will convert your file into standard Lurch form, load it into an invisible copy of the full Lurch web app running in a headless Chromium browser, validate the document, and then print to the console the results of that validation process, indented in a way that mimics the structure of nested environments in your document. Here is an example, without any of the colors that are used in the actual terminal output:

    rule:
        expression: `Assume A and B`
        expression: `A`
        expression: `B`
    expression: `Assume X and Y`
    expression: `Y`                       ✓ valid 
    expression: `Z`                       ? indeterminate 

Other output formats

If you do not want the output in this human-readable, simple, text form, you can ask for HTML output instead, which shows the long-form HTML that is stored in the actual Lurch app editor. Do so with the following command:

node cli.js --html path/to/your-file.md

This type of output is suitable for redirecting to an .html file that can then be opened by the main Lurch app. It will include the results of validation, but if you want the HTML without the validation results, use the --html-only switch instead of --html. For example, to redirect to an HTML file and exclude validation results, use the following form.

node cli.js --html-only path/to/your-file.md > output-file.html

If you would like to create a readable representation of the document for a non-technical audience, you can output to PDF. This mode of the CLI will automatically save the file into the same location as the input file, but with a .pdf extension. The PDF is just a direct capture of the Lurch app running in the headless Chromium, with your document loaded and validated.

node cli.js --pdf path/to/your-file.md

Simplified HTML vs. long-form HTML

Writing a Lurch document typically includes mathematical content like theorems, proofs, expressions, etc. In the main Lurch app, these are stored as complex HTML tags that are appropriate for rendering and editing by the Lurch app, but are not human-readable nor easy to create. To make it easier to create such content, we have the concept of "simplified HTML," which means that we provide simple HTML tags with common mathematical meanings, that can be programmatically converted on your behalf into the more complex format that the app uses internally.

Specifically, if you view the module supporting embedded copies of the Lurch app, its documentation describes how one can write tags of the form <lurch>...</lurch>, <latex>...</latex>, <theorem>...</theorem>, and others that represent meaningful mathematics in a compact way. Those tags are supported in both HTML and Markdown inputs to the CLI. Just as that documentation page describes support for the document header using a DIV of class "header," the CLI supports that as well.

That documentation also points out that, in Markdown input, the user can use inline Markdown code (surrounded in backticks) to represent expressions in Lurch notation, and can use inline LaTeX code (surrounded in dollar signs) to represent expository mathematics (that is, mathematics that is to be typeset and displayed, but not interpreted as part of the user's proof).

To see example Lurch documents written in Markdown using these conventions, refer to the source code for our documentation, which includes many tutorial pages with embedded copies of Lurch, each of which has its own document written in Markdown.

In addition to the features document on that page, the CLI also supports importing other documents into the one being processed by the CLI. Use an HTML tag of the form <import src="relative path"/> to do so. Imports can be recursive, and circular dependency chains generate errors. It is common to place such "import" tags in the document header, as described above, in a form that looks like the following.

<div class="header">
    <import src="path/to/some-import.md"/>
    <import src="path/to/another-import.md"/>
</div>

Use case 2: Validating existing Lurch documents

It is unlikely that the user will want to author documents in the long-form HTML format, because it is an internal storage format that is far less human-readable. But if the user already has a Lurch document saved from the app itself, and thus in the long-form HTML format, you can pass it to the CLI to have it validated.

node cli.js path/to/your-file.html

The output is the same as when Markdown input is given; it will be indented text output of the validation results. To instead see the output as HTML, so that you could use it to replace the original document, for example, use the --html switch mentioned earlier.

Use case 3: Validating an entire folder

If you run the command on a folder instead of a single file, the CLI will validate all the files in that folder, and print the results to the console. In this mode, you can use only the default output format (indented text, as shown above), which will be supplemented with a filename above each section of output. (The HTML output forms are typically for redirecting to a file, and thus do not make sense in this context.)

node cli.js path/to/your-folder

Use case 4: Watching for changes

If you run the command on a folder, you can pass the --watch switch to tell the CLI not to immediately process all the files in the folder, but to watch for changes to the folder itself. The CLI will respond whenever a file is added to the folder or when the contents of a file change; in each case, it will read the new or changed file and process it in the default way described above (printing validation results in text form, indented).

In this mode, the CLI does not exit until the user kills the process. It remains running so that you can use it to get constant, up-to-the-moment feedback on your recently saved edits. You can exit it with Ctrl+C, as with any CLI tool.

The --watch switch is not compatible with the --html or --html-only switches because their output is not human-readable, and the goal of the --watch switch is to provide a way for the user to edit a document and, each time they save, see the latest validation results. Thus the only output format that makes sense is the default one.

node cli.js --watch path/to/your-folder

Use case 5: Converting an entire folder

If you run the CLI on two folders, they are treated as a source and a destination folder. The CLI will convert all the files in the source folder to HTML, and write the results to the destination folder using the same filenames, but with each extension changed to .html. The output form is long-form HTML, meaning that it is ready to be opened in the main Lurch app.

node cli.js path/to/your-source-folder path/to/your-destination-folder

In this way, the user can write an entire library of mathematical documents with dependencies among one another in a single folder, in a convenient format like Markdown, and just occasionally compile them into the format used in the main Lurch app, for distribution to users of that app.

This module is supported by the headless Lurch module.