From 45f10cd19f71cc438a5967fd28548d479ab30da3 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 10 Feb 2026 18:08:51 -0500
Subject: [PATCH 01/21] feat: Add `ix compile` CLI and CI benchmarks

---
 .github/workflows/compile.yml                |  28 ++++
 .gitignore                                   |   2 +-
 Benchmarks/Compile/Compile.lean              |  13 ++
 Benchmarks/Compile/CompileFLT.lean           |   5 +
 Benchmarks/Compile/CompileLean.lean          |   4 +
 Benchmarks/Compile/CompileMathlib.lean       |   4 +
 Benchmarks/Compile/README.md                 |  14 ++
 Benchmarks/Compile/lake-manifest.json        | 142 +++++++++++++++++++
 Benchmarks/Compile/lakefile.lean             |  28 ++++
 Benchmarks/Compile/lean-toolchain            |   1 +
 Benchmarks/CompileFC/Main.lean               |   4 +
 Benchmarks/CompileFC/README.md               |  11 ++
 Benchmarks/CompileFC/flake.lock              | 117 +++++++++++++++
 Benchmarks/CompileFC/flake.nix               |  54 +++++++
 Benchmarks/CompileFC/lake-manifest.json      | 105 ++++++++++++++
 Benchmarks/CompileFC/lakefile.toml           |  19 +++
 Benchmarks/CompileFC/lean-toolchain          |   1 +
 Ix/Cli/CompileCmd.lean                       |  29 ++++
 Ix/Meta.lean                                 |  18 +--
 Main.lean                                    |   2 +
 ix_test/.github/workflows/lean_action_ci.yml |  14 --
 ix_test/lean-toolchain                       |   2 +-
 22 files changed, 590 insertions(+), 27 deletions(-)
 create mode 100644 .github/workflows/compile.yml
 create mode 100644 Benchmarks/Compile/Compile.lean
 create mode 100644 Benchmarks/Compile/CompileFLT.lean
 create mode 100644 Benchmarks/Compile/CompileLean.lean
 create mode 100644 Benchmarks/Compile/CompileMathlib.lean
 create mode 100644 Benchmarks/Compile/README.md
 create mode 100644 Benchmarks/Compile/lake-manifest.json
 create mode 100644 Benchmarks/Compile/lakefile.lean
 create mode 100644 Benchmarks/Compile/lean-toolchain
 create mode 100644 Benchmarks/CompileFC/Main.lean
 create mode 100644 Benchmarks/CompileFC/README.md
 create mode 100644 Benchmarks/CompileFC/flake.lock
 create mode 100644 Benchmarks/CompileFC/flake.nix
 create mode 100644 Benchmarks/CompileFC/lake-manifest.json
 create mode 100644 Benchmarks/CompileFC/lakefile.toml
 create mode 100644 Benchmarks/CompileFC/lean-toolchain
 create mode 100644 Ix/Cli/CompileCmd.lean
 delete mode 100644 ix_test/.github/workflows/lean_action_ci.yml

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
new file mode 100644
index 00000000..08b062a1
--- /dev/null
+++ b/.github/workflows/compile.yml
@@ -0,0 +1,28 @@
+name: Benchmark Ix compiler
+
+on:
+  push:
+    branches: "sb/cli"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  run-compiler:
+    strategy:
+      matrix:
+        bench: [lean, mathlib, flt]
+    runs-on: warp-ubuntu-latest-x64-32x
+    steps:
+      - uses: actions/checkout@v6
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "--wfail -v"
+          lake-package-directory: "Benchmarks/Compile"
+      - working-directory: Benchmarks/Compile
+        run: lake exe compile-${{ matrix.bench }}
diff --git a/.gitignore b/.gitignore
index 3ec5f26a..79c70512 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
 # Lean
-/.lake
+**/.lake
 
 # Rust
 /target
