feat: Add ix compile CLI and CI benchmarks

.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

.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
+

.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:

.gitignore

@@ -1,5 +1,5 @@
 # Lean
-/.lake
+**/.lake
 
 # Rust
 /target

Benchmarks/Compile/CompileFLT.lean

@@ -0,0 +1,2 @@
+import FLT
+

ix_test/IxTest.lean → 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

Benchmarks/Compile/CompileLean.lean

@@ -0,0 +1 @@
+import Lean

Benchmarks/Compile/CompileMathlib.lean

@@ -0,0 +1 @@
+import Mathlib

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.

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"}

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"

Benchmarks/Compile/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.26.0

Benchmarks/CompileFC/.envrc

@@ -0,0 +1 @@
+use flake