doc: typo #31
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
| on: | |
| push: | |
| pull_request: | |
| name: ci | |
| jobs: | |
| build: | |
| name: ${{ matrix.name }} | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: ${{ matrix.shell || 'sh' }} | |
| strategy: | |
| matrix: | |
| include: | |
| - name: Build on Ubuntu | |
| os: ubuntu-latest | |
| lean_os: linux | |
| - name: Build on macOS | |
| os: macos-latest | |
| lean_os: macOS | |
| - name: Build on Windows | |
| os: windows-latest | |
| lean_os: windows | |
| shell: msys2 {0} | |
| steps: | |
| - name: Install MSYS2 (Windows) | |
| if: matrix.os == 'windows-latest' | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| path-type: inherit | |
| install: curl unzip | |
| - name: Install elan | |
| shell: bash | |
| run: | | |
| curl -sSfLO https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | |
| chmod +x elan-init.sh | |
| ./elan-init.sh -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - uses: actions/checkout@v4 | |
| # TODO: investigate why `lake build` deadlocks on macOS | |
| - name: Build widgets | |
| run: npm clean-install && npm run build | |
| working-directory: ./widget | |
| env: | |
| NODE_OPTIONS: "--max-old-space-size=4096" | |
| - name: Build package | |
| run: lake build ProofWidgets | |
| - name: Create release for tag | |
| if: github.ref_type == 'tag' | |
| uses: softprops/action-gh-release@v1 | |
| # TODO: replace with just `lake upload $RELEASE_TAG` when lean4#2713 is fixed | |
| # References: | |
| # https://docs.github.com/en/actions/learn-github-actions/contexts#runner-context | |
| # https://stackoverflow.com/questions/8766730/tar-command-in-mac-os-x-adding-hidden-files-why | |
| - name: Upload release archive | |
| if: github.ref_type == 'tag' | |
| # All our runners are 64-bit ¯\_(ツ)_/¯ | |
| run: | | |
| export COPYFILE_DISABLE=true | |
| tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./.lake/build . | |
| gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| RELEASE_TAG: ${{ github.ref_name }} | |
| LEAN_OS: ${{ matrix.lean_os }} |