diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4a5ba48c..494a9fd9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -77,6 +77,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
new file mode 100644
index 00000000..09cb7857
--- /dev/null
+++ b/.github/workflows/compile.yml
@@ -0,0 +1,77 @@
+name: Benchmark Ix compiler
+
+on:
+  push:
+    branches: main
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+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:
+      - uses: actions/checkout@v6
+      - uses: Swatinem/rust-cache@v2
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "ix --wfail -v"
+          test: false
+      - run: |
+          mkdir -p ~/.local/bin
+          echo | lake run install
+      - uses: actions/cache/save@v4
+        with:
+          path: ~/.local/bin/ix
+          key: ix-${{ github.sha }}
+
+  # Run the Ix compiler over each library env in Benchmarks/Compile
+  run-compiler:
+    needs: build
+    strategy:
+      matrix:
+        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
+    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
+          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
+      - 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.cache_pkg
+        uses: actions/cache@v4
+        with:
+          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 env
+      - 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:
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/CompileFLT.lean b/Benchmarks/Compile/CompileFLT.lean
new file mode 100644
index 00000000..0b3e4b4d
--- /dev/null
+++ b/Benchmarks/Compile/CompileFLT.lean
@@ -0,0 +1,2 @@
+import FLT
+
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/CompileLean.lean b/Benchmarks/Compile/CompileLean.lean
new file mode 100644
index 00000000..78c878a7
--- /dev/null
+++ b/Benchmarks/Compile/CompileLean.lean
@@ -0,0 +1 @@
+import Lean
diff --git a/Benchmarks/Compile/CompileMathlib.lean b/Benchmarks/Compile/CompileMathlib.lean
new file mode 100644
index 00000000..0b4be76b
--- /dev/null
+++ b/Benchmarks/Compile/CompileMathlib.lean
@@ -0,0 +1 @@
+import Mathlib
diff --git a/Benchmarks/Compile/README.md b/Benchmarks/Compile/README.md
new file mode 100644
index 00000000..1e38c800
--- /dev/null
+++ b/Benchmarks/Compile/README.md
@@ -0,0 +1,14 @@
+# Compile
+
+Test libraries for the Ix compiler
+
+- [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 `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/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json
new file mode 100644
index 00000000..18d2be9a
--- /dev/null
+++ b/Benchmarks/Compile/lake-manifest.json
@@ -0,0 +1,115 @@
+{"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"},
+  {"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"}],
+ "name": "Compile",
+ "lakeDir": ".lake"}
diff --git a/Benchmarks/Compile/lakefile.toml b/Benchmarks/Compile/lakefile.toml
new file mode 100644
index 00000000..6b117f4b
--- /dev/null
+++ b/Benchmarks/Compile/lakefile.toml
@@ -0,0 +1,25 @@
+name = "Compile"
+version = "0.1.0"
+defaultTargets = ["CompileInitStd"]
+
+[[lean_lib]]
+name = "CompileInitStd"
+
+[[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"
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/.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
new file mode 100644
index 00000000..ed4c3e47
--- /dev/null
+++ b/Benchmarks/CompileFC/CompileFC.lean
@@ -0,0 +1,565 @@
+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
new file mode 100644
index 00000000..ecc37f2d
--- /dev/null
+++ b/Benchmarks/CompileFC/README.md
@@ -0,0 +1,20 @@
+# 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:
+```
+lake update
+cd .lake/packages/formal_conjectures
+lake exe mk_all --lib FormalConjectures
+mv FormalConjectures.lean ../../../CompileFC.lean
+```
+
+Uses Lean v4.22.0 to match the formal-conjectures project, hence the separate project.
+
+## Usage
+
+`ix compile --path /path/to/CompileFC.lean`
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..57b04053
--- /dev/null
+++ b/Benchmarks/CompileFC/flake.nix
@@ -0,0 +1,53 @@
+{
+  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,
+        ...
+      }: {
+        # 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..0e2f81c9
--- /dev/null
+++ b/Benchmarks/CompileFC/lakefile.toml
@@ -0,0 +1,11 @@
+name = "CompileFC"
+version = "0.1.0"
+defaultTargets = ["CompileFC"]
+
+[[lean_lib]]
+name = "CompileFC"
+
+[[require]]
+name = "formal_conjectures"
+git = "https://github.com/google-deepmind/formal-conjectures"
+rev = "20af7726bba72fc97d8feda6958a8afacc664ad4"
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/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
new file mode 100644
index 00000000..35196b79
--- /dev/null
+++ b/Ix/Cli/CompileCmd.lean
@@ -0,0 +1,76 @@
+import Cli
+import Ix.Common
+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 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"
+      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}"
+
+  let totalConsts := leanEnv.constants.toList.length
+  println! "Total constants: {totalConsts}"
+
+  let start ← IO.monoMsNow
+  let bytes ← Ix.CompileM.rsCompileEnvBytes leanEnv
+  let elapsed := (← IO.monoMsNow) - start
+
+  println! "Compiled {fmtBytes bytes.size} env in {elapsed.formatMs}"
+  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/Common.lean b/Ix/Common.lean
index 24e5ca86..2004aef5 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"`
+- `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/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/Tests/Cli.lean b/Tests/Cli.lean
index 89e2afce..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"
-  Tests.Cli.run "lake" (#["build"]) (some ixTestDir)
+  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
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
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
           ];
         };
 
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/.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 f434439d..00000000
--- a/ix_test/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:4.23.0