Remove -Kenv=dev and specified lean toolchain

lean-dojo · Dec 6, 2023 · bb05f1f · bb05f1f
1 parent 5d514e5
commit bb05f1f
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 8 deletions.
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -18,13 +18,13 @@ jobs:
         with:
           fetch-depth: 0
       - name: Set up elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
       - name: Build project
-        run: ~/.elan/bin/lake -Kenv=dev build
+        run: ~/.elan/bin/lake build
       - name: Download model
-        run: ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download
+        run: ~/.elan/bin/lake script run LeanInfer/download
       - name: Build tests
-        run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests
+        run: ~/.elan/bin/lake build LeanInferTests
   test_external:
     needs: build
     runs-on: ${{ matrix.os }}
@@ -34,7 +34,7 @@ jobs:
     name: Test external
     steps:
       - name: Set up elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
       - name: Get lean4-example
         run: |
           git clone https://github.com/yangky11/lean4-example
@@ -43,5 +43,5 @@ jobs:
       - name: Build lean4-example
         run: |
           cd lean4-example
-          ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download
-          ~/.elan/bin/lake -Kenv=dev build
+          ~/.elan/bin/lake script run LeanInfer/download
+          ~/.elan/bin/lake build
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,3 @@
-/build
 /lake-packages/*
 /.lake
-Original file line number
+Diff line change
@@ -1,4 +1,3 @@
-    /build
     /lake-packages/*
     /.lake
@@ Expand Down @@