CI を作成するテスト

.github/workflows/ci.yml

@@ -0,0 +1,50 @@
+# see: https://github.com/rami3l/plfl/blob/master/.github/workflows/ci.yml
+
+name: Test
+
+# https://docs.github.com/en/actions/using-jobs/using-concurrency#example-only-cancel-in-progress-jobs-or-runs-for-the-current-workflow
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      # src: https://harry.garrood.me/blog/easy-incremental-haskell-ci-builds-with-ghc-9.4/
+      - name: Cache dependencies
+        uses: actions/cache@v3
+        with:
+          path: |
+            ./lake-packages
+          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: Cache build
+        uses: actions/cache@v3
+        with:
+          path: |
+            ./build
+          key: build-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ github.sha }}
+          restore-keys: |
+            build-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: Test native build
+        run: |
+          lake exe cache get
+          lake build

lakefile.lean

@@ -2,12 +2,15 @@ import Lake
 open Lake DSL
 
 package examples {
-  -- add configuration options here
+  -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355145527
+  moreLeanArgs := #["-DrelaxedAutoImplicit=false"]
+  moreServerArgs := #["-DrelaxedAutoImplicit=false"]
 }
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "96806534a3a47c26cec8985be643f13c2a1b9c92"
 
+@[default_target]
 lean_lib Examples {
   -- add lib config here
 }