From 9dc4dbebe136522a6226a0a4ff6552526cbce3bb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Jul 2025 18:12:44 +0200 Subject: [PATCH] perf: do not try to mmap `.ir` to the same address as `.olean` (#9488) --- src/Lean/Environment.lean | 3 ++- stage0/src/stdlib_flags.h | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 8d9e13e204..9efd3d461e 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1778,7 +1778,8 @@ def writeModule (env : Environment) (fname : System.FilePath) : IO Unit := do (← mkPart .exported), (← mkPart .server), (← mkPart .private)] - saveModuleData (fname.withExtension "ir") env.mainModule (mkIRData env) + -- Make sure to change the module name so we derive a different base address + saveModuleData (fname.withExtension "ir") (env.mainModule ++ `ir) (mkIRData env) else saveModuleData fname env.mainModule (← mkModuleData env) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..0b833d9dc4 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// Dear CI, please update stage0 + namespace lean { options get_default_options() { options opts;