mdbook test using latest lean4 bits #1421
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: mdbook test using latest lean4 bits | |
| # Controls when the action will run. | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| schedule: | |
| - cron: '0 10 * * *' # 11AM CET/3AM PT | |
| # A workflow run is made up of one or more jobs that can run sequentially or in parallel | |
| jobs: | |
| Build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v2 | |
| with: | |
| # interferes with lean4-nightly authentication | |
| persist-credentials: false | |
| submodules: true | |
| - name: Set paths | |
| run: | | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Setup elan toolchain on this build | |
| run: | | |
| curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | |
| chmod u+x elan-init.sh | |
| ./elan-init.sh -y --default-toolchain leanprover/lean4:nightly | |
| echo Checking location "$HOME/.elan/bin"... | |
| ls -al "$HOME/.elan/bin" | |
| elan toolchain list | |
| - name: Download mdbook for Lean | |
| run: | | |
| curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.15l2/mdbook-linux.tar.gz | |
| tar xvf mdbook-linux.tar.gz | |
| ./mdbook-linux/mdbook --help | |
| ldd ./mdbook-linux/mdbook | |
| - name: Run mdbook test | |
| run: | | |
| ls -al | |
| ./mdbook-linux/mdbook test |