Update versions and add top-level CI

.github/workflows/lean.yml

@@ -0,0 +1,42 @@
+name: Lean CI
+
+on:
+  push:
+    branches: main
+    paths:
+      - 'lean/**'
+      - '.github/workflows/lean.yml'
+  pull_request:
+    paths:
+      - 'lean/**'
+      - '.github/workflows/lean.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: lean
+          build-args: "--wfail -v"
+
+  nix-test:
+    name: Nix Tests
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: lean
+    steps:
+      - uses: actions/checkout@v6
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - run: nix build --print-build-logs --accept-flake-config
+      - run: nix run .#lean-bin --print-build-logs --accept-flake-config

.github/workflows/rust.yml

@@ -0,0 +1,75 @@
+name: Rust CI
+
+on:
+  push:
+    branches: main
+    paths:
+      - 'rust/**'
+      - '.github/workflows/rust.yml'
+  pull_request:
+    paths:
+      - 'rust/**'
+      - '.github/workflows/rust.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+defaults:
+  run:
+    working-directory: rust
+
+jobs:
+  linux-test:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - name: Get Rust toolchain channel
+        id: rust-tc
+        run: echo "channel=$(awk -F '\"' '/^channel/ {print $2}' rust-toolchain.toml)" >> "$GITHUB_OUTPUT"
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+        with:
+          toolchain: ${{ steps.rust-tc.outputs.channel }}
+          cache-workspaces: rust
+      - uses: taiki-e/install-action@nextest
+      - name: Linux Tests
+        run: cargo nextest run --profile ci --workspace
+
+  lints:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - name: Get Rust toolchain channel
+        id: rust-tc
+        run: echo "channel=$(awk -F '\"' '/^channel/ {print $2}' rust-toolchain.toml)" >> "$GITHUB_OUTPUT"
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+        with:
+          toolchain: ${{ steps.rust-tc.outputs.channel }}
+          components: rustfmt, clippy
+          cache-workspaces: rust
+      - name: Check Rustfmt code style
+        run: cargo fmt --all -- --check
+      - name: Check *everything* compiles
+        run: cargo check --all-targets --all-features --workspace
+      - name: Check clippy lints
+        run: cargo clippy --workspace --all-targets --all-features -- -D warnings
+      - name: Doctests
+        run: cargo test --doc --workspace
+      - name: Cargo-deny
+        uses: EmbarkStudios/cargo-deny-action@v2
+        with:
+          manifest-path: rust/Cargo.toml
+          rust-version: ${{ steps.rust-tc.outputs.channel }}
+
+  nix-test:
+    name: Nix Tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - run: nix build --print-build-logs --accept-flake-config
+      - run: nix flake check --print-build-logs --accept-flake-config

lean/.github/workflows/lean_action_ci.yml

@@ -14,8 +14,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail -v"
-          #test: true

lean/.github/workflows/nix.yml

@@ -17,7 +17,7 @@ jobs:
     name: Nix Tests
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: cachix/install-nix-action@v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable

lean/flake.nix

@@ -1,33 +1,35 @@
 {
   description = "Lean Nix flake";
 
-  nixConfig = {
-    extra-substituters = [
-      "https://cache.garnix.io"
-    ];
-    extra-trusted-public-keys = [
-      "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g="
-    ];
-  };
+  # First enable Garnix GH App for the repo
+  # nixConfig = {
+  #   extra-substituters = [
+  #     "https://cache.garnix.io"
+  #   ];
+  #   extra-trusted-public-keys = [
+  #     "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g="
+  #   ];
+  # };
 
   inputs = {
     # System packages
     nixpkgs.follows = "lean4-nix/nixpkgs";
 
     # Lean 4 & Lake
-    lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=7653ecd6d80710f42fcc2c117144698b18acdfc1";
+    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;} {
+  outputs =
+    inputs@{
+      nixpkgs,
+      flake-parts,
+      lean4-nix,
+      ...
+    }:
+    flake-parts.lib.mkFlake { inherit inputs; } {
       # Systems we want to build for
       systems = [
         "aarch64-darwin"
@@ -36,50 +38,55 @@
         "x86_64-linux"
       ];
 
-      perSystem = {
-        system,
-        pkgs,
-        ...
-      }: let
-        lake2nix = pkgs.callPackage lean4-nix.lake {};
-        lakeArgs = {
-          src = ./.;
-        };
-        lakeDeps = lake2nix.buildDeps lakeArgs;
-        lakeBuildArgs =
-          lakeArgs
-          // {
+      perSystem =
+        {
+          system,
+          pkgs,
+          ...
+        }:
+        let
+          lake2nix = pkgs.callPackage lean4-nix.lake { };
+          lakeArgs = {
+            src = ./.;
+          };
+          lakeDeps = lake2nix.buildDeps lakeArgs;
+          lakeBuildArgs = lakeArgs // {
             inherit lakeDeps;
           };
-        leanLib = lake2nix.mkPackage (lakeBuildArgs
-          // {
-            name = "Template";
-            buildLibrary = true;
-          });
-        leanBin = lake2nix.mkPackage (lakeBuildArgs
-          // {
-            lakeArtifacts = leanLib;
-            installArtifacts = false;
-            name = "template";
-          });
-      in {
-        # Lean overlay
-        _module.args.pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
+          leanLib = lake2nix.mkPackage (
+            lakeBuildArgs
+            // {
+              name = "Template";
+              buildLibrary = true;
+            }
+          );
+          leanBin = lake2nix.mkPackage (
+            lakeBuildArgs
+            // {
+              lakeArtifacts = leanLib;
+              installArtifacts = false;
+              name = "template";
+            }
+          );
+        in
+        {
+          # Lean overlay
+          _module.args.pkgs = import nixpkgs {
+            inherit system;
+            overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+          };
 
-        packages = {
-          default = leanLib;
-          lean-bin = leanBin;
-        };
+          packages = {
+            default = leanLib;
+            lean-bin = leanBin;
+          };
 
-        # Provide a unified dev shell with Lean + Rust
-        devShells.default = pkgs.mkShell {
-          packages = with pkgs; [
-            lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
-          ];
+          # Provide a unified dev shell with Lean + Rust
+          devShells.default = pkgs.mkShell {
+            packages = with pkgs; [
+              lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
+            ];
+          };
         };
-      };
     };
 }

lean/lean-toolchain

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