Fixup

Author: samuelburnham

Benchmarks/Compile/README.md

@@ -11,4 +11,4 @@ Runs the Ix compiler over the following libraries when imported:
 `lake exe compile-<lib>`, e.g. `compile-mathlib`
 
 > [!NOTE]
-> Compiling Mathlib and FLT, which depends on the former, requires a multi-core CPU and 128+ GB RAM.
+> Compiling Mathlib and FLT, which depends on the former, requires a multi-core CPU and 64+ GB RAM.

Benchmarks/CompileFC/Main.lean

@@ -1,4 +1,12 @@
 import FormalConjectures
 
 def main : IO Unit :=
-  IO.println s!"Formal Conjectures environment"
+  IO.println s!"Compiling Formal Conjectures environment"
+
+  let leanEnv ← get_env!
+
+  let start ← IO.monoMsNow
+  let phases ← Ix.CompileM.rsCompilePhases leanEnv
+  let elapsed := (← IO.monoMsNow) - start
+
+  IO.println s!"{phases.rawEnv.consts.size} consts, {phases.condensed.blocks.size} blocks, {phases.compileEnv.constCount} compiled in {elapsed}ms"

Benchmarks/CompileFC/flake.nix

@@ -31,8 +31,7 @@
         system,
         pkgs,
         ...
-      }: let
-      in {
+      }: {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
           inherit system;

Benchmarks/CompileFC/lakefile.toml

@@ -8,6 +8,7 @@ name = "CompileFC"
 [[lean_exe]]
 name = "compile-fc"
 root = "Main"
+supportInterpreter = true
 
 [[require]]
 name = "formal_conjectures"

Benchmarks/CompileFC/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.26.0