`emit-typst`: Typst rendering backend, parallel to `emit-tex`

[michelk]

Verso already has a working LaTeX backend (emit-tex) built around three layers:

• Verso.Output.TeX — TeX AST (text, raw, command, environment, paragraphBreak, seq)
• Verso.Doc.TeX — TeXT rendering monad and GenreTeX typeclass (part/block/inline)
• VersoManual/TeX.lean — VersoManual's GenreTeX instance, plus VersoManual/TeX/Config.lean

The generated .tex file uses the memoir documentclass with a substantial preamble (~100 lines: sourcecodepro, fancyvrb, fvextra, tcolorbox, hyperref, custom \href override, unicode workarounds, …). CI already carries .github/actions/install-texlive to support this.

A Typst backend would follow the same three-layer structure with no preamble at all:

Verso.Output.Typst     — Typst content AST
Verso.Doc.Typst        — TypstT monad + GenreTypst typeclass
VersoManual/Typst.lean — VersoManual's GenreTypst instance

Why Typst rather than extending the TeX backend

	emit-tex (current)	emit-typst (proposed)
Runtime dependency	TeXLive (full install, GBs)	Single typst binary
Compilation speed	Seconds–minutes	~350 ms incremental
Preamble	~100 lines of package config	None
PDF/A, PDF/UA	Extra packages (pdfx, axessibility)	Built-in (set document(...))
Math	LaTeX math mode	Native Typst math
Verbatim	fancyvrb/fvextra + escape workarounds	``` fences, no escaping

The Verso.Output.TeX AST has command and environment as separate constructors because LaTeX needs them. Typst unifies these — everything is a content function call, so the AST can be simpler:

inductive Typst where
  | text   (s : String)
  | raw    (s : String)           -- pass-through markup
  | call   (name : String) (args : Array Typst) (body : Option Typst)
  | markup (sigil : String) (body : Typst)   -- *bold*, _italic_, = heading
  | seq    (contents : Array Typst)

Node mapping

Verso IR	emit-tex	emit-typst
Heading n	\section{...}	= ... / == ...
Bold	\textbf{...}	*...*
Code (inline)	\Verb|...| (fancyvrb)	`...`
Code block	Verbatim environment	```lang\n...\n```
Math (inline)	$...$	$...$
Math (block)	\[...\]	$ ... $
Link	\href{url}{text}	#link("url")[text]
Image	\includegraphics{...}	#image("...")
Cross-ref	\ref{label}	@label
Docstring block	\begin{tcolorbox}...	#block[...] or custom function

Scope

What would not change:

• The Doc IR, traversal, and resolve infrastructure (genre-agnostic)
• Lean code extraction and elaboration (happens during lake build, before rendering)
• {docstring}, {lean}, {name} extensions — these produce Doc nodes that both backends consume

What would be new:

• src/verso/Verso/Output/Typst.lean — the Typst AST and asString
• src/verso/Verso/Doc/Typst.lean — TypstT monad and GenreTypst typeclass
• src/verso-manual/VersoManual/Typst.lean — VersoManual's GenreTypst instance
• src/verso-manual/VersoManual/Typst/Config.lean — config (fonts, template path)
• Integration tests alongside the existing expected/tex/ directories
• CI: replace/supplement install-texlive with a typst download step

Tables and figures

Tables — a toTypst callback on an existing block_extension

VersoManual/Table.lean already registers Block.table as a block_extension with both toTeX and toHtml callbacks in one place. The toTeX callback emits a \begin{tabular}{ll...} environment; toHtml emits <table>. A toTypst callback would be a third entry in the same extension, keeping the backends symmetric:

-- existing (abbreviated)
block_extension Block.table (columns : Nat) (header : Bool) … where
  toTeX   := some <| fun _ goB _ data blocks => …   -- \begin{tabular}…\end{tabular}
  toHtml  := some <| fun _ goB id data blocks => …  -- <table>…</table>

  -- new
  toTypst := some <| fun _ goB _ data blocks =>
    open Verso.Output.Typst in do
    let (columns, header, _, _, align) ← deserialize data
    let rows ← …   -- same chunking logic as toTeX
    let cells ← rows.flatMapM (·.mapM goB)
    let colArg := mkColumnsArg columns align
    if header then
      let (hdr, body) := cells.splitAt columns
      pure <| call "table" #[colArg] (seq (#[call "table.header" #[] (seq hdr)] ++ body))
    else
      pure <| call "table" #[colArg] (seq cells)

Typst's #table is simpler than LaTeX's tabular: no column spec string for basic alignment, no & separators, no \\ row terminators. The current toTeX callback has a -- TODO: get this from align? comment on the column spec; the Typst backend would handle alignment cleanly via named arguments (align: left, align: center).

Cross-references already work: TableConfig stores an assignedTag : Option Tag. The Typst backend appends a label to the table block:

#figure(
  table(columns: 3, …),
  caption: [My table],
) <tbl-my-tag>

@tbl-my-tag in Verso source becomes @tbl-my-tag in Typst — the syntax is identical, so the cross-reference resolver needs no changes.

Figures — pre-rendered assets vs. Typst-native generation

There is currently no Block.figure extension in Verso. Two approaches are worth discussing; they differ in where figure content is produced.

Option A — pre-rendered assets (recommended)

The build pipeline generates SVG or PNG files before Typst runs. Verso embeds only the path and caption:

{figure path="figures/long-profile.svg" caption="Longitudinal profile, HQ100"}

The toTypst callback emits:

#figure(
  image("figures/long-profile.svg"),
  caption: [Longitudinal profile, HQ100],
) <fig-long-profile>

The toTeX callback would emit \begin{figure}\includegraphics{…}\caption{…}\end{figure}, and toHtml would emit <figure><img src="…"><figcaption>…</figcaption></figure>. All three backends consume the same pre-rendered asset — the format is backend-neutral. This is exactly how the toTeX backend handles figures today, so no new infrastructure is required.

Option B — Typst-native generation (CeTZ / Lilaq)

Verso could embed a Typst-native diagram block:

{typst-figure caption="Longitudinal profile"}
#cetz.canvas({ … })
{/typst-figure}

The toTypst callback emits the enclosed source verbatim as a #figure(…) body. The toHtml and toTeX callbacks have no equivalent, which breaks the multi-backend invariant that all block_extension callbacks are independently renderable. Appropriate only as a {typst-raw} escape hatch — explicitly backend-specific and not expected to round-trip to HTML or TeX.

Recommendation: Block.figure with path + caption + tag (Option A) as the standard figure extension.

Open questions

1. Is there interest in maintaining a GenreTypst instance for VersoManual, or would the first step be a lower-level emit-typst that genre authors implement themselves?
2. Should emit-typst call typst compile directly, or only emit the .typ file and let the user invoke Typst?
3. The typst Rust crate exposes a library API (typst-pdf) — is embedding it preferable to a subprocess call?
4. Should Block.figure be added to verso-manual now (independent of the Typst backend), since the toTeX backend would also benefit from it?