Merge pull request #6 from Anderssorby/acs/lean-v4.4.0

Use Lean v4.4.0

.github/workflows/build.yml

@@ -0,0 +1,35 @@
+on:
+  push:
+    branches-ignore:
+      # ignore tmp branches used by bors
+      - 'staging.tmp*'
+      - 'trying.tmp*'
+      - 'staging*.tmp'
+  pull_request:
+
+name: ci
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    env:
+      NIX_BUILD_ARGS: -v --print-build-logs --fallback --show-trace
+    steps:
+      - uses: cachix/install-nix-action@v22
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes ca-references
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/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@v3
+      - name: build
+        run: nix develop $NIX_BUILD_ARGS --command lake build SDL
+
+      - name: test SDL
+        run: nix develop $NIX_BUILD_ARGS --command lake build Tests

.gitignore

@@ -2,3 +2,4 @@
 result*
 /build
 /lake-packages/*
+/.lake

flake.nix

@@ -42,10 +42,10 @@
           "${leanPkgs.lean-bin-tools-unwrapped}/include"
         ];
         INCLUDE_PATH = concatStringsSep ":" includes;
-        libs = [
-          "${pkgs.SDL2.out}/lib" "${pkgs.SDL2_image.out}/lib"
-        ];
-        LD_LIBRARY_PATH = concatStringsSep ":" libs;
+        # libs = [
+        #   "${pkgs.SDL2.out}/lib" "${pkgs.SDL2_image.out}/lib"
+        # ];
+        # LD_LIBRARY_PATH = concatStringsSep ":" libs;
         libSDL2 = pkgs.SDL2.out // {
           name = "lib/libSDL2.so";
           linkName = "SDL2";
@@ -102,8 +102,8 @@
             # Where the lean files are located
             src = ./test;
           };
-        joinDepsDerivations = getSubDrv:
-          pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") ([ ] ++ project.allExternalDeps));
+        # joinDepsDerivations = getSubDrv:
+        #   pkgs.lib.concatStringsSep ":" (map (d: "${getSubDrv d}") ([ ] ++ project.allExternalDeps));
         withGdb = bin: pkgs.writeShellScriptBin "${bin.name}-with-gdb" "${pkgs.gdb}/bin/gdb ${bin}/bin/${bin.name}";
       in
       {

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "SDL",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -2,29 +2,28 @@ import Lake
 open Lake DSL
 
 package «SDL» {
-  moreLinkArgs := #["-L./build/lib", "-lsdl2-shim", "-lSDL2", "-lSDL2_image"]
+  moreLinkArgs := #["-L.lake/build/lib", "-lsdl2-shim", "-lSDL2", "-lSDL2_image"]
   extraDepTargets := #["sdl2-shim"]
 }
 
 lean_lib «SDL» {
   srcDir := "src"
-  -- add library configuration options here
 }
 
 def cDir   := "bindings"
 def ffiSrc := "sdl2-shim.c"
 def ffiO   := "sdl2-shim.o"
 def ffiLib := "sdl2-shim"
 
-target ffi.o (pkg : Package) : FilePath := do
+target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / ffiO
   let srcJob ← inputFile <| pkg.dir / cDir / ffiSrc
   buildFileAfterDep oFile srcJob fun srcFile => do
     let flags := #["-I", (← getLeanIncludeDir).toString,
       "-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC"]
     compileO ffiSrc oFile srcFile flags
 
-target «sdl2-shim» (pkg : Package) : FilePath := do
+target «sdl2-shim» pkg : FilePath := do
   let name := nameToStaticLib ffiLib
   let ffiO ← fetch <| pkg.target ``ffi.o
   buildStaticLib (pkg.buildDir / "lib" / name) #[ffiO]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-06
+leanprover/lean4:v4.4.0