From 06de6272d19eb7a34859ebea840f0f7eb8ae927a Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 28 Jul 2026 22:44:42 +0000 Subject: [PATCH 1/2] doc: mention precompileModules --- Manual/Runtime.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual/Runtime.lean b/Manual/Runtime.lean index 6119a189f..727d9fd52 100644 --- a/Manual/Runtime.lean +++ b/Manual/Runtime.lean @@ -524,6 +524,7 @@ The Lean interpreter can run Lean declarations for which symbols are available i To run this code (e.g. with {keywordOf Lean.Parser.Command.eval}`#eval`), the following steps are necessary: 1. The module containing the declaration and its dependencies must be compiled into a shared library 1. This shared library should be provided to `lean --load-dynlib=` to run code that imports the module. +The `precompileModules` {ref "lake-config"}[configuration option] instructs Lake to do the above automatically. It is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each {attr}`extern` declaration. Thus it is not possible to interpret an {attr}`extern` declaration in the same file. From 02a5580a4ff041f431063043e9bdc7ae80bc97c9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 29 Jul 2026 00:33:54 +0000 Subject: [PATCH 2/2] space --- Manual/Runtime.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual/Runtime.lean b/Manual/Runtime.lean index 727d9fd52..2ca10a1c8 100644 --- a/Manual/Runtime.lean +++ b/Manual/Runtime.lean @@ -524,6 +524,7 @@ The Lean interpreter can run Lean declarations for which symbols are available i To run this code (e.g. with {keywordOf Lean.Parser.Command.eval}`#eval`), the following steps are necessary: 1. The module containing the declaration and its dependencies must be compiled into a shared library 1. This shared library should be provided to `lean --load-dynlib=` to run code that imports the module. + The `precompileModules` {ref "lake-config"}[configuration option] instructs Lake to do the above automatically. It is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each {attr}`extern` declaration.