chore: bump Lean to v4.17.0

Extra: * Set the `LSpec` lib as the default target * Add a CI config to run `lean-action`
argumentcomputer · Mar 3, 2025 · 2425e0f · 2425e0f
1 parent fc8f902
commit 2425e0f
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 2 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -0,0 +1,14 @@
+name: "CI"
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "--wfail"
diff --git a/lakefile.toml b/lakefile.toml
@@ -1,6 +1,6 @@
 name = "LSpec"
 version = "2.0.0"
-defaultTargets = ["lspec"]
+defaultTargets = ["LSpec"]
 
 [[lean_lib]]
 name = "LSpec"
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0
+leanprover/lean4:v4.17.0