feat: Add lake CI

.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

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
       {

lakefile.lean

@@ -2,7 +2,7 @@ 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"]
 }