From af9ca5ecd59e6298eace6dafc427ce186fc549ce Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 23 Aug 2024 22:08:08 +0200 Subject: [PATCH] modify workflow --- .github/workflows/test.yml | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index c4e50cd..34dc1b0 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -45,14 +45,28 @@ jobs: with: submodules: true - uses: actions/setup-node@v4 - - uses: leanprover/lean-action@v1 - with: - lake-package-directory: "demo/server/LeanProject" - use-mathlib-cache: false - auto-config: false - build: true - test: false - lint: false + # - uses: leanprover/lean-action@v1 + # if: matrix.os != 'windows-latest' + # with: + # lake-package-directory: "demo/server/LeanProject" + # use-mathlib-cache: false + # auto-config: false + # build: true + # test: false + # lint: false + # - name: Install elan (Windows) + # if: matrix.os == 'windows-latest' + # run: | + # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh + # bash elan-init.sh -y + # echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH + # shell: bash + # - name: Run lake build (Windows) + # if: matrix.os == 'windows-latest' + # run: | + # cd demo/server/LeanProject + # lake build + # shell: bash - name: Install dependencies run: npm install # - name: Build