From 243f00225a2bfb88af208945608daa9f1c115663 Mon Sep 17 00:00:00 2001 From: Utensil Date: Tue, 10 Oct 2023 21:50:47 +0800 Subject: [PATCH 1/3] Accelelerate doc-gen4 build thanks to not calling lake from within doc-gen4 --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1f96eb2..3006fc5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -12,7 +12,7 @@ {"git": {"url": "https://github.com/leanprover/doc-gen4", "subDir?": null, - "rev": "402cfda104da78727a4ead99992abe638b8c14ef", + "rev": "f9d987567129f422ebd8cfac6a1e6233a06c720b", "opts": {}, "name": "«doc-gen4»", "inputRev?": "main", From ddb1e9173308eb7808f63b392161176f0eb2a261 Mon Sep 17 00:00:00 2001 From: Utensil Date: Tue, 10 Oct 2023 22:45:43 +0800 Subject: [PATCH 2/3] Free and save disk space --- .github/workflows/push.yml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 6856941..f3ccd9d 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -18,6 +18,22 @@ jobs: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true steps: + - name: Free Disk Space (Ubuntu) + uses: jlumbroso/free-disk-space@main + with: + # this might remove tools that are actually needed, + # if set to "true" but frees about 6 GB + tool-cache: false + + # all of these default to true, but feel free to set to + # "false" if necessary for your workflow + android: true + dotnet: true + haskell: true + large-packages: true + docker-images: true + swap-storage: true + - name: Checkout project uses: actions/checkout@v2 with: @@ -44,7 +60,7 @@ jobs: - name: Install blueprint apt deps run: | sudo apt-get update - sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full + sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-extra - name: Install blueprint deps run: | From 90c96947454e3bc26bbe6e8717585098c1a1195f Mon Sep 17 00:00:00 2001 From: Utensil Date: Wed, 11 Oct 2023 00:16:25 +0800 Subject: [PATCH 3/3] Back to texlive-full --- .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 f3ccd9d..d1a6139 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -60,7 +60,7 @@ jobs: - name: Install blueprint apt deps run: | sudo apt-get update - sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-extra + sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full - name: Install blueprint deps run: |