From bb05f1f0884239cd938edad7c6671605bc009041 Mon Sep 17 00:00:00 2001
From: Peiyang-Song <p_song@ucsb.edu>
Date: Wed, 6 Dec 2023 09:24:40 -0800
Subject: [PATCH] Remove -Kenv=dev and specified lean toolchain

---
 .github/workflows/push.yml | 14 +++++++-------
 .gitignore                 |  1 -
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index de58fc4..a7e52a2 100644
--- 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
\ No newline at end of file
+          ~/.elan/bin/lake script run LeanInfer/download
+          ~/.elan/bin/lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 9366b53..22dc57e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,3 @@
-/build
 /lake-packages/*
 /.lake