|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: David Thrane Christiansen |
| 5 | +-/ |
| 6 | +import Lean.DocString.Syntax |
| 7 | +import VersoManual |
| 8 | + |
| 9 | +open Verso Genre Manual |
| 10 | +open Verso.Doc |
| 11 | + |
| 12 | +#doc (Manual) "Development Server" => |
| 13 | +%%% |
| 14 | +tag := "serve" |
| 15 | +htmlSplit := .never |
| 16 | +%%% |
| 17 | + |
| 18 | +Verso includes a small HTTP server for previewing generated HTML on your own machine. |
| 19 | +Run it with `lake exe verso-serve`. |
| 20 | + |
| 21 | +The server is for *local development only*. |
| 22 | +It offers no HTTPS and no authentication. |
| 23 | +Do not use it to serve a real site. |
| 24 | + |
| 25 | +# Running the Server |
| 26 | +%%% |
| 27 | +tag := "serve-running" |
| 28 | +%%% |
| 29 | + |
| 30 | +:::paragraph |
| 31 | +The `verso-serve` command takes an optional port (8000 by default) and an optional directory (the current directory by default). |
| 32 | + |
| 33 | +``` |
| 34 | +$ lake exe serve --port 8000 _out/html |
| 35 | +``` |
| 36 | +::: |
| 37 | + |
| 38 | +If the requested port is already in use, the server scans the following ports for a free one and prints the port it settled on, so several servers started with default settings can run at once. |
| 39 | +Pass `--strict-port` to fail instead. |
| 40 | + |
| 41 | + |
| 42 | +# Command-Line Options |
| 43 | +%%% |
| 44 | +tag := "serve-options" |
| 45 | +%%% |
| 46 | + |
| 47 | +A single optional positional argument is accepted, which is the directory to be served at `/`. |
| 48 | +It defaults to the current directory unless {ref "serve-config"}[a configuration file] is provided. |
| 49 | +If the configuration file defines {ref "serve-mounts"}[mounts], then the positional argument is rejected. |
| 50 | +The following options are also accepted: |
| 51 | + |
| 52 | +: `--port PORT`, `-p PORT` |
| 53 | + |
| 54 | + The port to listen on. Defaults to `8000`. |
| 55 | + |
| 56 | +: `--strict-port` |
| 57 | + |
| 58 | + Fail if the port is in use instead of trying another. |
| 59 | + |
| 60 | +: `--config FILE` |
| 61 | + |
| 62 | + Load configuration from `FILE`. Defaults to `./verso-serve.toml` if it exists. |
| 63 | + If no configuration file is provided, the default values {ref "serve-config"}[for the configuration format] are used. |
| 64 | + |
| 65 | +: `--quiet` |
| 66 | + |
| 67 | + Suppress per-request logging. |
| 68 | + |
| 69 | +: `--verbose`, `-v` |
| 70 | + |
| 71 | + Log additional detail. |
| 72 | + |
| 73 | +: `--help`, `-h` |
| 74 | + |
| 75 | + Show usage and exit. |
| 76 | + |
| 77 | +Command-line options override values from the configuration file. |
| 78 | + |
| 79 | +# Configuration File |
| 80 | +%%% |
| 81 | +tag := "serve-config" |
| 82 | +%%% |
| 83 | + |
| 84 | +For anything beyond serving a single directory, place a `verso-serve.toml` file next to the project, or point at one with `--config`. |
| 85 | +Directories named in the configuration file are resolved relative to the configuration file itself. |
| 86 | +Every setting is optional, and an empty file behaves the same as no file. |
| 87 | + |
| 88 | +Every option is described here. |
| 89 | +The sections that follow add detail on mounts, redirects, and custom headers. |
| 90 | + |
| 91 | +: `port` |
| 92 | + |
| 93 | + The port to listen on. Must be a number from `1` to `65535`. Defaults to `8000`. If a port is also specified on the command line, the command-line option will be preferred. |
| 94 | + |
| 95 | +: `banner` |
| 96 | + |
| 97 | + A line shown in the command-line's startup banner to identify the project. Must be a string. No banner is shown by default. This can be helpful to distinguish between multiple Verso projects or to inform co-authors about relevant project-specific information. |
| 98 | + |
| 99 | +: `cors` |
| 100 | + |
| 101 | + Whether to send permissive cross-origin headers and answer `OPTIONS` preflight requests. Must be a boolean. Defaults to `false`. |
| 102 | + |
| 103 | +: `directory_listing` |
| 104 | + |
| 105 | + Whether to generate an HTML listing for a directory that has no `index.html`. Must be a boolean. Defaults to `true`. |
| 106 | + |
| 107 | +: `trailing_slash_redirect` |
| 108 | + |
| 109 | + Whether a request for a directory without a trailing slash is redirected to add one. Must be a boolean. Defaults to `true`. |
| 110 | + |
| 111 | +: `follow_symlinks_outside_root` |
| 112 | + |
| 113 | + Whether a symbolic link may resolve to a target outside every mounted directory. Must be a boolean. Defaults to `false`. |
| 114 | + |
| 115 | +: `[[mounts]]` |
| 116 | + |
| 117 | + Configures a mount, serving a directory at a URL prefix. The mount with the longest matching prefix wins. |
| 118 | + |
| 119 | + : `path` |
| 120 | + |
| 121 | + The URL prefix to serve at. Must be a string that begins with `/`. |
| 122 | + |
| 123 | + : `dir` |
| 124 | + |
| 125 | + The directory served under the prefix. Must be a string, resolved relative to the configuration file. |
| 126 | + |
| 127 | +: `[[redirects]]` |
| 128 | + |
| 129 | + Configures a redirect. Redirects are matched by their path prefix in order. The first match wins. |
| 130 | + |
| 131 | + : `from` |
| 132 | + |
| 133 | + The path prefix to match. Must be a string that begins with `/`. |
| 134 | + |
| 135 | + : `to` |
| 136 | + |
| 137 | + The location to redirect to. Must be a string. The path beneath the matched prefix is appended to it. |
| 138 | + |
| 139 | + : `status` |
| 140 | + |
| 141 | + The redirect status code. Must be one of `301`, `302`, `303`, `307`, or `308`. Defaults to `301`. |
| 142 | + |
| 143 | +: `[[headers]]` |
| 144 | + |
| 145 | + Configures a header rule, adding response headers to requests whose path begins with its prefix. |
| 146 | + |
| 147 | + : `path` |
| 148 | + |
| 149 | + The path prefix the rule applies to. Must be a string that begins with `/`. |
| 150 | + |
| 151 | + : `set` |
| 152 | + |
| 153 | + A table mapping header names to the values to set on matching responses. |
| 154 | + |
| 155 | +For example, this configuration serves a built site at `/` with the API reference mounted under `/api`, names the project in the banner, turns off directory listings, redirects an old entry point, and adds a header to everything: |
| 156 | + |
| 157 | +``` |
| 158 | +port = 4000 |
| 159 | +banner = "ACME Docs" |
| 160 | +directory_listing = false |
| 161 | + |
| 162 | +[[mounts]] |
| 163 | +path = "/" |
| 164 | +dir = "_out/html" |
| 165 | + |
| 166 | +[[mounts]] |
| 167 | +path = "/api" |
| 168 | +dir = "_out/api" |
| 169 | + |
| 170 | +[[redirects]] |
| 171 | +from = "/index.htm" |
| 172 | +to = "/" |
| 173 | + |
| 174 | +[[headers]] |
| 175 | +path = "/" |
| 176 | +set = { "X-Frame-Options" = "DENY" } |
| 177 | +``` |
| 178 | + |
| 179 | +## Mounts |
| 180 | +%%% |
| 181 | +tag := "serve-mounts" |
| 182 | +%%% |
| 183 | + |
| 184 | +A mount maps a URL prefix to a directory on disk. |
| 185 | +The mount whose prefix matches the most path segments wins, so more specific mounts override more general ones. |
| 186 | + |
| 187 | +``` |
| 188 | +[[mounts]] |
| 189 | +path = "/" |
| 190 | +dir = "_out/html" |
| 191 | + |
| 192 | +[[mounts]] |
| 193 | +path = "/foo" |
| 194 | +dir = "../foo-output" |
| 195 | + |
| 196 | +[[mounts]] |
| 197 | +path = "/foo/x" |
| 198 | +dir = "../special" |
| 199 | +``` |
| 200 | + |
| 201 | +With these mounts, `/foo/x/page.html` is served from `../special`, other paths under `/foo` from `../foo-output`, and everything else from `_out/html`. |
| 202 | +Two mounts may name the same directory. |
| 203 | +If a directory named by a mount does not exist, the server reports an error and exits rather than starting up in a broken state. |
| 204 | + |
| 205 | +:::paragraph |
| 206 | +The directory served at `/` is chosen in this order: |
| 207 | + 1. If a directory `DIR` is provided as a positional command-line parameter, then it is used. |
| 208 | + If the configuration file includes a mount for `/`, then it is replaced by `DIR`. |
| 209 | + 2. If no `DIR` is provided, then the `/` mount from the configuration file is served. |
| 210 | + 3. Otherwise, the current directory is served at `/`. |
| 211 | +::: |
| 212 | + |
| 213 | +## Redirects |
| 214 | +%%% |
| 215 | +tag := "serve-redirects" |
| 216 | +%%% |
| 217 | + |
| 218 | +Redirect rules are matched against the request path by prefix, in order, and the first match wins. |
| 219 | +The path beneath the matched prefix is appended to the target. |
| 220 | + |
| 221 | +``` |
| 222 | +[[redirects]] |
| 223 | +from = "/old" |
| 224 | +to = "/new" |
| 225 | +status = 301 |
| 226 | + |
| 227 | +[[redirects]] |
| 228 | +from = "/legacy" |
| 229 | +to = "/current" |
| 230 | +status = 302 |
| 231 | +``` |
| 232 | + |
| 233 | +## Custom Headers |
| 234 | +%%% |
| 235 | +tag := "serve-headers" |
| 236 | +%%% |
| 237 | + |
| 238 | +Header rules add response headers to requests whose path begins with a prefix. |
| 239 | +Later rules override earlier ones for the same header name. |
| 240 | + |
| 241 | +``` |
| 242 | +[[headers]] |
| 243 | +path = "/assets" |
| 244 | +set = { "Cache-Control" = "no-cache", "X-Frame-Options" = "DENY" } |
| 245 | +``` |
| 246 | + |
| 247 | +# Caching |
| 248 | +%%% |
| 249 | +tag := "serve-caching" |
| 250 | +%%% |
| 251 | + |
| 252 | +Every response carries `Cache-Control: no-cache`, which directs the browser to revalidate before reusing a cached copy rather than to skip caching entirely. |
| 253 | +Each file response also carries an `ETag` derived from the file's contents and a `Last-Modified` time. |
| 254 | + |
| 255 | +When a browser revalidates with `If-None-Match` or `If-Modified-Since` and the file is unchanged, the server replies `304 Not Modified` with no body. |
| 256 | +Because the `ETag` follows the contents, a rebuild that rewrites a file without changing it still will still be cheap to load. |
| 257 | + |
| 258 | +# Other Behavior |
| 259 | +%%% |
| 260 | +tag := "serve-behavior" |
| 261 | +%%% |
| 262 | + |
| 263 | + * A file's `Content-Type` comes from its extension. |
| 264 | + A file whose extension is unknown is served as `text/plain` when its contents are valid UTF-8 text, so text-like files open in the browser instead of downloading, and as `application/octet-stream` otherwise. |
| 265 | + * Directories are served by their `index.html` when one is present; otherwise a generated listing is shown unless listings are disabled, in which case the request is refused with `403 Forbidden`. |
| 266 | + * A request for a directory without a trailing slash is redirected to add one, so relative links resolve correctly. This can be turned off. |
| 267 | + * `Range` requests are supported, so media files can be sought and large files resumed. |
| 268 | + * Symbolic links are followed only while their target stays within a mounted directory. A link pointing outside every mount is refused, unless `follow_symlinks_outside_root` is set. |
| 269 | + * Only `GET` and `HEAD` are served. Other methods receive `405 Method Not Allowed`. With CORS enabled, `OPTIONS` preflight requests are answered. |
0 commit comments