From 44adfe938d67fac54948dad46a3fa06634f2ccc7 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 19:31:06 -0800 Subject: [PATCH 01/11] Set up CI --- .github/workflows/push.yml | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 .github/workflows/push.yml diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml new file mode 100644 index 0000000..b99c2b1 --- /dev/null +++ b/.github/workflows/push.yml @@ -0,0 +1,29 @@ +name: CI + +on: + push: + branches: + - main + +jobs: + build: + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + name: Build + steps: + - name: Checkout project + uses: actions/checkout@v2 + with: + fetch-depth: 0 + - name: Set up elan + run: | + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y + source $HOME/.elan/env + - name: Build project + run: lake build + - name: Download model + run: lake script run LeanInfer/download + - name: Build tests + run: lake build LeanInferTests \ No newline at end of file From acf6003550295a75e6ebbb61b25c8e7c900994d0 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 19:43:06 -0800 Subject: [PATCH 02/11] Try to fix lake not found error --- .github/workflows/push.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index b99c2b1..167ce57 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -19,8 +19,9 @@ jobs: fetch-depth: 0 - name: Set up elan run: | - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y - source $HOME/.elan/env + # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y + # source $HOME/.elan/env + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Build project run: lake build - name: Download model From dcf3dccb270912b6b8f89260606fc1d90255284e Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 19:46:39 -0800 Subject: [PATCH 03/11] Try to fix lake not found error --- .github/workflows/push.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 167ce57..dfbf9c8 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -23,7 +23,7 @@ jobs: # source $HOME/.elan/env curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Build project - run: lake build + run: ~/.elan/bin/lake -Kenv=dev build - name: Download model run: lake script run LeanInfer/download - name: Build tests From c78f2c0715929bd725de01a5f775a9b7a7669b26 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 19:53:26 -0800 Subject: [PATCH 04/11] Try to fix lake not found error --- .github/workflows/push.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index dfbf9c8..e5cbc6d 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -25,6 +25,6 @@ jobs: - name: Build project run: ~/.elan/bin/lake -Kenv=dev build - name: Download model - run: lake script run LeanInfer/download + run: ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download - name: Build tests - run: lake build LeanInferTests \ No newline at end of file + run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests \ No newline at end of file From 1bc0612927b8a8dd11c34c7d88fa9cadd6f1673b Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 20:12:10 -0800 Subject: [PATCH 05/11] Fix all error --- .github/workflows/push.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index e5cbc6d..585e6c4 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -19,8 +19,6 @@ jobs: fetch-depth: 0 - name: Set up elan run: | - # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y - # source $HOME/.elan/env curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 - name: Build project run: ~/.elan/bin/lake -Kenv=dev build From 5b3c7278fbd00181310648a61e1b12a8c0566dbd Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 20:49:54 -0800 Subject: [PATCH 06/11] Ubuntu only --- .github/workflows/push.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 585e6c4..aec9543 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -10,7 +10,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-latest, macos-latest] + os: [ubuntu-latest] name: Build steps: - name: Checkout project From b9f83ab3653b15f96dd8d5dc251048baf27da9c5 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sun, 3 Dec 2023 21:03:34 -0800 Subject: [PATCH 07/11] Ubuntu and macos --- .github/workflows/push.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index aec9543..585e6c4 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -10,7 +10,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-latest] + os: [ubuntu-latest, macos-latest] name: Build steps: - name: Checkout project From da1537bc5007c611f21cf08b30fb21a768c9043a Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Mon, 4 Dec 2023 18:24:23 -0800 Subject: [PATCH 08/11] Add CI checking external projects --- .github/workflows/push.yml | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 585e6c4..9cc252c 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -18,11 +18,34 @@ 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 --default-toolchain leanprover/lean4:4.0.0 - name: Build project run: ~/.elan/bin/lake -Kenv=dev build - name: Download model run: ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download - name: Build tests - run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests \ No newline at end of file + run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests + test_external: + needs: build + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + name: Test external + steps: + - name: Checkout project + uses: actions/checkout@v2 + 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 + - name: Get lean4-example + run: | + git clone https://github.com/yangky11/lean4-example /workspaces/lean4-example + cd /workspaces/lean4-example + git checkout LeanInfer-demo + - name: Build lean4-example + run: | + cd /workspaces/lean4-example + ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download + ~/.elan/bin/lake -Kenv=dev build \ No newline at end of file From bb519d71a12b5e268255b7f1bee2fa07def62522 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Mon, 4 Dec 2023 18:40:44 -0800 Subject: [PATCH 09/11] Fix permission denied for workspace folder --- .github/workflows/push.yml | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 9cc252c..1f48fb5 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -7,10 +7,11 @@ on: jobs: build: - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [ubuntu-latest, macos-latest] + runs-on: ubuntu-latest + # runs-on: ${{ matrix.os }} + # strategy: + # matrix: + # os: [ubuntu-latest, macos-latest] name: Build steps: - name: Checkout project @@ -27,25 +28,22 @@ jobs: run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests test_external: needs: build - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [ubuntu-latest, macos-latest] + runs-on: ubuntu-latest name: Test external steps: - - name: Checkout project - uses: actions/checkout@v2 - with: - fetch-depth: 0 + # - name: Checkout project + # uses: actions/checkout@v2 + # 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 - name: Get lean4-example run: | - git clone https://github.com/yangky11/lean4-example /workspaces/lean4-example - cd /workspaces/lean4-example + git clone https://github.com/yangky11/lean4-example + cd lean4-example git checkout LeanInfer-demo - name: Build lean4-example run: | - cd /workspaces/lean4-example + cd lean4-example ~/.elan/bin/lake -Kenv=dev script run LeanInfer/download ~/.elan/bin/lake -Kenv=dev build \ No newline at end of file From 5d514e5e75aa1f38e44ec895b7c3b60b852b8100 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Mon, 4 Dec 2023 18:52:30 -0800 Subject: [PATCH 10/11] Finish 2 CI jobs --- .github/workflows/push.yml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 1f48fb5..de58fc4 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -7,11 +7,10 @@ on: jobs: build: - runs-on: ubuntu-latest - # runs-on: ${{ matrix.os }} - # strategy: - # matrix: - # os: [ubuntu-latest, macos-latest] + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] name: Build steps: - name: Checkout project @@ -28,13 +27,12 @@ jobs: run: ~/.elan/bin/lake -Kenv=dev build LeanInferTests test_external: needs: build - runs-on: ubuntu-latest + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] name: Test external steps: - # - name: Checkout project - # uses: actions/checkout@v2 - # 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 - name: Get lean4-example From bb05f1f0884239cd938edad7c6671605bc009041 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 6 Dec 2023 09:24:40 -0800 Subject: [PATCH 11/11] 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