Manuals fail to render on Windows: `include_bin_dir` keys entries by a host-dependent path

[NicolasRouquette]

Repository: leanprover/verso
Version tested: tag v4.33.0 = 3bdedf29bada13d8103e6c979001c51dcee210c8
Still present on main (ac797d6adcb6ec06c0da7808abcfec90073d9fc5): binFiles and both call
sites are byte-identical to the tag. Only emitSearchBox has moved (681 → 710). Line numbers below
refer to main.
Toolchain: leanprover/lean4:v4.33.0
Platform: Windows 11, x86_64
Impact: Any Verso manual fails to render on Windows. Linux and macOS are unaffected.

Symptom

uncaught exception: no such file or directory (error code: 2)
  file: _out/blueprint\html-single\-verso-search\../../../static-web/search\domain-mappers.d.ts

The output directory is created and partially populated, then the run dies on the search assets.

The crux

include_bin_dir walks the directory as a System.FilePath, but keys each entry by that path's
toString — the path relative to the importing source file, complete with the build host's
separator. From that point on the value is a bare String, and every caller has to recover the
filename with dropPrefix against a hand-written literal duplicating the one in the call:

-- src/verso-search/VersoSearch/DomainSearch.lean:269-271
(include_bin_dir "../../../static-web/search").filterMap fun (name, contents) =>
  if name.endsWith "domain-mappers.js" then none
  else some (name.dropPrefix "../../../static-web/search/" |>.copy, contents)

Those keys are built in src/verso-util/VersoUtil/BinFiles.lean:41-49:

go (base path : System.FilePath) : StateT (Array _) IO Unit := do
  let here := base / path                     -- host-side read path: correct
  match (← here.metadata).type with
  | .dir =>
    for entry in (← here.readDir) do
      go base (path / entry.fileName)         -- this `/` ends up in the key
  | .file =>
    ...
    modify (·.push (path, e))                 -- `path` IS the key

path : FilePath and entry.fileName : String (a bare name — IO.FS.DirEntry keeps the directory
separately in root), so that / resolves to instance : HDiv FilePath String FilePath, i.e.
FilePath.join p ⟨sub⟩, which concatenates unconditionally:

def join (p sub : FilePath) : FilePath :=
  if sub.isAbsolute then sub
  else ⟨p.toString ++ pathSeparator.toString ++ sub.toString⟩

pathSeparator is '\\' on Windows. path is seeded from the call site's string literal — forward
slashes, as written in source — and each recursion appends one host separator; the elaborator
finally emits mkStrLit path.toString.

The observed key corroborates this: ../../../static-web/search\domain-mappers.d.ts is
forward-slashed throughout the portion contributed by the literal, with exactly one backslash,
immediately before the basename. static-web/search/ is flat, so the walk recurses once — one
join, one separator.

Two things then go wrong, and both follow from that choice of key:

1. The prefix comparison is separator-sensitive. The dropped literal ends in /; the key has
\ there. dropPrefix finds no match and returns the string unchanged, so the "filename" is the
entire source-relative path, and emitSearchBox throws writing
<out>/-verso-search/../../../static-web/search\domain-mappers.d.ts.

2. The key points outside the output directory. This is the more serious half: being
source-relative, it begins with ../../../. emitSearchBox
(src/verso-manual/VersoManual.lean:710) writes dir / file after only ensureDir dir, so the
failure is loud. Had it created parent directories first — as the KaTeX loop at
src/verso-manual/VersoManual/Html/Features.lean:98 does — Verso would have silently written its
search assets three levels above the requested output directory. The crash is the lucky outcome.

src/verso/Verso/Output/Html/KaTeX.lean:31-33 has the same shape and is latently affected: its
dropped prefix lies entirely within the literal portion, so it matches, and the key merely comes
out as katex/fonts\KaTeX_AMS-Regular.woff2 — not the katex/fonts/... the docstring promises,
but still writable, so the fonts land correctly today.

The docstring's contract does not hold on Windows either:

the strings are the filenames; the provided path is a prefix of all of them

Suggested fix: stay in System.FilePath

FilePath is already the right tool and is already in use for the traversal — the defect is
leaving it. Lean already models a path as a structured value, and gives both directions of the
conversion:

• mkFilePath : List String → FilePath builds a host path from a list of names;
• FilePath.components : FilePath → List String recovers the names, normalizing first
  (pathSeparators is ['\\', '/'] on Windows, so it folds mixed input).

The names are the platform-neutral datum. So key each entry by its names relative to the
included directory, and convert to a FilePath once, at the point where something actually
touches the disk:

private meta partial def binFiles (base root : System.FilePath) : IO (Array (List String × Expr)) :=
  (·.snd) <$> StateT.run (go []) #[]
where
  go (rel : List String) : StateT (Array _) IO Unit := do
    let here := rel.foldl (· / ·) (base / root)
    match (← here.metadata).type with
    | .dir =>
      for entry in (← here.readDir) do
        go (rel ++ [entry.fileName])
    | .file =>
      let contents ← IO.FS.readBinFile here
      let e : Expr := mkApp2 (.const ``Z85.decode []) (mkStrLit (Z85.encode contents)) (toExpr contents.size)
      modify (·.push (rel, e))
    | .symlink | .other => return ()

FilePath stays inside the elaborator, where it is joined against the real filesystem; the
components are what crosses into the artifact. (Note FilePath.join has no empty-path guard —
("" : FilePath) / "x" yields "\x" on Windows — which is why the accumulator is a component
list seeded with [] rather than an empty FilePath.)

Both call sites then lose their string surgery entirely — the key never becomes a string to begin
with, so there is nothing to concatenate or strip:

-- DomainSearch.lean
(include_bin_dir "../../../static-web/search").filter fun (name, _) =>
  name.getLast? != some "domain-mappers.js"

-- KaTeX.lean
(include_bin_dir "../../../../../vendored-js/katex/fonts").map fun (name, contents) =>
  ("katex" :: "fonts" :: name, contents)

and the consumers build a FilePath only where they write:

-- VersoManual.lean:710
for (name, contents) in searchBoxCode do
  IO.FS.writeBinFile (name.foldl (· / ·) dir) contents

Three things fall out of this:

• A key relative to the include root can never contain .., so the escape hazard above is
  impossible by construction rather than something emitSearchBox must guard against.
• No separator is ever baked into the compiled artifact. That matters beyond tidiness: .olean
  files are shared across platforms, so a key joined on the build host would carry \ into a
  Linux consumer.
• The endsWith filter becomes an exact match on the final name, where before a file called
  xdomain-mappers.js would also have been dropped.

The docstring should then read that keys are the entry's path components relative to the included
directory. This changes include_bin_dir's key type, but it is an internal utility and both
in-tree call sites are updated in the same change.