feat: lightweight HTTP server for Verso projects by david-christiansen · Pull Request #876 · leanprover/verso

david-christiansen · 2026-06-15T14:18:09Z

Adds a lightweight HTTP server for previewing generated Verso HTML locally, run with lake exe serve. The server binds only 127.0.0.1, reducing the temptation to deploy it to production.

This replaces Python or Node local servers, with defaults that are better-suited to hosting Verso correctly. It also doesn't rely on users having any other programming language ecosystem available.

It can be configured from the command line, or for slightly more complex setups, via serve.toml.

Along the way, this branch encountered a bug in the TeX code generation that needed fixing in order to render the docs for the feature.

This replaces Python or Node local servers, with defaults that are better-suited to hosting Verso correctly. It also doesn't rely on users having any other programming language ecosystem available.

@david-christiansen

…r#900) In writing leanprover#876, @david-christiansen noted "this branch encountered a bug in the TeX code generation that needed fixing" — but I think the issue was slightly misdiagnosed, it wasn't a fragility issue, a `]` anywhere in an item description (including outside of verbatim) caused a rendering issue because it was read as the description closer. This fix fixes the bug from leanprover#876, also fixes bugs for `]` in literal text, and adds a test for the behavior.

robsimmons · 2026-07-31T15:04:21Z

-You can preview the resulting files by running
-`python3 -m http.server 8000 -d html` and pointing a web browser to
-http://localhost:8000/
+You can preview the resulting files by running `lake exe serve html`


Let's do lake exe verso-serve for this. (Todo for me: do the cli arguments to verso-serve make sense?)

(Check that no-args serves .)

robsimmons

Some documentation comments (which imply some code changes too, especially around removing command-line options to avoid duplication). I'm still not sure every configuration option makes sense for a development-only and/or verso-specific server, but that may be a failure of imagination — and these defaults seem reasonable.

robsimmons · 2026-08-01T02:12:57Z

+%%%
+
+Verso includes a small HTTP server for previewing generated HTML on your own machine.
+Run it with `lake exe serve`.


Change to verso-serve throughout.

robsimmons · 2026-08-01T02:15:06Z

+: `DIR`
+
+  The directory served at `/`, relative to the current directory. Defaults to the current directory.
+


This is confusing without a USAGE-style line that explains that DIR is a positional argument. Maybe just start "in addition to the directory served, which is given as a positional argument, the following arguments are supported:

I think the new text addresses this

robsimmons · 2026-08-01T02:22:34Z

+
+: `--config FILE`
+
+  Load configuration from `FILE`. Defaults to `./serve.toml` if it exists.


Suggested change

Load configuration from `FILE`. Defaults to `./serve.toml` if it exists.

Load configuration from `FILE`. Defaults to `./serve.toml` if it exists. Otherwise uses defaults (see {ref "serve-config"}[Configuration file specification]).

I went with a somewhat more verbose (and grammatical) alternative.

robsimmons · 2026-08-01T02:27:51Z

+tag := "serve-config"
+%%%
+
+For anything beyond serving a single directory, place a `serve.toml` file next to the project, or point at one with `--config`.


"Next to the project" assumes verso-serve is being invoked in the folder with lakefile.toml, which isn't necessarily the case.

Suggested change

For anything beyond serving a single directory, place a `serve.toml` file next to the project, or point at one with `--config`.

For anything beyond serving a single directory, create a `serve.toml` file. When `verso-serve` is invoked, it will look for `serve.toml` in the current working directory unless another location is specified with the `--config` {ref "serve-options"}[command line option].

lake exe only works from the project root, so I think this is actually the right way to do things.

robsimmons · 2026-08-01T02:40:35Z

+:::paragraph
+As requests arrive, each is logged with the active port, the method, the path, and the response status:
+
+```
+[8000] GET /index.html 200
+[8000] GET /missing 404
+```
+:::
+


I think this would read better without this section — it's behavior description that will be either obvious to the user or still confusing with this explanation; it would be better to get on to the command-line options.

Agreed - it's gone.

robsimmons

mostly comments on the docs / spec, i didn't review tests but the Config/Mime/Static/VersoServeMain quartet looks okay modulo questions about docs/spec.

robsimmons · 2026-08-04T13:58:51Z

+: `banner`
+
+  A line shown in the startup banner to identify the project. Must be a string. No banner is shown by default.


This feels like a pretty high documentation-noise to user-value-signal ratio. Was there a use case for a configurable command-line banner you had in mind?

From conversation with @robsimmons: "banner" was initially understood as HTML injection rather than command-line dump. Be more specific here.

robsimmons · 2026-08-04T17:23:41Z

