From a5c41d25a47ec8a8d8781435f64688c9e3a17190 Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sat, 22 Apr 2023 01:01:19 +0200
Subject: [PATCH] chore: cleanup CI after partial migration to mathlib4

---
 .github/workflows/mathlib4docs.yml | 29 ------------------
 deploy_docs.sh                     | 47 ------------------------------
 2 files changed, 76 deletions(-)
 delete mode 100644 .github/workflows/mathlib4docs.yml
 delete mode 100755 deploy_docs.sh

diff --git a/.github/workflows/mathlib4docs.yml b/.github/workflows/mathlib4docs.yml
deleted file mode 100644
index 5e75fb6..0000000
--- a/.github/workflows/mathlib4docs.yml
+++ /dev/null
@@ -1,29 +0,0 @@
-name: build and deploy mathlib4 docs
-
-on:
-  workflow_dispatch:
-  schedule:
-    - cron: '0 */8 * * *' # every 8 hours
-jobs:
-  build:
-    name: build and deploy mathlib4 docs
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout repo
-        uses: actions/checkout@v3
-
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          ~/.elan/bin/lean --version
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: generate and deploy docs
-        if: github.repository == 'leanprover/doc-gen4'
-        run: |
-          cd ../
-          ./doc-gen4/deploy_docs.sh
-        env:
-          MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
-          DOC_GEN_REF: ${{ github.sha }}
diff --git a/deploy_docs.sh b/deploy_docs.sh
deleted file mode 100755
index 9d910e9..0000000
--- a/deploy_docs.sh
+++ /dev/null
@@ -1,47 +0,0 @@
-set -e
-set -x
-
-git config --global user.email "leanprover.community@gmail.com"
-git config --global user.name "leanprover-community-bot"
-
-git clone "https://github.com/leanprover-community/mathlib4_docs.git" mathlib4_docs
-
-# Workaround for the lake issue
-elan default leanprover/lean4:nightly
-lake new workaround math
-cd workaround
-echo 'require «doc-gen4» from ".." / "doc-gen4" ' >> lakefile.lean
-
-# doc-gen4 expects to work on github repos with at least one commit
-git add .
-git commit -m "workaround"
-git remote add origin "https://github.com/leanprover/workaround"
-
-lake update
-
-cd lake-packages/mathlib
-mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
-cd ../../
-
-if [ "$(cd ../mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF" ]; then
-  exit 0
-fi
-
-lake exe cache get
-lake build Mathlib:docs Std:docs
-
-cd ..
-rm -rf mathlib4_docs/docs/
-cp -r "workaround/build/doc" mathlib4_docs/docs
-mkdir ~/.ssh
-echo "$MATHLIB4_DOCS_KEY" > ~/.ssh/id_ed25519
-chmod 600 ~/.ssh/id_ed25519
-cd mathlib4_docs/docs
-git remote set-url origin "git@github.com:leanprover-community/mathlib4_docs.git"
-git config user.email "leanprover.community@gmail.com"
-git config user.name "leanprover-community-bot"
-git add -A .
-git checkout --orphan master2
-git commit -m "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF"
-git push -f origin HEAD:master
-