chore: bump Lean to v4.17.0 (#8)

Extra:
* Overwrite `BLAKE3_USE_NEON=0` and ignore `blake3_neon.c`
* Tag `Blake3Test` as the test driver
* tag `Blake3` lib as the default target for `lake build`
* Use `lean-action` for CI

Author: arthurpaulino

.github/workflows/ci.yml

@@ -6,15 +6,10 @@ on:
       - main
 jobs:
   build:
-    name: Build
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - uses: actions/checkout@v4
-      - name: Run Blake3Test
-        run: lake exe Blake3Test
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: "--wfail"
+          test: true

Blake3Test.lean

@@ -11,5 +11,5 @@ abbrev output : ByteArray := ⟨#[
 def main : IO UInt32 := do
   println! s!"BLAKE3 version: {Blake3.version}"
   if (Blake3.hash input).val.data != output.data
-    then IO.println "BLAKE3 test failed"; return 1
-    else IO.println "BLAKE3 test succeeded"; return 0
+    then IO.eprintln "BLAKE3 test failed";    return 1
+    else IO.println  "BLAKE3 test succeeded"; return 0

lakefile.lean

@@ -4,8 +4,10 @@ open Lake DSL
 
 package Blake3
 
+@[default_target]
 lean_lib Blake3
 
+@[test_driver]
 lean_exe Blake3Test
 
 abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3"
@@ -27,38 +29,41 @@ target cloneBlake3 pkg : GitRepo := do
 def blake3CDir (blake3Repo : GitRepo) : System.FilePath :=
   blake3Repo.dir / "c"
 
-abbrev blake3Flags : Array String :=
-  #["-DBLAKE3_NO_SSE2", "-DBLAKE3_NO_SSE41", "-DBLAKE3_NO_AVX2", "-DBLAKE3_NO_AVX512"]
+abbrev blake3Flags : Array String := #[
+    "-DBLAKE3_NO_SSE2",
+    "-DBLAKE3_NO_SSE41",
+    "-DBLAKE3_NO_AVX2",
+    "-DBLAKE3_NO_AVX512",
+    "-DBLAKE3_USE_NEON=0"
+  ]
 
 abbrev compiler := "cc"
 
-def buildBlake3Obj (pkg : Package) (fileName : String) (addFlags : Bool) := do
+def buildBlake3Obj (pkg : Package) (fileName : String) := do
   let blake3Repo ← cloneBlake3.fetch >>= (·.await)
   let cDir := blake3CDir blake3Repo
   let srcJob ← inputTextFile $ cDir / fileName |>.addExtension "c"
   let oFile := pkg.buildDir / fileName |>.addExtension "o"
   let includeArgs := #["-I", cDir.toString]
-  let weakArgs := if addFlags then includeArgs ++ blake3Flags else includeArgs
+  let weakArgs := includeArgs ++ blake3Flags
   buildO oFile srcJob weakArgs #[] compiler getLeanTrace
 
 target ffi.o pkg : System.FilePath := do
   let blake3Repo ← cloneBlake3.fetch >>= (·.await)
   let oFile := pkg.buildDir / "ffi.o"
   let srcJob ← inputTextFile $ pkg.dir / "ffi.c"
-  let includeDir ← getLeanIncludeDir
+  let leanIncludeDir ← getLeanIncludeDir
   let cDir := blake3CDir blake3Repo
-  let weakArgs := #["-I", includeDir.toString, "-I", cDir.toString]
+  let weakArgs := #["-I", leanIncludeDir.toString, "-I", cDir.toString]
   buildO oFile srcJob weakArgs #[] compiler getLeanTrace
 
 extern_lib ffi pkg := do
   -- Gather all `.o` file build jobs
-  let mut oFileJobs := #[]
-  oFileJobs := oFileJobs.push $ ← buildBlake3Obj pkg "blake3" false
-  oFileJobs := oFileJobs.push $ ← buildBlake3Obj pkg "blake3_dispatch" true
-  oFileJobs := oFileJobs.push $ ← buildBlake3Obj pkg "blake3_portable" true
-  if (← IO.getEnv "BLAKE3_USE_NEON") == some "1" then
-    oFileJobs := oFileJobs.push $ ← buildBlake3Obj pkg "blake3_neon" true
-  oFileJobs := oFileJobs.push $ ← ffi.o.fetch
+  let blake3O ← buildBlake3Obj pkg "blake3"
+  let blake3DispatchO ← buildBlake3Obj pkg "blake3_dispatch"
+  let blake3PortableO ← buildBlake3Obj pkg "blake3_portable"
+  let ffiO ← ffi.o.fetch
+  let oFileJobs := #[blake3O, blake3DispatchO, blake3PortableO, ffiO]
 
   let name := nameToStaticLib "ffi"
   buildStaticLib (pkg.nativeLibDir / name) oFileJobs

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.16.0
+leanprover/lean4:v4.17.0