From 12fafde2d24c61e8b2d6ea11b058481b06af13a7 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 19 Aug 2026 18:09:01 +0000 Subject: [PATCH 1/4] feat: re-enable precompileModules --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index ade9bbab..b13eee02 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ require plausible from git "https://github.com/leanprover-community/plausible"@" require illuminate from git "https://github.com/leanprover/illuminate"@"main" package verso where - precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30 + precompileModules := true leanOptions := #[⟨`experimental.module, true⟩] @[default_target] From 54ebc2a7ed1f307fa75179e8ce44bcbb6514ec58 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 21 Aug 2026 18:07:33 +0000 Subject: [PATCH 2/4] fix: exe name --- doc/UsersGuide/Serve.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/UsersGuide/Serve.lean b/doc/UsersGuide/Serve.lean index c7acfd74..898cea29 100644 --- a/doc/UsersGuide/Serve.lean +++ b/doc/UsersGuide/Serve.lean @@ -31,7 +31,7 @@ tag := "serve-running" The `verso-serve` command takes an optional port (8000 by default) and an optional directory (the current directory by default). ``` -$ lake exe serve --port 8000 _out/html +$ lake exe verso-serve --port 8000 _out/html ``` ::: From ef36edfdd452a12adde87231e168a5a3129e49e6 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 21 Aug 2026 18:59:11 +0000 Subject: [PATCH 3/4] doc: note faster build strategy --- doc/UsersGuide/Elab.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean index 1954a42c..37cfac19 100644 --- a/doc/UsersGuide/Elab.lean +++ b/doc/UsersGuide/Elab.lean @@ -67,6 +67,15 @@ Each genre provides a `main` function that will carry out the remainder of the s Usually, this `main` function can be applied to the part that represents the whole document; however, genres that don't have a strict linear order (such as the {ref "website"}[website genre]) will provide their own means of configuring the document's layout. The `main` function typically also takes configuration parameters both in the code and on the command line, such as which output formats to generate or customizations to the generated output. +Tip: for projects with large dependencies such as mathlib, +compiling the document to a native executable can take a long time. +For faster rebuilds, +you can try running the `main` function through the Lean interpreter instead: +invoke `lake lean Main.lean --run Main.lean` in your shell, +where `Main.lean` is the file in which the genre `main` function is called +with your document as an argument. +Future updates to the Verso build process may make this the default. + # Traversal %%% tag := "traversal" From 6c2483eefb453d783ae858142a927bb4bd0bb8c9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com> Date: Mon, 24 Aug 2026 17:30:23 -0400 Subject: [PATCH 4/4] Update doc/UsersGuide/Elab.lean Co-authored-by: David Thrane Christiansen --- doc/UsersGuide/Elab.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean index 37cfac19..6a441af9 100644 --- a/doc/UsersGuide/Elab.lean +++ b/doc/UsersGuide/Elab.lean @@ -67,13 +67,9 @@ Each genre provides a `main` function that will carry out the remainder of the s Usually, this `main` function can be applied to the part that represents the whole document; however, genres that don't have a strict linear order (such as the {ref "website"}[website genre]) will provide their own means of configuring the document's layout. The `main` function typically also takes configuration parameters both in the code and on the command line, such as which output formats to generate or customizations to the generated output. -Tip: for projects with large dependencies such as mathlib, -compiling the document to a native executable can take a long time. -For faster rebuilds, -you can try running the `main` function through the Lean interpreter instead: -invoke `lake lean Main.lean --run Main.lean` in your shell, -where `Main.lean` is the file in which the genre `main` function is called -with your document as an argument. +Tip: for projects with large dependencies such as Mathlib, compiling the document to a native executable can take a long time. +It is often faster to run the `main` function through the Lean interpreter instead. +To do so, invoke `lake lean Main.lean --run Main.lean` in your shell, where `Main.lean` is the file in which the genre's `main` function is called with your document as an argument. Future updates to the Verso build process may make this the default. # Traversal