diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean
index 1954a42c..6a441af9 100644
--- a/doc/UsersGuide/Elab.lean
+++ b/doc/UsersGuide/Elab.lean
@@ -67,6 +67,11 @@ 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.
+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
 %%%
 tag := "traversal"
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
 ```
 :::
 
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]