+Scalar flags override the corresponding config values. A positional directory replaces the `/`
+mount. If no `/` mount remains, a default one serving the current directory is added, so `/` is
+always mapped.
+-/


The mount-juggling is strange in a function called withCli, and I think if there are any mounts in the config file then lake exe verso-serve should not auto-mount the root directory — and possibly should reject a positional argument altogether. The port winning on the CLI makes sense, but the mount isn't anywhere near so obvious to me.

If the ServeConfig/CliArgs overlap is limited to mounts and ports this could probably be inlined.

The positional argument is now rejected when mounts are configured

robsimmons · 2026-08-04T17:30:06Z

-You can preview the resulting files by running
-`python3 -m http.server 8000 -d html` and pointing a web browser to
-http://localhost:8000/
+You can preview the resulting files by running `lake exe serve html`


…edirect

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

# Conflicts: # test-projects/literate-config/lake-manifest.json # test-projects/literate-multi-root/lake-manifest.json

david-christiansen added 15 commits June 15, 2026 16:16

feat: lightweight HTTP server for Verso projects

b19b3ab

This replaces Python or Node local servers, with defaults that are better-suited to hosting Verso correctly. It also doesn't rely on users having any other programming language ecosystem available.

fix: fragile rendering in description lists for TeX

f2542aa

consistent section pluralization in config for server

b0e49fe

improvements

b05dd49

fix symlink index bug

618470a

Merge remote-tracking branch 'upstream/main' into serve

ddf440c

release notes

558ba35

small fixes

4a973fc

fix: path separators

86865f1

cleanup

a38dbbc

range cleanup

4e83d8f

config and path handling fixes

dbfeca9

fix: validate redirect better

820bd05

small cleanups and test coverage improvements

f698f98

feat: sniff content type from bytes

d56ecdd

david-christiansen requested a review from robsimmons June 16, 2026 07:51

robsimmons mentioned this pull request Jun 29, 2026

fix: add braces to item description to avoid errors on ] #900

Merged

robsimmons added 2 commits July 3, 2026 15:58

Merge branch 'main' into serve

6903bb9

adapt to merge

35c258e

robsimmons reviewed Jul 31, 2026

View reviewed changes

robsimmons requested changes Aug 1, 2026

View reviewed changes

robsimmons reviewed Aug 1, 2026

View reviewed changes

robsimmons requested changes Aug 4, 2026

View reviewed changes

david-christiansen and others added 6 commits August 7, 2026 16:32

rename serve to verso-serve

9416740

Config file name and defaults doc

1bd7ba9

Remove command-line flags --cors, --no-listing, --no-trailing-slash-r…

133c4e6

…edirect

fix test

e067001

Update doc/UsersGuide/Serve.lean

5254c50

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

Update doc/UsersGuide/Serve.lean

d578bd9

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

david-christiansen and others added 5 commits August 7, 2026 16:43

Clarify banner docs

e90042f

clarify positional arg

45cf63a

Update doc/UsersGuide/Serve.lean

37dd12b

Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>

Merge remote-tracking branch 'origin/main' into serve

17e965a

# Conflicts: # test-projects/literate-config/lake-manifest.json # test-projects/literate-multi-root/lake-manifest.json

it is now an error to have a root dir and mounts

e4b21e8

david-christiansen force-pushed the serve branch from a9a6299 to e4b21e8 Compare August 7, 2026 15:01

david-christiansen and others added 3 commits August 7, 2026 17:03

document rejection

7894096

delete useless para

66016b4

prettier fix, serve -> verso-serve in tests

a5dcaf3

robsimmons approved these changes Aug 7, 2026

View reviewed changes

robsimmons added this pull request to the merge queue Aug 7, 2026

Merged via the queue into main with commit 4ac0364 Aug 7, 2026
11 checks passed

robsimmons deleted the serve branch August 7, 2026 19:02

		: `DIR`

		The directory served at `/`, relative to the current directory. Defaults to the current directory.


		: `--config FILE`

		Load configuration from `FILE`. Defaults to `./serve.toml` if it exists.

	For anything beyond serving a single directory, place a `serve.toml` file next to the project, or point at one with `--config`.
	For anything beyond serving a single directory, create a `serve.toml` file. When `verso-serve` is invoked, it will look for `serve.toml` in the current working directory unless another location is specified with the `--config` {ref "serve-options"}[command line option].

		: `banner`

		A line shown in the startup banner to identify the project. Must be a string. No banner is shown by default.

Uh oh!

Conversation

david-christiansen commented Jun 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons Jul 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robsimmons left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robsimmons Aug 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robsimmons left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

david-christiansen commented Jun 15, 2026 •

edited

Loading

robsimmons Jul 31, 2026 •

edited

Loading

robsimmons Aug 1, 2026 •

edited

Loading