diff --git a/Benchmarks/Compile/Compile.lean b/Benchmarks/Compile/Compile.lean
new file mode 100644
index 00000000..6cea9317
--- /dev/null
+++ b/Benchmarks/Compile/Compile.lean
@@ -0,0 +1,13 @@
+import Ix.CompileM
+import Ix.Meta
+
+def compile (name : String) : IO Unit := do
+  println! "Compiling {name} 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"
diff --git a/Benchmarks/Compile/CompileFLT.lean b/Benchmarks/Compile/CompileFLT.lean
new file mode 100644
index 00000000..535b9256
--- /dev/null
+++ b/Benchmarks/Compile/CompileFLT.lean
@@ -0,0 +1,5 @@
+import Compile
+import FLT
+
+def main : IO Unit := compile "FLT"
+
diff --git a/Benchmarks/Compile/CompileLean.lean b/Benchmarks/Compile/CompileLean.lean
new file mode 100644
index 00000000..eaaf3cfa
--- /dev/null
+++ b/Benchmarks/Compile/CompileLean.lean
@@ -0,0 +1,4 @@
+import Compile
+import Lean
+
+def main : IO Unit := compile "Lean"
diff --git a/Benchmarks/Compile/CompileMathlib.lean b/Benchmarks/Compile/CompileMathlib.lean
new file mode 100644
index 00000000..ec9f9feb
--- /dev/null
+++ b/Benchmarks/Compile/CompileMathlib.lean
@@ -0,0 +1,4 @@
+import Compile
+import Mathlib
+
+def main : IO Unit := compile "Mathlib"
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
new file mode 100644
index 00000000..c7fb6787
--- /dev/null
+++ b/Benchmarks/Compile/README.md
@@ -0,0 +1,14 @@
+# Compile
+
+Runs the Ix compiler over the following libraries when imported:
+
+- [Lean4](https://github.com/leanprover/lean4)
+- [Mathlib](https://github.com/leanprover-community/mathlib4)
+- [FLT project](https://github.com/ImperialCollegeLondon/FLT)
+
+## Usage
+
+`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.
diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json
new file mode 100644
index 00000000..edf0a98e
--- /dev/null
+++ b/Benchmarks/Compile/lake-manifest.json
@@ -0,0 +1,142 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/ImperialCollegeLondon/FLT",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5d2db3af80b5260ae7d64ba4daf2b7768a9a95b7",
+   "name": "flt",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "ix",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../..",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.83",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/Blake3.lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
+   "name": "Blake3",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "Compile",
+ "lakeDir": ".lake"}
diff --git a/Benchmarks/Compile/lakefile.lean b/Benchmarks/Compile/lakefile.lean
new file mode 100644
index 00000000..73bc9e49
--- /dev/null
+++ b/Benchmarks/Compile/lakefile.lean
@@ -0,0 +1,28 @@
+import Lake
+open Lake DSL
+
+package "Compile" where
+  version := v!"0.1.0"
+
+@[default_target]
+lean_lib Compile
+
+lean_exe "compile-lean" where
+  root := `CompileLean
+  supportInterpreter := true
+
+lean_exe "compile-mathlib" where
+  root := `CompileMathlib
+  supportInterpreter := true
+
+lean_exe "compile-flt" where
+  root := `CompileFLT
+  supportInterpreter := true
+
+require ix from "../.."
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4" @ "v4.26.0"
+
+require flt from git
+  "https://github.com/ImperialCollegeLondon/FLT" @ "v4.26.0"
diff --git a/Benchmarks/Compile/lean-toolchain b/Benchmarks/Compile/lean-toolchain
new file mode 100644
index 00000000..e59446d5
--- /dev/null
+++ b/Benchmarks/Compile/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.26.0
diff --git a/Benchmarks/CompileFC/Main.lean b/Benchmarks/CompileFC/Main.lean
new file mode 100644
index 00000000..efcf2ad0
--- /dev/null
+++ b/Benchmarks/CompileFC/Main.lean
@@ -0,0 +1,4 @@
+import FormalConjectures
+
+def main : IO Unit :=
+  IO.println s!"Formal Conjectures environment"
diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md
new file mode 100644
index 00000000..6f3d90df
--- /dev/null
+++ b/Benchmarks/CompileFC/README.md
@@ -0,0 +1,11 @@
+# CompileFC
+
+WIP: Doesn't build with lean4-nix v4.22.0 with the lake dev shell due to changes in `.lake` behavior
+
+Runs the Ix compiler over the Lean environment of https://github.com/google-deepmind/formal-conjectures.
+
+Uses Lean v4.22.0 to match the formal-conjectures project, hence the separate project.
+
+## Usage
+
+`lake exe compile-fc`
diff --git a/Benchmarks/CompileFC/flake.lock b/Benchmarks/CompileFC/flake.lock
new file mode 100644
index 00000000..e2d0ab18
--- /dev/null
+++ b/Benchmarks/CompileFC/flake.lock
@@ -0,0 +1,117 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1769996383,
+        "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "57928607ea566b5db3ad13af0e57e921e6b12381",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-parts_2": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib_2"
+      },
+      "locked": {
+        "lastModified": 1765835352,
+        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "lean4-nix": {
+      "inputs": {
+        "flake-parts": "flake-parts_2",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1770601541,
+        "narHash": "sha256-wCun5wynV3vLoVrr9gU46qI0UG4YeID6IKhPIhtsp8U=",
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "rev": "561f1a779737e109d4e03a6f967108497bbbd73f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1765779637,
+        "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "lastModified": 1769909678,
+        "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "72716169fe93074c333e8d0173151350670b824c",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib_2": {
+      "locked": {
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "lean4-nix": "lean4-nix",
+        "nixpkgs": [
+          "lean4-nix",
+          "nixpkgs"
+        ]
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/Benchmarks/CompileFC/flake.nix b/Benchmarks/CompileFC/flake.nix
new file mode 100644
index 00000000..c6d95b0e
--- /dev/null
+++ b/Benchmarks/CompileFC/flake.nix
@@ -0,0 +1,54 @@
+{
+  description = "Ix Nix flake (Lean4 + C + Rust)";
+
+  inputs = {
+    # System packages, follows lean4-nix so we stay in sync
+    nixpkgs.follows = "lean4-nix/nixpkgs";
+
+    # Lean 4 & Lake
+    lean4-nix.url = "github:lenianiva/lean4-nix";
+
+    # Helper: flake-parts for easier outputs
+    flake-parts.url = "github:hercules-ci/flake-parts";
+  };
+
+  outputs = inputs @ {
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      # Systems we want to build for
+      systems = [
+        "aarch64-darwin"
+        "aarch64-linux"
+        "x86_64-darwin"
+        "x86_64-linux"
+      ];
+
+      perSystem = {
+        system,
+        pkgs,
+        ...
+      }: let
+      in {
+        # Lean overlay
+        _module.args.pkgs = import nixpkgs {
+          inherit system;
+          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+        };
+        # Provide a unified dev shell with Lean + Rust
+        devShells.default = pkgs.mkShell {
+          packages = with pkgs; [
+            pkg-config
+            openssl
+            clang
+            lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
+          ];
+        };
+
+        formatter = pkgs.alejandra;
+      };
+    };
+}
diff --git a/Benchmarks/CompileFC/lake-manifest.json b/Benchmarks/CompileFC/lake-manifest.json
new file mode 100644
index 00000000..a084d624
--- /dev/null
+++ b/Benchmarks/CompileFC/lake-manifest.json
@@ -0,0 +1,105 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/google-deepmind/formal-conjectures",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "20af7726bba72fc97d8feda6958a8afacc664ad4",
+   "name": "formal_conjectures",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "20af7726bba72fc97d8feda6958a8afacc664ad4",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.68",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "CompileFC",
+ "lakeDir": ".lake"}
diff --git a/Benchmarks/CompileFC/lakefile.toml b/Benchmarks/CompileFC/lakefile.toml
new file mode 100644
index 00000000..edafd12d
--- /dev/null
+++ b/Benchmarks/CompileFC/lakefile.toml
@@ -0,0 +1,19 @@
+name = "CompileFC"
+version = "0.1.0"
+defaultTargets = ["compile-fc"]
+
+[[lean_lib]]
+name = "CompileFC"
+
+[[lean_exe]]
+name = "compile-fc"
+root = "Main"
+
+[[require]]
+name = "formal_conjectures"
+git = "https://github.com/google-deepmind/formal-conjectures"
+rev = "20af7726bba72fc97d8feda6958a8afacc664ad4"
+
+[[require]]
+name = "ix"
+path = "../.."
diff --git a/Benchmarks/CompileFC/lean-toolchain b/Benchmarks/CompileFC/lean-toolchain
new file mode 100644
index 00000000..6ac6d4c4
--- /dev/null
+++ b/Benchmarks/CompileFC/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.22.0
diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
new file mode 100644
index 00000000..37eb14e2
--- /dev/null
+++ b/Ix/Cli/CompileCmd.lean
@@ -0,0 +1,29 @@
+import Cli
+import Ix.Common
+import Ix.CompileM
+import Ix.Meta
+import Lean
+
+def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
+  let some path := p.flag? "path"
+    | p.printError "error: must specify --path"
+      return 1
+  let leanEnv ← getFileEnv <| path.as! String
+
+  IO.println s!"Running Ix compiler"
+
+  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"
+  return 0
+    
+
+def compileCmd : Cli.Cmd := `[Cli|
+  compile VIA runCompileCmd;
+  "Compile Lean file to Ixon"
+
+  FLAGS:
+    path : String; "Path to file to compile"
+]
diff --git a/Ix/Meta.lean b/Ix/Meta.lean
index ad1afc09..3ad07882 100644
--- a/Ix/Meta.lean
+++ b/Ix/Meta.lean
@@ -8,27 +8,23 @@ open System (FilePath)
 
 open Elab in
 def getFileEnv (path : FilePath) : IO Environment := do
+  let path ← IO.FS.realPath path
   let out ← IO.Process.output {
     cmd := "lake"
-    args := #["setup-file", path.toString]
+    args := #["env", "printenv", "LEAN_PATH"]
+    cwd := path.parent
   }
-  let split := out.stdout.splitOn "\"oleanPath\":[" |>.getD 1 ""
-  let split := split.splitOn "],\"loadDynlibPaths\":[" |>.getD 0 ""
-  let paths := split.replace "\"" "" |>.splitOn ","|>.map FilePath.mk
+  let paths := out.stdout.trim.splitOn ":" |>.map FilePath.mk
   initSearchPath (← findSysroot) paths
 
   let source ← IO.FS.readFile path
   let inputCtx := Parser.mkInputContext source path.toString
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, messages) ← processHeader header default messages inputCtx 0
-  let env := env.setMainModule default
-  let commandState := Command.mkState env messages default
-  let stt ← IO.processCommands inputCtx parserState commandState
-  let msgs := stt.commandState.messages
-  if msgs.hasErrors then
+  if messages.hasErrors then
     throw $ IO.userError $ "\n\n".intercalate $
-      (← msgs.toList.mapM (·.toString)).map String.trim
-  else return stt.commandState.env
+      (← messages.toList.mapM (·.toString)).map String.trim
+  return env
 
 elab "this_file!" : term => do
   let ctx ← readThe Core.Context
diff --git a/Main.lean b/Main.lean
index 825d5d80..3d111f56 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,5 +1,6 @@
 --import Ix.Cli.ProveCmd
 --import Ix.Cli.StoreCmd
+import Ix.Cli.CompileCmd
 import Ix.Cli.ServeCmd
 import Ix.Cli.ConnectCmd
 import Ix
@@ -14,6 +15,7 @@ def ixCmd : Cli.Cmd := `[Cli|
   SUBCOMMANDS:
     --proveCmd;
     --storeCmd;
+    compileCmd;
     serveCmd;
     connectCmd
 ]
diff --git a/ix_test/.github/workflows/lean_action_ci.yml b/ix_test/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index 09cd4ca6..00000000
--- a/ix_test/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v4
-      - uses: leanprover/lean-action@v1
diff --git a/ix_test/lean-toolchain b/ix_test/lean-toolchain
index f434439d..4a5353be 100644
--- a/ix_test/lean-toolchain
+++ b/ix_test/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.23.0
+leanprover/lean4:4.26.0

From 666bf91045535b5d71b03e8016d1bacdbd52c6e3 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 10 Feb 2026 18:26:38 -0500
Subject: [PATCH 02/21] Fixup

---
 Benchmarks/Compile/README.md        |  2 +-
 Benchmarks/CompileFC/Main.lean      | 10 +++++++++-
 Benchmarks/CompileFC/flake.nix      |  3 +--
 Benchmarks/CompileFC/lakefile.toml  |  1 +
 Benchmarks/CompileFC/lean-toolchain |  2 +-
 5 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
index c7fb6787..535ca04f 100644
--- a/Benchmarks/Compile/README.md
+++ b/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.
diff --git a/Benchmarks/CompileFC/Main.lean b/Benchmarks/CompileFC/Main.lean
index efcf2ad0..19a5d29e 100644
--- a/Benchmarks/CompileFC/Main.lean
+++ b/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"
diff --git a/Benchmarks/CompileFC/flake.nix b/Benchmarks/CompileFC/flake.nix
index c6d95b0e..57b04053 100644
--- a/Benchmarks/CompileFC/flake.nix
+++ b/Benchmarks/CompileFC/flake.nix
@@ -31,8 +31,7 @@
         system,
         pkgs,
         ...
-      }: let
-      in {
+      }: {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
           inherit system;
diff --git a/Benchmarks/CompileFC/lakefile.toml b/Benchmarks/CompileFC/lakefile.toml
index edafd12d..4af65631 100644
--- a/Benchmarks/CompileFC/lakefile.toml
+++ b/Benchmarks/CompileFC/lakefile.toml
@@ -8,6 +8,7 @@ name = "CompileFC"
 [[lean_exe]]
 name = "compile-fc"
 root = "Main"
+supportInterpreter = true
 
 [[require]]
 name = "formal_conjectures"
diff --git a/Benchmarks/CompileFC/lean-toolchain b/Benchmarks/CompileFC/lean-toolchain
index 6ac6d4c4..2654c20b 100644
--- a/Benchmarks/CompileFC/lean-toolchain
+++ b/Benchmarks/CompileFC/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.26.0
\ No newline at end of file

From 50c8f60ae7e462c693681e351e62b2d73002601b Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 10 Feb 2026 22:39:15 -0500
Subject: [PATCH 03/21] Fix env

---
 .github/workflows/compile.yml   |  4 +++-
 Benchmarks/Compile/Compile.lean | 23 ++++++++++++++++++++---
 Cargo.lock                      | 12 ++++++------
 Ix/Cli/CompileCmd.lean          |  6 ++++--
 Tests/Cli.lean                  |  4 ++--
 flake.nix                       |  1 +
 6 files changed, 36 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 08b062a1..68998da6 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -1,8 +1,10 @@
 name: Benchmark Ix compiler
 
 on:
+  schedule:
+    - cron: "0 0 * * *" # nightly
   push:
-    branches: "sb/cli"
+    branches: sb/cli
   workflow_dispatch:
 
 permissions:
diff --git a/Benchmarks/Compile/Compile.lean b/Benchmarks/Compile/Compile.lean
index 6cea9317..273b769d 100644
--- a/Benchmarks/Compile/Compile.lean
+++ b/Benchmarks/Compile/Compile.lean
@@ -1,13 +1,30 @@
 import Ix.CompileM
 import Ix.Meta
 
+/-- Format a byte count with appropriate unit suffix (B, kB, MB, GB). -/
+def fmtBytes (n : Nat) : String :=
+  if n < 1024 then s!"{n} B"
+  else if n < 1024 * 1024 then
+    let kb := n * 10 / 1024
+    s!"{kb / 10}.{kb % 10} kB"
+  else if n < 1024 * 1024 * 1024 then
+    let mb := n * 10 / (1024 * 1024)
+    s!"{mb / 10}.{mb % 10} MB"
+  else
+    let gb := n * 10 / (1024 * 1024 * 1024)
+    s!"{gb / 10}.{gb % 10} GB"
+
 def compile (name : String) : IO Unit := do
   println! "Compiling {name} environment"
 
-  let leanEnv ← get_env!
+  let path := s!"Compile{name}.lean"
+  let leanEnv ← getFileEnv path
+
+  let totalConsts := leanEnv.constants.toList.length
+  println! "{totalConsts} consts"
 
   let start ← IO.monoMsNow
-  let phases ← Ix.CompileM.rsCompilePhases leanEnv
+  let bytes ← Ix.CompileM.rsCompileEnvBytes 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"
+  IO.println s!"Compiled {fmtBytes bytes.size} env in {elapsed}ms"
diff --git a/Cargo.lock b/Cargo.lock
index 5b9da024..dd4ac112 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2137,9 +2137,9 @@ dependencies = [
 
 [[package]]
 name = "num-conv"
-version = "0.1.0"
+version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+checksum = "cf97ec579c3c42f953ef76dbf8d55ac91fb219dde70e49aa4a6b7d74e9919050"
 
 [[package]]
 name = "num-integer"
@@ -3629,9 +3629,9 @@ dependencies = [
 
 [[package]]
 name = "time"
-version = "0.3.45"
+version = "0.3.47"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f9e442fc33d7fdb45aa9bfeb312c095964abdf596f7567261062b2a7107aaabd"
+checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c"
 dependencies = [
  "deranged",
  "js-sys",
@@ -3643,9 +3643,9 @@ dependencies = [
 
 [[package]]
 name = "time-core"
-version = "0.1.7"
+version = "0.1.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8b36ee98fd31ec7426d599183e8fe26932a8dc1fb76ddb6214d05493377d34ca"
+checksum = "7694e1cfe791f8d31026952abf09c69ca6f6fa4e1a1229e18988f06a04a12dca"
 
 [[package]]
 name = "tiny-keccak"
diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index 37eb14e2..ff9ec0e9 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -8,9 +8,11 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   let some path := p.flag? "path"
     | p.printError "error: must specify --path"
       return 1
-  let leanEnv ← getFileEnv <| path.as! String
+  let pathStr := path.as! String
 
-  IO.println s!"Running Ix compiler"
+  let leanEnv ← getFileEnv pathStr
+
+  println! "Running Ix compiler on {pathStr}"
 
   let start ← IO.monoMsNow
   let phases ← Ix.CompileM.rsCompilePhases leanEnv
diff --git a/Tests/Cli.lean b/Tests/Cli.lean
index 89e2afce..76756738 100644
--- a/Tests/Cli.lean
+++ b/Tests/Cli.lean
@@ -14,8 +14,8 @@ def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Opti
 
 def Tests.Cli.suite : IO UInt32 := do
   Tests.Cli.run "lake" (#["run", "install"]) none
-  let ixTestDir := (← IO.currentDir) / "ix_test"
-  Tests.Cli.run "lake" (#["build"]) (some ixTestDir)
+  let ixTestDir := (← IO.currentDir) / "ix_test" / "IxTest.lean"
+  Tests.Cli.run "ix" (#["compile", "--path", ixTestDir.toString]) none
   --Tests.Cli.run "ix" (#["store", "ix_test/IxTest.lean"]) none
   --Tests.Cli.run "ix" (#["prove", "ix_test/IxTest.lean", "one"]) none
   return 0
diff --git a/flake.nix b/flake.nix
index 03644345..3a2e80bd 100644
--- a/flake.nix
+++ b/flake.nix
@@ -157,6 +157,7 @@
             rust-analyzer
             lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
             gmp
+            cargo-deny
           ];
         };
 

From d174f72b00de752e2e5881ac59d3188022724db9 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 09:49:35 -0500
Subject: [PATCH 04/21] Switch to compiler binary

---
 .github/workflows/compile.yml          |  7 +++---
 Benchmarks/Compile/Compile.lean        | 30 --------------------------
 Benchmarks/Compile/CompileFLT.lean     |  3 ---
 Benchmarks/Compile/CompileLean.lean    |  3 ---
 Benchmarks/Compile/CompileMathlib.lean |  3 ---
 Benchmarks/Compile/README.md           |  4 ++--
 Benchmarks/Compile/lake-manifest.json  | 27 -----------------------
 Benchmarks/Compile/lakefile.lean       | 28 ------------------------
 Benchmarks/Compile/lakefile.toml       | 22 +++++++++++++++++++
 9 files changed, 27 insertions(+), 100 deletions(-)
 delete mode 100644 Benchmarks/Compile/Compile.lean
 delete mode 100644 Benchmarks/Compile/lakefile.lean
 create mode 100644 Benchmarks/Compile/lakefile.toml

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 68998da6..7af80dcc 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -18,13 +18,12 @@ jobs:
   run-compiler:
     strategy:
       matrix:
-        bench: [lean, mathlib, flt]
+        bench: [Lean, Mathlib, FLT]
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
-          lake-package-directory: "Benchmarks/Compile"
-      - working-directory: Benchmarks/Compile
-        run: lake exe compile-${{ matrix.bench }}
+      - run: lake exe ix compile --path Benchmarks/Compile/Compile${{ matrix.bench }}.lean
+
diff --git a/Benchmarks/Compile/Compile.lean b/Benchmarks/Compile/Compile.lean
deleted file mode 100644
index 273b769d..00000000
--- a/Benchmarks/Compile/Compile.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-import Ix.CompileM
-import Ix.Meta
-
-/-- Format a byte count with appropriate unit suffix (B, kB, MB, GB). -/
-def fmtBytes (n : Nat) : String :=
-  if n < 1024 then s!"{n} B"
-  else if n < 1024 * 1024 then
-    let kb := n * 10 / 1024
-    s!"{kb / 10}.{kb % 10} kB"
-  else if n < 1024 * 1024 * 1024 then
-    let mb := n * 10 / (1024 * 1024)
-    s!"{mb / 10}.{mb % 10} MB"
-  else
-    let gb := n * 10 / (1024 * 1024 * 1024)
-    s!"{gb / 10}.{gb % 10} GB"
-
-def compile (name : String) : IO Unit := do
-  println! "Compiling {name} environment"
-
-  let path := s!"Compile{name}.lean"
-  let leanEnv ← getFileEnv path
-
-  let totalConsts := leanEnv.constants.toList.length
-  println! "{totalConsts} consts"
-
-  let start ← IO.monoMsNow
-  let bytes ← Ix.CompileM.rsCompileEnvBytes leanEnv
-  let elapsed := (← IO.monoMsNow) - start
-
-  IO.println s!"Compiled {fmtBytes bytes.size} env in {elapsed}ms"
diff --git a/Benchmarks/Compile/CompileFLT.lean b/Benchmarks/Compile/CompileFLT.lean
index 535b9256..0b3e4b4d 100644
--- a/Benchmarks/Compile/CompileFLT.lean
+++ b/Benchmarks/Compile/CompileFLT.lean
@@ -1,5 +1,2 @@
-import Compile
 import FLT
 
-def main : IO Unit := compile "FLT"
-
diff --git a/Benchmarks/Compile/CompileLean.lean b/Benchmarks/Compile/CompileLean.lean
index eaaf3cfa..78c878a7 100644
--- a/Benchmarks/Compile/CompileLean.lean
+++ b/Benchmarks/Compile/CompileLean.lean
@@ -1,4 +1 @@
-import Compile
 import Lean
-
-def main : IO Unit := compile "Lean"
diff --git a/Benchmarks/Compile/CompileMathlib.lean b/Benchmarks/Compile/CompileMathlib.lean
index ec9f9feb..0b4be76b 100644
--- a/Benchmarks/Compile/CompileMathlib.lean
+++ b/Benchmarks/Compile/CompileMathlib.lean
@@ -1,4 +1 @@
-import Compile
 import Mathlib
-
-def main : IO Unit := compile "Mathlib"
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
index 535ca04f..a4031995 100644
--- a/Benchmarks/Compile/README.md
+++ b/Benchmarks/Compile/README.md
@@ -1,6 +1,6 @@
 # Compile
 
-Runs the Ix compiler over the following libraries when imported:
+Test libraries for the Ix compiler
 
 - [Lean4](https://github.com/leanprover/lean4)
 - [Mathlib](https://github.com/leanprover-community/mathlib4)
@@ -8,7 +8,7 @@ Runs the Ix compiler over the following libraries when imported:
 
 ## Usage
 
-`lake exe compile-<lib>`, e.g. `compile-mathlib`
+`ix compile --path /path/to/Compile<Lib>.lean` # replace <Lib> with `Lean`, `Mathlib`, or `FLT`
 
 > [!NOTE]
 > Compiling Mathlib and FLT, which depends on the former, requires a multi-core CPU and 64+ GB RAM.
diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json
index edf0a98e..18d2be9a 100644
--- a/Benchmarks/Compile/lake-manifest.json
+++ b/Benchmarks/Compile/lake-manifest.json
@@ -21,13 +21,6 @@
    "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"type": "path",
-   "scope": "",
-   "name": "ix",
-   "manifestFile": "lake-manifest.json",
-   "inherited": false,
-   "dir": "../..",
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
@@ -117,26 +110,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.26.0",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/argumentcomputer/Blake3.lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
-   "name": "Blake3",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/argumentcomputer/LSpec",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e",
-   "name": "LSpec",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e",
-   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Compile",
  "lakeDir": ".lake"}
diff --git a/Benchmarks/Compile/lakefile.lean b/Benchmarks/Compile/lakefile.lean
deleted file mode 100644
index 73bc9e49..00000000
--- a/Benchmarks/Compile/lakefile.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-import Lake
-open Lake DSL
-
-package "Compile" where
-  version := v!"0.1.0"
-
-@[default_target]
-lean_lib Compile
-
-lean_exe "compile-lean" where
-  root := `CompileLean
-  supportInterpreter := true
-
-lean_exe "compile-mathlib" where
-  root := `CompileMathlib
-  supportInterpreter := true
-
-lean_exe "compile-flt" where
-  root := `CompileFLT
-  supportInterpreter := true
-
-require ix from "../.."
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "v4.26.0"
-
-require flt from git
-  "https://github.com/ImperialCollegeLondon/FLT" @ "v4.26.0"
diff --git a/Benchmarks/Compile/lakefile.toml b/Benchmarks/Compile/lakefile.toml
new file mode 100644
index 00000000..4e1fba4d
--- /dev/null
+++ b/Benchmarks/Compile/lakefile.toml
@@ -0,0 +1,22 @@
+name = "Compile"
+version = "0.1.0"
+defaultTargets = ["CompileLean"]
+
+[[lean_lib]]
+name = "CompileLean"
+
+[[lean_lib]]
+name = "CompileMathlib"
+
+[[lean_lib]]
+name = "CompileFLT"
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.26.0"
+
+[[require]]
+name = "flt"
+git = "https://github.com/ImperialCollegeLondon/FLT"
+rev = "v4.26.0"

From 408af8e4e5b147ddce1a6c07cc694f5b97180937 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 10:07:21 -0500
Subject: [PATCH 05/21] Pretty print

---
 Ix/Cli/CompileCmd.lean |  7 +++++--
 Ix/Common.lean         | 29 +++++++++++++++++++++++++++++
 Tests/Ix/Compile.lean  | 13 -------------
 3 files changed, 34 insertions(+), 15 deletions(-)

diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index ff9ec0e9..1a9768c4 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -14,11 +14,14 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
 
   println! "Running Ix compiler on {pathStr}"
 
+  let totalConsts := leanEnv.constants.toList.length
+  println! "Total constants: {totalConsts}"
+
   let start ← IO.monoMsNow
-  let phases ← Ix.CompileM.rsCompilePhases leanEnv
+  let bytes ← Ix.CompileM.rsCompileEnvBytes 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"
+  println! "Compiled {fmtBytes bytes.size} env in {elapsed.formatMs}"
   return 0
     
 
diff --git a/Ix/Common.lean b/Ix/Common.lean
index 24e5ca86..808bccd2 100644
--- a/Ix/Common.lean
+++ b/Ix/Common.lean
@@ -302,3 +302,32 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do
   else return s.commandState.env
 
 end Lean
+
+/-- Format a duration in milliseconds with appropriate unit suffix.
+- `0` → `"< 1ms"` (sub-ms precision not available with `Nat` ms)
+- `1`–`999` → `"Xms"`
+- `≥ 1000` → `"X.XXs"` (rounded to two decimal places) -/
+def Nat.formatMs (ms : Nat) : String :=
+  if ms ≥ 1000 then
+    let centisecs := ms / 10
+    let whole := centisecs / 100
+    let frac := centisecs % 100
+    let fracStr := if frac < 10 then s!"0{frac}" else s!"{frac}"
+    s!"{whole}.{fracStr}s"
+  else if ms > 0 then
+    s!"{ms}ms"
+  else
+    "< 1ms"
+
+/-- Format a byte count with appropriate unit suffix (B, kB, MB, GB). -/
+def fmtBytes (n : Nat) : String :=
+  if n < 1024 then s!"{n} B"
+  else if n < 1024 * 1024 then
+    let kb := n * 10 / 1024
+    s!"{kb / 10}.{kb % 10} kB"
+  else if n < 1024 * 1024 * 1024 then
+    let mb := n * 10 / (1024 * 1024)
+    s!"{mb / 10}.{mb % 10} MB"
+  else
+    let gb := n * 10 / (1024 * 1024 * 1024)
+    s!"{gb / 10}.{gb % 10} GB"
diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean
index bd940332..fa6dadff 100644
--- a/Tests/Ix/Compile.lean
+++ b/Tests/Ix/Compile.lean
@@ -37,19 +37,6 @@ def hexDump (bytes : ByteArray) (maxBytes : Nat := 64) : String := Id.run do
   if bytes.size > maxBytes then s := s ++ s!" ... ({bytes.size} bytes total)"
   return s
 
-/-- Format a byte count with appropriate unit suffix (B, kB, MB, GB). -/
-def fmtBytes (n : Nat) : String :=
-  if n < 1024 then s!"{n} B"
-  else if n < 1024 * 1024 then
-    let kb := n * 10 / 1024
-    s!"{kb / 10}.{kb % 10} kB"
-  else if n < 1024 * 1024 * 1024 then
-    let mb := n * 10 / (1024 * 1024)
-    s!"{mb / 10}.{mb % 10} MB"
-  else
-    let gb := n * 10 / (1024 * 1024 * 1024)
-    s!"{gb / 10}.{gb % 10} GB"
-
 /-- Find first byte position where two arrays differ -/
 def findFirstDiff (a b : ByteArray) : Option Nat := Id.run do
   for i in [:min a.size b.size] do

From 88dcc4b80cd333e6d78d2436ab87b437e710668b Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 10:12:44 -0500
Subject: [PATCH 06/21] Build Benchmarks/Compile to get mathlib cache

---
 .github/workflows/compile.yml | 5 +++++
 Benchmarks/Compile/README.md  | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 7af80dcc..07b9c0db 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -25,5 +25,10 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
+          test: false
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "Compile${{ matrix.bench }} --wfail -v"
+          lake-package-directory: "Benchmarks/Compile"
       - run: lake exe ix compile --path Benchmarks/Compile/Compile${{ matrix.bench }}.lean
 
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
index a4031995..05ca13d3 100644
--- a/Benchmarks/Compile/README.md
+++ b/Benchmarks/Compile/README.md
@@ -11,4 +11,4 @@ Test libraries for the Ix compiler
 `ix compile --path /path/to/Compile<Lib>.lean` # replace <Lib> with `Lean`, `Mathlib`, or `FLT`
 
 > [!NOTE]
-> Compiling Mathlib and FLT, which depends on the former, requires a multi-core CPU and 64+ GB RAM.
+> Compiling Mathlib and FLT currently requires a multi-core CPU and >64 GB RAM.

From 8c45064e8cdd0b3b82988782bfed342c24f5d5bb Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 11:09:28 -0500
Subject: [PATCH 07/21] Cache each matrix job separately

---
 .github/workflows/compile.yml | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 07b9c0db..737d1e66 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -15,20 +15,45 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  build:
+    runs-on: warp-ubuntu-latest-x64-32x
+    steps:
+      - uses: actions/checkout@v6
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "--wfail -v"
+          test: false
+
   run-compiler:
+    needs: build
     strategy:
       matrix:
         bench: [Lean, Mathlib, FLT]
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
+      - uses: actions/cache/restore@v4
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
           test: false
+          use-github-cache: false
+      - uses: actions/cache/restore@v4
+        with:
+          path: Benchmarks/Compile/.lake
+          key: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
         with:
           build-args: "Compile${{ matrix.bench }} --wfail -v"
           lake-package-directory: "Benchmarks/Compile"
+          use-github-cache: false
+      - uses: actions/cache/save@v4
+        with:
+          path: Benchmarks/Compile/.lake
+          key: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}-${{ github.sha }}
       - run: lake exe ix compile --path Benchmarks/Compile/Compile${{ matrix.bench }}.lean
-

From 31e75c87b96d5814974af0e51dc93064b4076f50 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 11:19:08 -0500
Subject: [PATCH 08/21] Deduplicate vars

---
 .github/workflows/compile.yml | 36 ++++++++++++++++++++++-------------
 1 file changed, 23 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 737d1e66..7c1d5943 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -14,6 +14,10 @@ concurrency:
   group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
   cancel-in-progress: true
 
+env:
+  BUILD_ARGS: "--wfail -v"
+  COMPILE_DIR: Benchmarks/Compile
+
 jobs:
   build:
     runs-on: warp-ubuntu-latest-x64-32x
@@ -21,7 +25,7 @@ jobs:
       - uses: actions/checkout@v6
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "--wfail -v"
+          build-args: ${{ env.BUILD_ARGS }}
           test: false
 
   run-compiler:
@@ -32,28 +36,34 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
+      - name: Set cache keys
+        run: |
+          ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
+          COMPILE="lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}"
+          echo "ROOT_CACHE_PREFIX=$ROOT" | tee -a $GITHUB_ENV
+          echo "COMPILE_CACHE_PREFIX=$COMPILE" | tee -a $GITHUB_ENV
       - uses: actions/cache/restore@v4
         with:
-          path: .lake
-          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          path: ./.lake
+          key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
+          restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "--wfail -v"
+          build-args: ${{ env.BUILD_ARGS }}
           test: false
           use-github-cache: false
       - uses: actions/cache/restore@v4
         with:
-          path: Benchmarks/Compile/.lake
-          key: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}
+          path: ${{ env.COMPILE_DIR }}/.lake
+          key: ${{ env.COMPILE_CACHE_PREFIX }}-${{ github.sha }}
+          restore-keys: ${{ env.COMPILE_CACHE_PREFIX }}
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "Compile${{ matrix.bench }} --wfail -v"
-          lake-package-directory: "Benchmarks/Compile"
+          build-args: "Compile${{ matrix.bench }} ${{ env.BUILD_ARGS }}"
+          lake-package-directory: ${{ env.COMPILE_DIR }}
           use-github-cache: false
       - uses: actions/cache/save@v4
         with:
-          path: Benchmarks/Compile/.lake
-          key: lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Benchmarks/Compile/lean-toolchain') }}-${{ hashFiles('Benchmarks/Compile/lake-manifest.json') }}-${{ github.sha }}
-      - run: lake exe ix compile --path Benchmarks/Compile/Compile${{ matrix.bench }}.lean
+          path: ${{ env.COMPILE_DIR }}/.lake
+          key: ${{ env.COMPILE_CACHE_PREFIX }}-${{ github.sha }}
+      - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean

From 44e2caf2329a60d7367111abf6287fed5288dcd8 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 11:30:06 -0500
Subject: [PATCH 09/21] Cache ix binary

---
 .github/workflows/compile.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 7c1d5943..c7763ae1 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -20,12 +20,12 @@ env:
 
 jobs:
   build:
-    runs-on: warp-ubuntu-latest-x64-32x
+    runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v6
       - uses: leanprover/lean-action@v1
         with:
-          build-args: ${{ env.BUILD_ARGS }}
+          build-args: "ix ${{ env.BUILD_ARGS }}"
           test: false
 
   run-compiler:
@@ -49,7 +49,7 @@ jobs:
           restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
       - uses: leanprover/lean-action@v1
         with:
-          build-args: ${{ env.BUILD_ARGS }}
+          build-args: "ix ${{ env.BUILD_ARGS }}"
           test: false
           use-github-cache: false
       - uses: actions/cache/restore@v4

From 3f63b7ec48178c480b152cadda506b337c2decea Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 12:56:34 -0500
Subject: [PATCH 10/21] Pre-build when compiling, move ix_test to Benchmarks

---
 .github/workflows/ci.yml                      |  2 +
 .github/workflows/compile.yml                 |  9 ++++-
 .../Compile/CompileInitStd.lean               |  4 --
 Benchmarks/Compile/README.md                  |  4 +-
 Benchmarks/Compile/lakefile.toml              |  5 ++-
 Ix/Cli/CompileCmd.lean                        | 37 +++++++++++++++++++
 ix_test/.gitignore                            |  1 -
 ix_test/IxTest/Basic.lean                     |  1 -
 ix_test/Main.lean                             |  4 --
 ix_test/README.md                             |  1 -
 ix_test/lake-manifest.json                    |  5 ---
 ix_test/lakefile.toml                         | 10 -----
 ix_test/lean-toolchain                        |  1 -
 13 files changed, 53 insertions(+), 31 deletions(-)
 rename ix_test/IxTest.lean => Benchmarks/Compile/CompileInitStd.lean (52%)
 delete mode 100644 ix_test/.gitignore
 delete mode 100644 ix_test/IxTest/Basic.lean
 delete mode 100644 ix_test/Main.lean
 delete mode 100644 ix_test/README.md
 delete mode 100644 ix_test/lake-manifest.json
 delete mode 100644 ix_test/lakefile.toml
 delete mode 100644 ix_test/lean-toolchain

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4a5ba48c..a3b8579b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -30,6 +30,7 @@ jobs:
           ln -sf /opt/homebrew/bin/gcc-14 ~/local/bin/gcc
           export PATH=~/local/bin:$PATH
           which gcc
+      - uses: Swatinem/rust-cache@v2
       - uses: leanprover/lean-action@v1 # https://github.com/leanprover/lean-action
         with:
           build-args: "--wfail -v"
@@ -77,6 +78,7 @@ jobs:
       - uses: ./.github/actions/ci-env
       - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
       - name: Check Rustfmt code style
         run: cargo fmt --all --check
       - name: Check *everything* compiles
diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index c7763ae1..3a8f7c45 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -23,6 +23,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v6
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "ix"
       - uses: leanprover/lean-action@v1
         with:
           build-args: "ix ${{ env.BUILD_ARGS }}"
@@ -32,10 +35,14 @@ jobs:
     needs: build
     strategy:
       matrix:
-        bench: [Lean, Mathlib, FLT]
+        bench: [InitStd, Lean, Mathlib, FLT]
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "ix"
+          save-if: "false"
       - name: Set cache keys
         run: |
           ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
diff --git a/ix_test/IxTest.lean b/Benchmarks/Compile/CompileInitStd.lean
similarity index 52%
rename from ix_test/IxTest.lean
rename to Benchmarks/Compile/CompileInitStd.lean
index f64d0469..2997756a 100644
--- a/ix_test/IxTest.lean
+++ b/Benchmarks/Compile/CompileInitStd.lean
@@ -1,11 +1,7 @@
--- This module serves as the root of the `IxTest` library.
--- Import modules here that should be built as part of the library.
-import IxTest.Basic
 import Init
 import Std
 
 def id' (A: Type) (x: A) := x
-def ref (A: Type) (_x : A) := hello
 
 def idX {A: Type} : A -> A := fun x => x
 def idY {A: Type} : A -> A := fun y => y
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
index 05ca13d3..1e38c800 100644
--- a/Benchmarks/Compile/README.md
+++ b/Benchmarks/Compile/README.md
@@ -2,13 +2,13 @@
 
 Test libraries for the Ix compiler
 
-- [Lean4](https://github.com/leanprover/lean4)
+- [Init, Std, and Lean libraries](https://github.com/leanprover/lean4)
 - [Mathlib](https://github.com/leanprover-community/mathlib4)
 - [FLT project](https://github.com/ImperialCollegeLondon/FLT)
 
 ## Usage
 
-`ix compile --path /path/to/Compile<Lib>.lean` # replace <Lib> with `Lean`, `Mathlib`, or `FLT`
+`ix compile --path /path/to/Compile<Lib>.lean` # replace `<Lib>` with `InitStd`, `Lean`, `Mathlib`, or `FLT`
 
 > [!NOTE]
 > Compiling Mathlib and FLT currently requires a multi-core CPU and >64 GB RAM.
diff --git a/Benchmarks/Compile/lakefile.toml b/Benchmarks/Compile/lakefile.toml
index 4e1fba4d..6b117f4b 100644
--- a/Benchmarks/Compile/lakefile.toml
+++ b/Benchmarks/Compile/lakefile.toml
@@ -1,6 +1,9 @@
 name = "Compile"
 version = "0.1.0"
-defaultTargets = ["CompileLean"]
+defaultTargets = ["CompileInitStd"]
+
+[[lean_lib]]
+name = "CompileInitStd"
 
 [[lean_lib]]
 name = "CompileLean"
diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index 1a9768c4..0c07daee 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -4,12 +4,49 @@ import Ix.CompileM
 import Ix.Meta
 import Lean
 
+open System (FilePath)
+
+/-- If the project depends on Mathlib, download the Mathlib cache. -/
+private def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do
+  let manifest := (cwd.getD ".") / "lake-manifest.json"
+  let contents ← IO.FS.readFile manifest
+  if contents.containsSubstr "leanprover-community/mathlib4" then
+    println! "Detected Mathlib dependency. Fetching Mathlib cache..."
+    let child ← IO.Process.spawn {
+      cmd := "lake"
+      args := #["exe", "cache", "get"]
+      cwd := cwd
+      stdout := .inherit
+      stderr := .inherit
+    }
+    let exitCode ← child.wait
+    if exitCode != 0 then
+      throw $ IO.userError "lake exe cache get failed"
+
+/-- Build the Lean module at the given file path using Lake. -/
+private def buildFile (path : FilePath) : IO Unit := do
+  let path ← IO.FS.realPath path
+  let some moduleName := path.fileStem
+    | throw $ IO.userError s!"cannot determine module name from {path}"
+  fetchMathlibCache path.parent
+  let child ← IO.Process.spawn {
+    cmd := "lake"
+    args := #["build", moduleName]
+    cwd := path.parent
+    stdout := .inherit
+    stderr := .inherit
+  }
+  let exitCode ← child.wait
+  if exitCode != 0 then
+    throw $ IO.userError "lake build failed"
+
 def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   let some path := p.flag? "path"
     | p.printError "error: must specify --path"
       return 1
   let pathStr := path.as! String
 
+  buildFile pathStr
   let leanEnv ← getFileEnv pathStr
 
   println! "Running Ix compiler on {pathStr}"
diff --git a/ix_test/.gitignore b/ix_test/.gitignore
deleted file mode 100644
index bfb30ec8..00000000
--- a/ix_test/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/.lake
diff --git a/ix_test/IxTest/Basic.lean b/ix_test/IxTest/Basic.lean
deleted file mode 100644
index 484c5c43..00000000
--- a/ix_test/IxTest/Basic.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello (A: Type) (x : A) : A := x
diff --git a/ix_test/Main.lean b/ix_test/Main.lean
deleted file mode 100644
index 1c8c23e9..00000000
--- a/ix_test/Main.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import IxTest
-
-def main : IO Unit :=
-  IO.println s!"Hello, world!"
diff --git a/ix_test/README.md b/ix_test/README.md
deleted file mode 100644
index afd8772b..00000000
--- a/ix_test/README.md
+++ /dev/null
@@ -1 +0,0 @@
-# ix_test
\ No newline at end of file
diff --git a/ix_test/lake-manifest.json b/ix_test/lake-manifest.json
deleted file mode 100644
index 9a82a6ac..00000000
--- a/ix_test/lake-manifest.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages": [],
- "name": "ix_test",
- "lakeDir": ".lake"}
diff --git a/ix_test/lakefile.toml b/ix_test/lakefile.toml
deleted file mode 100644
index ff2fd985..00000000
--- a/ix_test/lakefile.toml
+++ /dev/null
@@ -1,10 +0,0 @@
-name = "ix_test"
-version = "0.1.0"
-defaultTargets = ["ix_test"]
-
-[[lean_lib]]
-name = "IxTest"
-
-[[lean_exe]]
-name = "ix_test"
-root = "Main"
diff --git a/ix_test/lean-toolchain b/ix_test/lean-toolchain
deleted file mode 100644
index 4a5353be..00000000
--- a/ix_test/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:4.26.0

From 9f47eb4deb7dda8bd2f2294e0bb3cc3e308cb3a9 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 12:59:08 -0500
Subject: [PATCH 11/21] Fix CLI test

---
 Tests/Cli.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Tests/Cli.lean b/Tests/Cli.lean
index 76756738..fb62e84a 100644
--- a/Tests/Cli.lean
+++ b/Tests/Cli.lean
@@ -14,8 +14,7 @@ def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Opti
 
 def Tests.Cli.suite : IO UInt32 := do
   Tests.Cli.run "lake" (#["run", "install"]) none
-  let ixTestDir := (← IO.currentDir) / "ix_test" / "IxTest.lean"
-  Tests.Cli.run "ix" (#["compile", "--path", ixTestDir.toString]) none
+  Tests.Cli.run "ix" (#["--help"]) none
   --Tests.Cli.run "ix" (#["store", "ix_test/IxTest.lean"]) none
   --Tests.Cli.run "ix" (#["prove", "ix_test/IxTest.lean", "one"]) none
   return 0

From 06a4f5efb7cacb1d2e7fe92290c03b6fdbb21000 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 14:01:21 -0500
Subject: [PATCH 12/21] Auto-detect mathlib cache

---
 Ix/Cli/CompileCmd.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index 0c07daee..35196b79 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -8,9 +8,14 @@ open System (FilePath)
 
 /-- If the project depends on Mathlib, download the Mathlib cache. -/
 private def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do
-  let manifest := (cwd.getD ".") / "lake-manifest.json"
+  let root := cwd.getD "."
+  let manifest := root / "lake-manifest.json"
   let contents ← IO.FS.readFile manifest
   if contents.containsSubstr "leanprover-community/mathlib4" then
+    let mathlibBuild := root / ".lake" / "packages" / "mathlib" / ".lake" / "build"
+    if ← mathlibBuild.pathExists then
+      println! "Mathlib cache already present, skipping fetch."
+      return
     println! "Detected Mathlib dependency. Fetching Mathlib cache..."
     let child ← IO.Process.spawn {
       cmd := "lake"

From 2d12d9590fd0e340f4bea9042527dcda17de3554 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 14:14:50 -0500
Subject: [PATCH 13/21] Add CompileFC benchmark

---
 .github/workflows/compile.yml       |  4 +++-
 Benchmarks/CompileFC/CompileFC.lean |  1 +
 Benchmarks/CompileFC/Main.lean      | 12 ------------
 Benchmarks/CompileFC/README.md      |  7 ++++---
 Benchmarks/CompileFC/lakefile.toml  | 11 +----------
 5 files changed, 9 insertions(+), 26 deletions(-)
 create mode 100644 Benchmarks/CompileFC/CompileFC.lean
 delete mode 100644 Benchmarks/CompileFC/Main.lean

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 3a8f7c45..91802571 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -35,7 +35,7 @@ jobs:
     needs: build
     strategy:
       matrix:
-        bench: [InitStd, Lean, Mathlib, FLT]
+        bench: [InitStd, Lean, Mathlib, FLT, FC]
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
@@ -43,6 +43,8 @@ jobs:
         with:
           shared-key: "ix"
           save-if: "false"
+      - if: matrix.bench == 'FC'
+        run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
       - name: Set cache keys
         run: |
           ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
diff --git a/Benchmarks/CompileFC/CompileFC.lean b/Benchmarks/CompileFC/CompileFC.lean
new file mode 100644
index 00000000..2be764da
--- /dev/null
+++ b/Benchmarks/CompileFC/CompileFC.lean
@@ -0,0 +1 @@
+import FormalConjectures
diff --git a/Benchmarks/CompileFC/Main.lean b/Benchmarks/CompileFC/Main.lean
deleted file mode 100644
index 19a5d29e..00000000
--- a/Benchmarks/CompileFC/Main.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import FormalConjectures
-
-def main : IO Unit :=
-  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"
diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md
index 6f3d90df..af038b74 100644
--- a/Benchmarks/CompileFC/README.md
+++ b/Benchmarks/CompileFC/README.md
@@ -1,11 +1,12 @@
 # CompileFC
 
-WIP: Doesn't build with lean4-nix v4.22.0 with the lake dev shell due to changes in `.lake` behavior
-
 Runs the Ix compiler over the Lean environment of https://github.com/google-deepmind/formal-conjectures.
 
 Uses Lean v4.22.0 to match the formal-conjectures project, hence the separate project.
 
+> [!NOTE]
+> Doesn't build with lean4-nix v4.22.0 with the lake dev shell due to changes in `.lake` behavior
+
 ## Usage
 
-`lake exe compile-fc`
+`ix compile --path /path/to/CompileFC.lean`
diff --git a/Benchmarks/CompileFC/lakefile.toml b/Benchmarks/CompileFC/lakefile.toml
index 4af65631..0e2f81c9 100644
--- a/Benchmarks/CompileFC/lakefile.toml
+++ b/Benchmarks/CompileFC/lakefile.toml
@@ -1,20 +1,11 @@
 name = "CompileFC"
 version = "0.1.0"
-defaultTargets = ["compile-fc"]
+defaultTargets = ["CompileFC"]
 
 [[lean_lib]]
 name = "CompileFC"
 
-[[lean_exe]]
-name = "compile-fc"
-root = "Main"
-supportInterpreter = true
-
 [[require]]
 name = "formal_conjectures"
 git = "https://github.com/google-deepmind/formal-conjectures"
 rev = "20af7726bba72fc97d8feda6958a8afacc664ad4"
-
-[[require]]
-name = "ix"
-path = "../.."

From 3453312be08cddd73b23589dc52ae4d31bed7849 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 15:06:05 -0500
Subject: [PATCH 14/21] Revert to shared cache

---
 .github/workflows/compile.yml | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 91802571..c9ac7687 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -35,7 +35,7 @@ jobs:
     needs: build
     strategy:
       matrix:
-        bench: [InitStd, Lean, Mathlib, FLT, FC]
+        bench: [InitStd, Lean, Mathlib, FLT] # Add FC when it works
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
@@ -43,14 +43,12 @@ jobs:
         with:
           shared-key: "ix"
           save-if: "false"
-      - if: matrix.bench == 'FC'
-        run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
+      # - if: matrix.bench == 'FC'
+      #   run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
       - name: Set cache keys
         run: |
           ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
-          COMPILE="lake-${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}"
           echo "ROOT_CACHE_PREFIX=$ROOT" | tee -a $GITHUB_ENV
-          echo "COMPILE_CACHE_PREFIX=$COMPILE" | tee -a $GITHUB_ENV
       - uses: actions/cache/restore@v4
         with:
           path: ./.lake
@@ -61,18 +59,8 @@ jobs:
           build-args: "ix ${{ env.BUILD_ARGS }}"
           test: false
           use-github-cache: false
-      - uses: actions/cache/restore@v4
-        with:
-          path: ${{ env.COMPILE_DIR }}/.lake
-          key: ${{ env.COMPILE_CACHE_PREFIX }}-${{ github.sha }}
-          restore-keys: ${{ env.COMPILE_CACHE_PREFIX }}
       - uses: leanprover/lean-action@v1
         with:
           build-args: "Compile${{ matrix.bench }} ${{ env.BUILD_ARGS }}"
           lake-package-directory: ${{ env.COMPILE_DIR }}
-          use-github-cache: false
-      - uses: actions/cache/save@v4
-        with:
-          path: ${{ env.COMPILE_DIR }}/.lake
-          key: ${{ env.COMPILE_CACHE_PREFIX }}-${{ github.sha }}
       - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean

From 093b87224fcff10e37a5bfe1914f37247211a1c7 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 15:16:47 -0500
Subject: [PATCH 15/21] Don't cache individual targets

---
 .github/workflows/compile.yml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index c9ac7687..292b96b3 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -43,24 +43,19 @@ jobs:
         with:
           shared-key: "ix"
           save-if: "false"
-      # - if: matrix.bench == 'FC'
-      #   run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
       - name: Set cache keys
         run: |
           ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
           echo "ROOT_CACHE_PREFIX=$ROOT" | tee -a $GITHUB_ENV
+      # Restore cached `ix` build from prior step
       - uses: actions/cache/restore@v4
         with:
           path: ./.lake
           key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
           restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
-      - uses: leanprover/lean-action@v1
-        with:
-          build-args: "ix ${{ env.BUILD_ARGS }}"
-          test: false
-          use-github-cache: false
       - uses: leanprover/lean-action@v1
         with:
           build-args: "Compile${{ matrix.bench }} ${{ env.BUILD_ARGS }}"
           lake-package-directory: ${{ env.COMPILE_DIR }}
+          use-github-cache: false
       - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean

From 8d752c7b59f037c2f7c3d4400a3b00939fb8b8bf Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 15:30:23 -0500
Subject: [PATCH 16/21] Cache FLT only

---
 .github/workflows/compile.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 292b96b3..386167ac 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -53,9 +53,17 @@ jobs:
           path: ./.lake
           key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
           restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
+      # FLT takes a few minutes to rebuild, so we cache the build artifacts
+      - if: matrix.bench == 'FLT'
+        uses: actions/cache@v4
+        with:
+          path: ${{ env.COMPILE_DIR }}/.lake/packages/flt/.lake/build
+          key: flt-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
+      # Build the input library
       - uses: leanprover/lean-action@v1
         with:
           build-args: "Compile${{ matrix.bench }} ${{ env.BUILD_ARGS }}"
           lake-package-directory: ${{ env.COMPILE_DIR }}
           use-github-cache: false
+      # Run the `ix` compiler over the input library
       - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean

From 083a10fbdc4a270121ae0ea4473ee0304e85a8bc Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 16:35:00 -0500
Subject: [PATCH 17/21] Restore CompileFC bench

---
 .github/workflows/compile.yml       |  10 +-
 Benchmarks/CompileFC/.envrc         |   1 +
 Benchmarks/CompileFC/CompileFC.lean | 566 +++++++++++++++++++++++++++-
 Benchmarks/CompileFC/README.md      |  13 +-
 Benchmarks/CompileFC/lean-toolchain |   2 +-
 5 files changed, 582 insertions(+), 10 deletions(-)
 create mode 100644 Benchmarks/CompileFC/.envrc

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 386167ac..4a5b1667 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -35,7 +35,7 @@ jobs:
     needs: build
     strategy:
       matrix:
-        bench: [InitStd, Lean, Mathlib, FLT] # Add FC when it works
+        bench: [InitStd, Lean, Mathlib, FLT, FC]
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
@@ -53,12 +53,14 @@ jobs:
           path: ./.lake
           key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
           restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
-      # FLT takes a few minutes to rebuild, so we cache the build artifacts
-      - if: matrix.bench == 'FLT'
+      - if: matrix.bench == 'FC'
+        run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
+      # FLT and FC take a few minutes to rebuild, so we cache the build artifacts
+      - if: matrix.bench == 'FLT' || matrix.bench == 'FC'
         uses: actions/cache@v4
         with:
           path: ${{ env.COMPILE_DIR }}/.lake/packages/flt/.lake/build
-          key: flt-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
+          key: ${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
       # Build the input library
       - uses: leanprover/lean-action@v1
         with:
diff --git a/Benchmarks/CompileFC/.envrc b/Benchmarks/CompileFC/.envrc
new file mode 100644
index 00000000..3550a30f
--- /dev/null
+++ b/Benchmarks/CompileFC/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/Benchmarks/CompileFC/CompileFC.lean b/Benchmarks/CompileFC/CompileFC.lean
index 2be764da..ed4c3e47 100644
--- a/Benchmarks/CompileFC/CompileFC.lean
+++ b/Benchmarks/CompileFC/CompileFC.lean
@@ -1 +1,565 @@
-import FormalConjectures
+import FormalConjectures.Arxiv.«0911.2077».Conjecture6_3
+import FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture
+import FormalConjectures.Arxiv.«1308.0994».BoxdotConjecture
+import FormalConjectures.Arxiv.«1506.05785».MaximumAngle
+import FormalConjectures.Arxiv.«1601.03081».UniqueCrystalComponents
+import FormalConjectures.Arxiv.«1609.08688».sIncreasingrTuples
+import FormalConjectures.Arxiv.«2107.00295».IndependentDomination
+import FormalConjectures.Arxiv.«2107.12475».CollatzLike
+import FormalConjectures.Arxiv.«2208.14736».ZariskiCancellation
+import FormalConjectures.Arxiv.«2501.03234».ArithmeticSumS
+import FormalConjectures.Arxiv.«2504.17644».Margulis
+import FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution
+import FormalConjectures.ErdosProblems.«1003»
+import FormalConjectures.ErdosProblems.«1004»
+import FormalConjectures.ErdosProblems.«100»
+import FormalConjectures.ErdosProblems.«1038»
+import FormalConjectures.ErdosProblems.«1041»
+import FormalConjectures.ErdosProblems.«1043»
+import FormalConjectures.ErdosProblems.«1051»
+import FormalConjectures.ErdosProblems.«1052»
+import FormalConjectures.ErdosProblems.«1054»
+import FormalConjectures.ErdosProblems.«1055»
+import FormalConjectures.ErdosProblems.«1056»
+import FormalConjectures.ErdosProblems.«1059»
+import FormalConjectures.ErdosProblems.«1060»
+import FormalConjectures.ErdosProblems.«1061»
+import FormalConjectures.ErdosProblems.«1062»
+import FormalConjectures.ErdosProblems.«1063»
+import FormalConjectures.ErdosProblems.«1064»
+import FormalConjectures.ErdosProblems.«1065»
+import FormalConjectures.ErdosProblems.«1067»
+import FormalConjectures.ErdosProblems.«1068»
+import FormalConjectures.ErdosProblems.«1071»
+import FormalConjectures.ErdosProblems.«1072»
+import FormalConjectures.ErdosProblems.«1073»
+import FormalConjectures.ErdosProblems.«1074»
+import FormalConjectures.ErdosProblems.«1077»
+import FormalConjectures.ErdosProblems.«107»
+import FormalConjectures.ErdosProblems.«1080»
+import FormalConjectures.ErdosProblems.«1084»
+import FormalConjectures.ErdosProblems.«1085»
+import FormalConjectures.ErdosProblems.«108»
+import FormalConjectures.ErdosProblems.«1092»
+import FormalConjectures.ErdosProblems.«1093»
+import FormalConjectures.ErdosProblems.«1094»
+import FormalConjectures.ErdosProblems.«1095»
+import FormalConjectures.ErdosProblems.«1097»
+import FormalConjectures.ErdosProblems.«109»
+import FormalConjectures.ErdosProblems.«10»
+import FormalConjectures.ErdosProblems.«1101»
+import FormalConjectures.ErdosProblems.«1102»
+import FormalConjectures.ErdosProblems.«1104»
+import FormalConjectures.ErdosProblems.«1105»
+import FormalConjectures.ErdosProblems.«1106»
+import FormalConjectures.ErdosProblems.«1107»
+import FormalConjectures.ErdosProblems.«1108»
+import FormalConjectures.ErdosProblems.«1135»
+import FormalConjectures.ErdosProblems.«1137»
+import FormalConjectures.ErdosProblems.«1139»
+import FormalConjectures.ErdosProblems.«1145»
+import FormalConjectures.ErdosProblems.«1148»
+import FormalConjectures.ErdosProblems.«1150»
+import FormalConjectures.ErdosProblems.«1176»
+import FormalConjectures.ErdosProblems.«119»
+import FormalConjectures.ErdosProblems.«11»
+import FormalConjectures.ErdosProblems.«120»
+import FormalConjectures.ErdosProblems.«123»
+import FormalConjectures.ErdosProblems.«124»
+import FormalConjectures.ErdosProblems.«125»
+import FormalConjectures.ErdosProblems.«126»
+import FormalConjectures.ErdosProblems.«128»
+import FormalConjectures.ErdosProblems.«12»
+import FormalConjectures.ErdosProblems.«137»
+import FormalConjectures.ErdosProblems.«138»
+import FormalConjectures.ErdosProblems.«139»
+import FormalConjectures.ErdosProblems.«13»
+import FormalConjectures.ErdosProblems.«141»
+import FormalConjectures.ErdosProblems.«142»
+import FormalConjectures.ErdosProblems.«143»
+import FormalConjectures.ErdosProblems.«145»
+import FormalConjectures.ErdosProblems.«14»
+import FormalConjectures.ErdosProblems.«152»
+import FormalConjectures.ErdosProblems.«153»
+import FormalConjectures.ErdosProblems.«155»
+import FormalConjectures.ErdosProblems.«158»
+import FormalConjectures.ErdosProblems.«160»
+import FormalConjectures.ErdosProblems.«168»
+import FormalConjectures.ErdosProblems.«170»
+import FormalConjectures.ErdosProblems.«172»
+import FormalConjectures.ErdosProblems.«17»
+import FormalConjectures.ErdosProblems.«188»
+import FormalConjectures.ErdosProblems.«189»
+import FormalConjectures.ErdosProblems.«194»
+import FormalConjectures.ErdosProblems.«195»
+import FormalConjectures.ErdosProblems.«196»
+import FormalConjectures.ErdosProblems.«197»
+import FormalConjectures.ErdosProblems.«198»
+import FormalConjectures.ErdosProblems.«1»
+import FormalConjectures.ErdosProblems.«200»
+import FormalConjectures.ErdosProblems.«203»
+import FormalConjectures.ErdosProblems.«204»
+import FormalConjectures.ErdosProblems.«208»
+import FormalConjectures.ErdosProblems.«20»
+import FormalConjectures.ErdosProblems.«212»
+import FormalConjectures.ErdosProblems.«213»
+import FormalConjectures.ErdosProblems.«218»
+import FormalConjectures.ErdosProblems.«219»
+import FormalConjectures.ErdosProblems.«228»
+import FormalConjectures.ErdosProblems.«229»
+import FormalConjectures.ErdosProblems.«233»
+import FormalConjectures.ErdosProblems.«234»
+import FormalConjectures.ErdosProblems.«236»
+import FormalConjectures.ErdosProblems.«238»
+import FormalConjectures.ErdosProblems.«239»
+import FormalConjectures.ErdosProblems.«242»
+import FormalConjectures.ErdosProblems.«243»
+import FormalConjectures.ErdosProblems.«244»
+import FormalConjectures.ErdosProblems.«245»
+import FormalConjectures.ErdosProblems.«247»
+import FormalConjectures.ErdosProblems.«248»
+import FormalConjectures.ErdosProblems.«249»
+import FormalConjectures.ErdosProblems.«250»
+import FormalConjectures.ErdosProblems.«251»
+import FormalConjectures.ErdosProblems.«252»
+import FormalConjectures.ErdosProblems.«253»
+import FormalConjectures.ErdosProblems.«257»
+import FormalConjectures.ErdosProblems.«258»
+import FormalConjectures.ErdosProblems.«259»
+import FormalConjectures.ErdosProblems.«25»
+import FormalConjectures.ErdosProblems.«263»
+import FormalConjectures.ErdosProblems.«264»
+import FormalConjectures.ErdosProblems.«266»
+import FormalConjectures.ErdosProblems.«267»
+import FormalConjectures.ErdosProblems.«268»
+import FormalConjectures.ErdosProblems.«269»
+import FormalConjectures.ErdosProblems.«26»
+import FormalConjectures.ErdosProblems.«273»
+import FormalConjectures.ErdosProblems.«274»
+import FormalConjectures.ErdosProblems.«275»
+import FormalConjectures.ErdosProblems.«276»
+import FormalConjectures.ErdosProblems.«277»
+import FormalConjectures.ErdosProblems.«283»
+import FormalConjectures.ErdosProblems.«285»
+import FormalConjectures.ErdosProblems.«288»
+import FormalConjectures.ErdosProblems.«289»
+import FormalConjectures.ErdosProblems.«28»
+import FormalConjectures.ErdosProblems.«295»
+import FormalConjectures.ErdosProblems.«298»
+import FormalConjectures.ErdosProblems.«299»
+import FormalConjectures.ErdosProblems.«303»
+import FormalConjectures.ErdosProblems.«304»
+import FormalConjectures.ErdosProblems.«306»
+import FormalConjectures.ErdosProblems.«307»
+import FormalConjectures.ErdosProblems.«30»
+import FormalConjectures.ErdosProblems.«312»
+import FormalConjectures.ErdosProblems.«313»
+import FormalConjectures.ErdosProblems.«316»
+import FormalConjectures.ErdosProblems.«317»
+import FormalConjectures.ErdosProblems.«318»
+import FormalConjectures.ErdosProblems.«319»
+import FormalConjectures.ErdosProblems.«321»
+import FormalConjectures.ErdosProblems.«324»
+import FormalConjectures.ErdosProblems.«325»
+import FormalConjectures.ErdosProblems.«326»
+import FormalConjectures.ErdosProblems.«329»
+import FormalConjectures.ErdosProblems.«330»
+import FormalConjectures.ErdosProblems.«331»
+import FormalConjectures.ErdosProblems.«332»
+import FormalConjectures.ErdosProblems.«33»
+import FormalConjectures.ErdosProblems.«340»
+import FormalConjectures.ErdosProblems.«341»
+import FormalConjectures.ErdosProblems.«346»
+import FormalConjectures.ErdosProblems.«347»
+import FormalConjectures.ErdosProblems.«348»
+import FormalConjectures.ErdosProblems.«349»
+import FormalConjectures.ErdosProblems.«350»
+import FormalConjectures.ErdosProblems.«351»
+import FormalConjectures.ErdosProblems.«352»
+import FormalConjectures.ErdosProblems.«354»
+import FormalConjectures.ErdosProblems.«355»
+import FormalConjectures.ErdosProblems.«357»
+import FormalConjectures.ErdosProblems.«358»
+import FormalConjectures.ErdosProblems.«359»
+import FormalConjectures.ErdosProblems.«361»
+import FormalConjectures.ErdosProblems.«364»
+import FormalConjectures.ErdosProblems.«366»
+import FormalConjectures.ErdosProblems.«36»
+import FormalConjectures.ErdosProblems.«370»
+import FormalConjectures.ErdosProblems.«371»
+import FormalConjectures.ErdosProblems.«373»
+import FormalConjectures.ErdosProblems.«375»
+import FormalConjectures.ErdosProblems.«376»
+import FormalConjectures.ErdosProblems.«377»
+import FormalConjectures.ErdosProblems.«379»
+import FormalConjectures.ErdosProblems.«383»
+import FormalConjectures.ErdosProblems.«385»
+import FormalConjectures.ErdosProblems.«386»
+import FormalConjectures.ErdosProblems.«387»
+import FormalConjectures.ErdosProblems.«389»
+import FormalConjectures.ErdosProblems.«38»
+import FormalConjectures.ErdosProblems.«390»
+import FormalConjectures.ErdosProblems.«392»
+import FormalConjectures.ErdosProblems.«394»
+import FormalConjectures.ErdosProblems.«396»
+import FormalConjectures.ErdosProblems.«397»
+import FormalConjectures.ErdosProblems.«398»
+import FormalConjectures.ErdosProblems.«399»
+import FormalConjectures.ErdosProblems.«39»
+import FormalConjectures.ErdosProblems.«3»
+import FormalConjectures.ErdosProblems.«402»
+import FormalConjectures.ErdosProblems.«406»
+import FormalConjectures.ErdosProblems.«409»
+import FormalConjectures.ErdosProblems.«40»
+import FormalConjectures.ErdosProblems.«410»
+import FormalConjectures.ErdosProblems.«412»
+import FormalConjectures.ErdosProblems.«413»
+import FormalConjectures.ErdosProblems.«414»
+import FormalConjectures.ErdosProblems.«416»
+import FormalConjectures.ErdosProblems.«417»
+import FormalConjectures.ErdosProblems.«418»
+import FormalConjectures.ErdosProblems.«41»
+import FormalConjectures.ErdosProblems.«421»
+import FormalConjectures.ErdosProblems.«422»
+import FormalConjectures.ErdosProblems.«424»
+import FormalConjectures.ErdosProblems.«427»
+import FormalConjectures.ErdosProblems.«428»
+import FormalConjectures.ErdosProblems.«42»
+import FormalConjectures.ErdosProblems.«434»
+import FormalConjectures.ErdosProblems.«442»
+import FormalConjectures.ErdosProblems.«44»
+import FormalConjectures.ErdosProblems.«454»
+import FormalConjectures.ErdosProblems.«455»
+import FormalConjectures.ErdosProblems.«457»
+import FormalConjectures.ErdosProblems.«458»
+import FormalConjectures.ErdosProblems.«463»
+import FormalConjectures.ErdosProblems.«469»
+import FormalConjectures.ErdosProblems.«470»
+import FormalConjectures.ErdosProblems.«477»
+import FormalConjectures.ErdosProblems.«479»
+import FormalConjectures.ErdosProblems.«480»
+import FormalConjectures.ErdosProblems.«486»
+import FormalConjectures.ErdosProblems.«488»
+import FormalConjectures.ErdosProblems.«48»
+import FormalConjectures.ErdosProblems.«494»
+import FormalConjectures.ErdosProblems.«495»
+import FormalConjectures.ErdosProblems.«499»
+import FormalConjectures.ErdosProblems.«4»
+import FormalConjectures.ErdosProblems.«503»
+import FormalConjectures.ErdosProblems.«507»
+import FormalConjectures.ErdosProblems.«508»
+import FormalConjectures.ErdosProblems.«509»
+import FormalConjectures.ErdosProblems.«510»
+import FormalConjectures.ErdosProblems.«513»
+import FormalConjectures.ErdosProblems.«516»
+import FormalConjectures.ErdosProblems.«517»
+import FormalConjectures.ErdosProblems.«51»
+import FormalConjectures.ErdosProblems.«520»
+import FormalConjectures.ErdosProblems.«522»
+import FormalConjectures.ErdosProblems.«536»
+import FormalConjectures.ErdosProblems.«541»
+import FormalConjectures.ErdosProblems.«562»
+import FormalConjectures.ErdosProblems.«564»
+import FormalConjectures.ErdosProblems.«566»
+import FormalConjectures.ErdosProblems.«567»
+import FormalConjectures.ErdosProblems.«56»
+import FormalConjectures.ErdosProblems.«587»
+import FormalConjectures.ErdosProblems.«590»
+import FormalConjectures.ErdosProblems.«591»
+import FormalConjectures.ErdosProblems.«592»
+import FormalConjectures.ErdosProblems.«598»
+import FormalConjectures.ErdosProblems.«617»
+import FormalConjectures.ErdosProblems.«61»
+import FormalConjectures.ErdosProblems.«623»
+import FormalConjectures.ErdosProblems.«624»
+import FormalConjectures.ErdosProblems.«645»
+import FormalConjectures.ErdosProblems.«647»
+import FormalConjectures.ErdosProblems.«64»
+import FormalConjectures.ErdosProblems.«659»
+import FormalConjectures.ErdosProblems.«66»
+import FormalConjectures.ErdosProblems.«672»
+import FormalConjectures.ErdosProblems.«677»
+import FormalConjectures.ErdosProblems.«678»
+import FormalConjectures.ErdosProblems.«67»
+import FormalConjectures.ErdosProblems.«680»
+import FormalConjectures.ErdosProblems.«681»
+import FormalConjectures.ErdosProblems.«686»
+import FormalConjectures.ErdosProblems.«689»
+import FormalConjectures.ErdosProblems.«68»
+import FormalConjectures.ErdosProblems.«694»
+import FormalConjectures.ErdosProblems.«695»
+import FormalConjectures.ErdosProblems.«697»
+import FormalConjectures.ErdosProblems.«699»
+import FormalConjectures.ErdosProblems.«69»
+import FormalConjectures.ErdosProblems.«6»
+import FormalConjectures.ErdosProblems.«705»
+import FormalConjectures.ErdosProblems.«707»
+import FormalConjectures.ErdosProblems.«723»
+import FormalConjectures.ErdosProblems.«727»
+import FormalConjectures.ErdosProblems.«728»
+import FormalConjectures.ErdosProblems.«730»
+import FormalConjectures.ErdosProblems.«741»
+import FormalConjectures.ErdosProblems.«749»
+import FormalConjectures.ErdosProblems.«74»
+import FormalConjectures.ErdosProblems.«757»
+import FormalConjectures.ErdosProblems.«770»
+import FormalConjectures.ErdosProblems.«779»
+import FormalConjectures.ErdosProblems.«786»
+import FormalConjectures.ErdosProblems.«817»
+import FormalConjectures.ErdosProblems.«822»
+import FormalConjectures.ErdosProblems.«825»
+import FormalConjectures.ErdosProblems.«826»
+import FormalConjectures.ErdosProblems.«828»
+import FormalConjectures.ErdosProblems.«82»
+import FormalConjectures.ErdosProblems.«830»
+import FormalConjectures.ErdosProblems.«835»
+import FormalConjectures.ErdosProblems.«845»
+import FormalConjectures.ErdosProblems.«846»
+import FormalConjectures.ErdosProblems.«847»
+import FormalConjectures.ErdosProblems.«848»
+import FormalConjectures.ErdosProblems.«849»
+import FormalConjectures.ErdosProblems.«850»
+import FormalConjectures.ErdosProblems.«851»
+import FormalConjectures.ErdosProblems.«853»
+import FormalConjectures.ErdosProblems.«855»
+import FormalConjectures.ErdosProblems.«859»
+import FormalConjectures.ErdosProblems.«85»
+import FormalConjectures.ErdosProblems.«868»
+import FormalConjectures.ErdosProblems.«873»
+import FormalConjectures.ErdosProblems.«881»
+import FormalConjectures.ErdosProblems.«885»
+import FormalConjectures.ErdosProblems.«886»
+import FormalConjectures.ErdosProblems.«887»
+import FormalConjectures.ErdosProblems.«888»
+import FormalConjectures.ErdosProblems.«889»
+import FormalConjectures.ErdosProblems.«890»
+import FormalConjectures.ErdosProblems.«891»
+import FormalConjectures.ErdosProblems.«893»
+import FormalConjectures.ErdosProblems.«897»
+import FormalConjectures.ErdosProblems.«899»
+import FormalConjectures.ErdosProblems.«89»
+import FormalConjectures.ErdosProblems.«906»
+import FormalConjectures.ErdosProblems.«90»
+import FormalConjectures.ErdosProblems.«912»
+import FormalConjectures.ErdosProblems.«913»
+import FormalConjectures.ErdosProblems.«918»
+import FormalConjectures.ErdosProblems.«920»
+import FormalConjectures.ErdosProblems.«92»
+import FormalConjectures.ErdosProblems.«930»
+import FormalConjectures.ErdosProblems.«931»
+import FormalConjectures.ErdosProblems.«932»
+import FormalConjectures.ErdosProblems.«936»
+import FormalConjectures.ErdosProblems.«938»
+import FormalConjectures.ErdosProblems.«939»
+import FormalConjectures.ErdosProblems.«940»
+import FormalConjectures.ErdosProblems.«942»
+import FormalConjectures.ErdosProblems.«943»
+import FormalConjectures.ErdosProblems.«944»
+import FormalConjectures.ErdosProblems.«945»
+import FormalConjectures.ErdosProblems.«946»
+import FormalConjectures.ErdosProblems.«949»
+import FormalConjectures.ErdosProblems.«951»
+import FormalConjectures.ErdosProblems.«952»
+import FormalConjectures.ErdosProblems.«961»
+import FormalConjectures.ErdosProblems.«965»
+import FormalConjectures.ErdosProblems.«968»
+import FormalConjectures.ErdosProblems.«971»
+import FormalConjectures.ErdosProblems.«972»
+import FormalConjectures.ErdosProblems.«975»
+import FormalConjectures.ErdosProblems.«978»
+import FormalConjectures.ErdosProblems.«979»
+import FormalConjectures.ErdosProblems.«97»
+import FormalConjectures.ErdosProblems.«982»
+import FormalConjectures.ErdosProblems.«985»
+import FormalConjectures.ErdosProblems.«996»
+import FormalConjectures.ErdosProblems.«99»
+import FormalConjectures.ErdosProblems.«9»
+import FormalConjectures.GreensOpenProblems.«12»
+import FormalConjectures.GreensOpenProblems.«16»
+import FormalConjectures.GreensOpenProblems.«1»
+import FormalConjectures.GreensOpenProblems.«23»
+import FormalConjectures.GreensOpenProblems.«24»
+import FormalConjectures.GreensOpenProblems.«2»
+import FormalConjectures.GreensOpenProblems.«35»
+import FormalConjectures.GreensOpenProblems.«37»
+import FormalConjectures.GreensOpenProblems.«3»
+import FormalConjectures.GreensOpenProblems.«45»
+import FormalConjectures.GreensOpenProblems.«4»
+import FormalConjectures.GreensOpenProblems.«57»
+import FormalConjectures.GreensOpenProblems.«58»
+import FormalConjectures.GreensOpenProblems.«60»
+import FormalConjectures.GreensOpenProblems.«61»
+import FormalConjectures.GreensOpenProblems.«62»
+import FormalConjectures.GreensOpenProblems.«63»
+import FormalConjectures.GreensOpenProblems.«72»
+import FormalConjectures.GreensOpenProblems.«7»
+import FormalConjectures.GreensOpenProblems.«81»
+import FormalConjectures.GreensOpenProblems.«85»
+import FormalConjectures.GreensOpenProblems.«94»
+import FormalConjectures.GreensOpenProblems.«9»
+import FormalConjectures.HilbertProblems.«17»
+import FormalConjectures.Mathoverflow.«1973»
+import FormalConjectures.Mathoverflow.«21003»
+import FormalConjectures.Mathoverflow.«235893»
+import FormalConjectures.Mathoverflow.«31809»
+import FormalConjectures.Mathoverflow.«339137»
+import FormalConjectures.Mathoverflow.«34145»
+import FormalConjectures.Mathoverflow.«347178»
+import FormalConjectures.Mathoverflow.«486451»
+import FormalConjectures.Mathoverflow.«75792»
+import FormalConjectures.Millenium.GeneralizedRiemannHypothesis
+import FormalConjectures.Millenium.PvsNP
+import FormalConjectures.OEIS.«228828»
+import FormalConjectures.OEIS.«231201»
+import FormalConjectures.OEIS.«232174»
+import FormalConjectures.OEIS.«239957»
+import FormalConjectures.OEIS.«280831»
+import FormalConjectures.OEIS.«281976»
+import FormalConjectures.OEIS.«287616»
+import FormalConjectures.OEIS.«303656»
+import FormalConjectures.OEIS.«306477»
+import FormalConjectures.OEIS.«308734»
+import FormalConjectures.OEIS.«34693»
+import FormalConjectures.OEIS.«358684»
+import FormalConjectures.OEIS.«41»
+import FormalConjectures.OEIS.«56777»
+import FormalConjectures.OEIS.«63880»
+import FormalConjectures.OEIS.«6697»
+import FormalConjectures.OEIS.«67720»
+import FormalConjectures.OEIS.«80170»
+import FormalConjectures.OEIS.«81091»
+import FormalConjectures.OEIS.«87719»
+import FormalConjectures.Other.BeaverMathOlympiad
+import FormalConjectures.Other.EquationalTheories_677_255
+import FormalConjectures.Other.OddPerfectNumber
+import FormalConjectures.Other.SchurTruncatedExponential
+import FormalConjectures.Other.VCDimConvex
+import FormalConjectures.Paper.CardinalityLindelof
+import FormalConjectures.Paper.CasasAlvero
+import FormalConjectures.Paper.CatchUpConjecture
+import FormalConjectures.Paper.Chvatal
+import FormalConjectures.Paper.DegreeSequencesTriangleFree
+import FormalConjectures.Paper.HartshorneConjecture
+import FormalConjectures.Paper.Homogenous
+import FormalConjectures.Paper.Kurepa
+import FormalConjectures.Paper.PrimeTuples
+import FormalConjectures.Paper.Rupert
+import FormalConjectures.Paper.StrongSensitivityConjecture
+import FormalConjectures.Paper.WeaklyFirstCountable
+import FormalConjectures.Util.Answer
+import FormalConjectures.Util.Answer.Syntax
+import FormalConjectures.Util.Attributes.AMS
+import FormalConjectures.Util.Attributes.Basic
+import FormalConjectures.Util.ForMathlib
+import FormalConjectures.Util.Linters.AMSLinter
+import FormalConjectures.Util.Linters.AnswerLinter
+import FormalConjectures.Util.Linters.AnswerLinterTest
+import FormalConjectures.Util.Linters.CategoryLinter
+import FormalConjectures.Util.Linters.CopyrightLinter
+import FormalConjectures.Util.ProblemImports
+import FormalConjectures.Wikipedia.ABC
+import FormalConjectures.Wikipedia.AgohGiuga
+import FormalConjectures.Wikipedia.Andrica
+import FormalConjectures.Wikipedia.ArtinPrimitiveRootsConjecture
+import FormalConjectures.Wikipedia.BalancedPrimes
+import FormalConjectures.Wikipedia.BatemanHornConjecture
+import FormalConjectures.Wikipedia.BealConjecture
+import FormalConjectures.Wikipedia.BoundedBurnsideProblem
+import FormalConjectures.Wikipedia.BrocardConjecture
+import FormalConjectures.Wikipedia.BrocardProblem
+import FormalConjectures.Wikipedia.Bunyakovsky
+import FormalConjectures.Wikipedia.BusyBeaver
+import FormalConjectures.Wikipedia.CarmichaelTotient
+import FormalConjectures.Wikipedia.Catalan
+import FormalConjectures.Wikipedia.ClassNumberProblem
+import FormalConjectures.Wikipedia.CollatzConjecture
+import FormalConjectures.Wikipedia.CongruentNumber
+import FormalConjectures.Wikipedia.Conway99Graph
+import FormalConjectures.Wikipedia.DeterminantalConjecture
+import FormalConjectures.Wikipedia.Dickson
+import FormalConjectures.Wikipedia.EllipticCurveRank
+import FormalConjectures.Wikipedia.Euclid
+import FormalConjectures.Wikipedia.EulerBrick
+import FormalConjectures.Wikipedia.EulerSumOfPowers
+import FormalConjectures.Wikipedia.Exponentials
+import FormalConjectures.Wikipedia.FeitThompsonPrimeConjecture
+import FormalConjectures.Wikipedia.Fermat
+import FormalConjectures.Wikipedia.FermatCatalanConjecture
+import FormalConjectures.Wikipedia.FibonacciPrimes
+import FormalConjectures.Wikipedia.Firoozbakht
+import FormalConjectures.Wikipedia.GaussCircleProblem
+import FormalConjectures.Wikipedia.Gilbreath
+import FormalConjectures.Wikipedia.GoldbachConjecture
+import FormalConjectures.Wikipedia.Grimm
+import FormalConjectures.Wikipedia.GromovPolynomialGrowth
+import FormalConjectures.Wikipedia.Hadamard
+import FormalConjectures.Wikipedia.HadwigerNelson
+import FormalConjectures.Wikipedia.Hall
+import FormalConjectures.Wikipedia.HappyEndingProblem
+import FormalConjectures.Wikipedia.HardyLittlewood
+import FormalConjectures.Wikipedia.HerzogSchonheimConjecture
+import FormalConjectures.Wikipedia.InscribedSquare
+import FormalConjectures.Wikipedia.InvariantSubspaceProblem
+import FormalConjectures.Wikipedia.InverseGalois
+import FormalConjectures.Wikipedia.Irrational
+import FormalConjectures.Wikipedia.JacobianConjecture
+import FormalConjectures.Wikipedia.JugglerConjecture
+import FormalConjectures.Wikipedia.Kakeya
+import FormalConjectures.Wikipedia.Kaplansky
+import FormalConjectures.Wikipedia.Koethe
+import FormalConjectures.Wikipedia.KummerVandiver
+import FormalConjectures.Wikipedia.LegendreConjecture
+import FormalConjectures.Wikipedia.LehmerMahlerMeasureProblem
+import FormalConjectures.Wikipedia.LehmerTotient
+import FormalConjectures.Wikipedia.LeinsterGroup
+import FormalConjectures.Wikipedia.Lemoine
+import FormalConjectures.Wikipedia.LittlewoodConjecture
+import FormalConjectures.Wikipedia.LonelyRunnerConjecture
+import FormalConjectures.Wikipedia.MagicSquareOfSquares
+import FormalConjectures.Wikipedia.Mahler32
+import FormalConjectures.Wikipedia.Mandelbrot
+import FormalConjectures.Wikipedia.MeanValueProblem
+import FormalConjectures.Wikipedia.Mersenne
+import FormalConjectures.Wikipedia.MinimalOverlapProblem
+import FormalConjectures.Wikipedia.ModularityConjecture
+import FormalConjectures.Wikipedia.MoserWorm
+import FormalConjectures.Wikipedia.NoetherProblem
+import FormalConjectures.Wikipedia.Oppermann
+import FormalConjectures.Wikipedia.PebblingNumberConjecture
+import FormalConjectures.Wikipedia.Pell
+import FormalConjectures.Wikipedia.PierceBirkhoff
+import FormalConjectures.Wikipedia.PollocksConjecture
+import FormalConjectures.Wikipedia.PrimesAndPerfectSquares
+import FormalConjectures.Wikipedia.RamanujanTau
+import FormalConjectures.Wikipedia.RationalDistanceProblem
+import FormalConjectures.Wikipedia.RegularPrimes
+import FormalConjectures.Wikipedia.RiemannZetaValues
+import FormalConjectures.Wikipedia.Schanuel
+import FormalConjectures.Wikipedia.Schinzel
+import FormalConjectures.Wikipedia.Selfridge
+import FormalConjectures.Wikipedia.Sendov
+import FormalConjectures.Wikipedia.Singmaster
+import FormalConjectures.Wikipedia.SnakeInTheBox
+import FormalConjectures.Wikipedia.SparseRuler
+import FormalConjectures.Wikipedia.SquarePacking
+import FormalConjectures.Wikipedia.SumOfThreeCubes
+import FormalConjectures.Wikipedia.Toronto
+import FormalConjectures.Wikipedia.Transcendental
+import FormalConjectures.Wikipedia.TwinPrimes
+import FormalConjectures.Wikipedia.UnionClosed
+import FormalConjectures.Wikipedia.VaughtConjecture
+import FormalConjectures.Wikipedia.WallSunSun
+import FormalConjectures.Wikipedia.WolstenholmePrime
+import FormalConjectures.Wikipedia.WoodalPrimes
+import FormalConjectures.Wikipedia.conjecture_1_3_to_2_3
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture1
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture19
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture2
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture3
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture34
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture4
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture40
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture5
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture58
+import FormalConjectures.WrittenOnTheWallII.GraphConjecture6
+import FormalConjectures.WrittenOnTheWallII.Test
diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md
index af038b74..2ab0940f 100644
--- a/Benchmarks/CompileFC/README.md
+++ b/Benchmarks/CompileFC/README.md
@@ -1,11 +1,16 @@
 # CompileFC
 
-Runs the Ix compiler over the Lean environment of https://github.com/google-deepmind/formal-conjectures.
+Runs the Ix compiler over the Lean environment of all defs from https://github.com/google-deepmind/formal-conjectures.
 
-Uses Lean v4.22.0 to match the formal-conjectures project, hence the separate project.
+The defs in CompileFC.lean were generated automatically with the following:
+```
+lake update
+cd .lake/packages/formal_conjectures
+lake exe mk_all --lib FormalConjectures
+mv FormalConjectures.lean ../../../CompileFC.lean
+```
 
-> [!NOTE]
-> Doesn't build with lean4-nix v4.22.0 with the lake dev shell due to changes in `.lake` behavior
+Uses Lean v4.22.0 to match the formal-conjectures project, hence the separate project.
 
 ## Usage
 
diff --git a/Benchmarks/CompileFC/lean-toolchain b/Benchmarks/CompileFC/lean-toolchain
index 2654c20b..6ac6d4c4 100644
--- a/Benchmarks/CompileFC/lean-toolchain
+++ b/Benchmarks/CompileFC/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
\ No newline at end of file
+leanprover/lean4:v4.22.0

From 0aeba7259dad315d271ae5c54e1a1dcc52e2db56 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 16:42:03 -0500
Subject: [PATCH 18/21] Fix FLT/FC caching

---
 .github/workflows/compile.yml | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 4a5b1667..4444093b 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -15,7 +15,6 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  BUILD_ARGS: "--wfail -v"
   COMPILE_DIR: Benchmarks/Compile
 
 jobs:
@@ -28,7 +27,7 @@ jobs:
           shared-key: "ix"
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "ix ${{ env.BUILD_ARGS }}"
+          build-args: "ix --wfail -v"
           test: false
 
   run-compiler:
@@ -36,6 +35,11 @@ jobs:
     strategy:
       matrix:
         bench: [InitStd, Lean, Mathlib, FLT, FC]
+        include:
+          - bench: FLT
+            cache_pkg: flt
+          - bench: FC
+            cache_pkg: formal_conjectures
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
@@ -54,18 +58,22 @@ jobs:
           key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
           restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
       - if: matrix.bench == 'FC'
-        run: echo "COMPILE_DIR=Benchmarks/CompileFC" | tee -a $GITHUB_ENV
+        run: echo "COMPILE_DIR=${{env.COMPILE_DIR}}FC" | tee -a $GITHUB_ENV
+      # Download elan and fetch mathlib cache
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: ${{ env.COMPILE_DIR }}
+          build: false
+          use-github-cache: false 
       # FLT and FC take a few minutes to rebuild, so we cache the build artifacts
-      - if: matrix.bench == 'FLT' || matrix.bench == 'FC'
+      - if: matrix.cache_pkg
         uses: actions/cache@v4
         with:
-          path: ${{ env.COMPILE_DIR }}/.lake/packages/flt/.lake/build
-          key: ${{ matrix.bench }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
+          path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build
+          key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
       # Build the input library
-      - uses: leanprover/lean-action@v1
-        with:
-          build-args: "Compile${{ matrix.bench }} ${{ env.BUILD_ARGS }}"
-          lake-package-directory: ${{ env.COMPILE_DIR }}
-          use-github-cache: false
+      - run: lake build Compile${{ matrix.bench }}
+        working-directory: ${{ env.COMPILE_DIR }}
       # Run the `ix` compiler over the input library
+      # Allow warnings due to copyright notice in formal-conjectures
       - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean

From 4862c2c190d0c23a106c0d0c57e73fb08ef96c05 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 17:03:37 -0500
Subject: [PATCH 19/21] Cache ix binary and remove broken CompileFC for now

---
 .github/workflows/compile.yml | 30 +++++++++++++-----------------
 .github/workflows/nix.yml     |  5 +++--
 2 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 4444093b..bdd71d4c 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -29,34 +29,30 @@ jobs:
         with:
           build-args: "ix --wfail -v"
           test: false
+      - run: echo | lake run install
+      - uses: actions/cache/save@v4
+        with:
+          path: ~/.local/bin/ix
+          key: ix-${{ github.sha }}
 
   run-compiler:
     needs: build
     strategy:
       matrix:
-        bench: [InitStd, Lean, Mathlib, FLT, FC]
+        bench: [InitStd, Lean, Mathlib, FLT] # Add FC once updated to Lean v4.26.0
         include:
           - bench: FLT
             cache_pkg: flt
-          - bench: FC
-            cache_pkg: formal_conjectures
+          # - bench: FC
+          #   cache_pkg: formal_conjectures
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
-      - uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "ix"
-          save-if: "false"
-      - name: Set cache keys
-        run: |
-          ROOT="lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}"
-          echo "ROOT_CACHE_PREFIX=$ROOT" | tee -a $GITHUB_ENV
-      # Restore cached `ix` build from prior step
       - uses: actions/cache/restore@v4
         with:
-          path: ./.lake
-          key: ${{ env.ROOT_CACHE_PREFIX }}-${{ github.sha }}
-          restore-keys: ${{ env.ROOT_CACHE_PREFIX }}
+          path: ~/.local/bin/ix
+          key: ix-${{ github.sha }}
+      - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
       - if: matrix.bench == 'FC'
         run: echo "COMPILE_DIR=${{env.COMPILE_DIR}}FC" | tee -a $GITHUB_ENV
       # Download elan and fetch mathlib cache
@@ -72,8 +68,8 @@ jobs:
           path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build
           key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
       # Build the input library
+      # Allow warnings due to copyright notice in formal-conjectures
       - run: lake build Compile${{ matrix.bench }}
         working-directory: ${{ env.COMPILE_DIR }}
       # Run the `ix` compiler over the input library
-      # Allow warnings due to copyright notice in formal-conjectures
-      - run: lake exe ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean
+      - run: ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index e39dc4be..cb4d4747 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -33,8 +33,9 @@ jobs:
       - run: nix build .#bench-shardmap --print-build-logs --accept-flake-config
       # Ix tests
       - run: nix run .#test --accept-flake-config
-      - run: nix run .#test-aiur --accept-flake-config
-      - run: nix run .#test-ixvm --accept-flake-config
+      # Expensive tests are only built in Nix to save time
+      - run: nix build .#test-aiur --accept-flake-config
+      - run: nix build .#test-ixvm --accept-flake-config
 
   # Tests Nix devShell support on Ubuntu
   nix-devshell:

From 478890aefcbe3bd11d465f5d6c38bb2ccb1114d6 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 17:08:40 -0500
Subject: [PATCH 20/21] Fixup

---
 .github/workflows/compile.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index bdd71d4c..3908b2bf 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -23,13 +23,13 @@ jobs:
     steps:
       - uses: actions/checkout@v6
       - uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "ix"
       - uses: leanprover/lean-action@v1
         with:
           build-args: "ix --wfail -v"
           test: false
-      - run: echo | lake run install
+      - run: |
+          mkdir -p ~/.local/bin
+          echo | lake run install
       - uses: actions/cache/save@v4
         with:
           path: ~/.local/bin/ix

From ce3e69970513b0dba16e9eb8a11e1b9affe2c726 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 11 Feb 2026 17:44:59 -0500
Subject: [PATCH 21/21] Cleanup

---
 .github/workflows/ci.yml       |  1 -
 .github/workflows/compile.yml  | 10 ++++++----
 Benchmarks/CompileFC/README.md |  3 +++
 Ix/Common.lean                 |  2 +-
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a3b8579b..494a9fd9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -30,7 +30,6 @@ jobs:
           ln -sf /opt/homebrew/bin/gcc-14 ~/local/bin/gcc
           export PATH=~/local/bin:$PATH
           which gcc
-      - uses: Swatinem/rust-cache@v2
       - uses: leanprover/lean-action@v1 # https://github.com/leanprover/lean-action
         with:
           build-args: "--wfail -v"
diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 3908b2bf..09cb7857 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -1,10 +1,8 @@
 name: Benchmark Ix compiler
 
 on:
-  schedule:
-    - cron: "0 0 * * *" # nightly
   push:
-    branches: sb/cli
+    branches: main
   workflow_dispatch:
 
 permissions:
@@ -18,6 +16,7 @@ env:
   COMPILE_DIR: Benchmarks/Compile
 
 jobs:
+  # First build and cache the `ix` binary for use in each matrix job
   build:
     runs-on: ubuntu-latest
     steps:
@@ -35,6 +34,7 @@ jobs:
           path: ~/.local/bin/ix
           key: ix-${{ github.sha }}
 
+  # Run the Ix compiler over each library env in Benchmarks/Compile
   run-compiler:
     needs: build
     strategy:
@@ -48,6 +48,7 @@ jobs:
     runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
+      # Restore cached `ix` binary
       - uses: actions/cache/restore@v4
         with:
           path: ~/.local/bin/ix
@@ -71,5 +72,6 @@ jobs:
       # Allow warnings due to copyright notice in formal-conjectures
       - run: lake build Compile${{ matrix.bench }}
         working-directory: ${{ env.COMPILE_DIR }}
-      # Run the `ix` compiler over the input library
+      # Run the `ix` compiler over the input library env
       - run: ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean
+
diff --git a/Benchmarks/CompileFC/README.md b/Benchmarks/CompileFC/README.md
index 2ab0940f..ecc37f2d 100644
--- a/Benchmarks/CompileFC/README.md
+++ b/Benchmarks/CompileFC/README.md
@@ -1,5 +1,8 @@
 # CompileFC
 
+> [!NOTE]
+> This project does not currently work with Ix as the Lean version is out of date.
+
 Runs the Ix compiler over the Lean environment of all defs from https://github.com/google-deepmind/formal-conjectures.
 
 The defs in CompileFC.lean were generated automatically with the following:
diff --git a/Ix/Common.lean b/Ix/Common.lean
index 808bccd2..2004aef5 100644
--- a/Ix/Common.lean
+++ b/Ix/Common.lean
@@ -304,7 +304,7 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do
 end Lean
 
 /-- Format a duration in milliseconds with appropriate unit suffix.
-- `0` → `"< 1ms"` (sub-ms precision not available with `Nat` ms)
+- `0` → `"< 1ms"`
 - `1`–`999` → `"Xms"`
 - `≥ 1000` → `"X.XXs"` (rounded to two decimal places) -/
 def Nat.formatMs (ms : Nat) : String :=