chore: cleanup CI after partial migration to mathlib4
parent
9b028566ec
commit
a5c41d25a4
|
@ -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 }}
|
|
|
@ -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
|
|
||||||
|
|
Loading…
Reference in New Issue