Add groebner_basis_def
#5
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
| # modified from https://github.com/leanprover-community/mathlib4/blob/master/.github/workflows/build_fork.yml | |
| on: | |
| push: | |
| branches-ignore: | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| - 'nolints' | |
| name: continuous integration | |
| jobs: | |
| # Cancels previous runs of jobs in this file | |
| cancel: | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| name: 'Cancel Previous Runs (CI)' | |
| runs-on: ubuntu-latest | |
| # timeout-minutes: 3 | |
| steps: | |
| - uses: styfle/[email protected] | |
| with: | |
| all_but_latest: true | |
| access_token: ${{ github.token }} | |
| # style_lint: | |
| # if: github.repository != 'leanprover-community/mathlib4' | |
| # name: Lint style (fork) | |
| # runs-on: ubuntu-latest | |
| # steps: | |
| # - name: cleanup | |
| # run: | | |
| # find . -name . -o -prune -exec rm -rf -- {} + | |
| # | |
| # - uses: actions/checkout@v3 | |
| # | |
| # - name: Install bibtool | |
| # if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| # run: | | |
| # sudo apt-get update | |
| # sudo apt-get install -y bibtool | |
| # | |
| # - name: install Python | |
| # if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| # uses: actions/setup-python@v4 | |
| # with: | |
| # python-version: 3.8 | |
| # | |
| # - name: lint | |
| # run: | | |
| # ./scripts/lint-style.sh | |
| # | |
| # - name: lint references.bib | |
| # run: | | |
| # ./scripts/lint-bib.sh | |
| # check_imported: | |
| # if: github.repository != 'leanprover-community/mathlib4' | |
| # name: Check all files imported (fork) | |
| # runs-on: ubuntu-latest | |
| # steps: | |
| # - name: cleanup | |
| # run: | | |
| # find . -name . -o -prune -exec rm -rf -- {} + | |
| # | |
| # - uses: actions/checkout@v3 | |
| # | |
| # - name: update Mathlib.lean | |
| # run: | | |
| # find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean | |
| # | |
| # - name: update MathlibExtras.lean | |
| # run: | | |
| # find MathlibExtras -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean | |
| # | |
| # - name: update Mathlib/Tactic.lean | |
| # run: | | |
| # find Mathlib/Tactic -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean | |
| # | |
| # - name: check that all files are imported | |
| # run: git diff --exit-code | |
| build: | |
| # if: github.repository != 'leanprover-community/mathlib4' | |
| name: Build | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - uses: actions/checkout@v3 | |
| # We update `Mathlib.lean` as a convenience here, | |
| # but verify that this didn't change anything in the `check_imported` job. | |
| # - name: update Mathlib.lean | |
| # run: | | |
| # find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean | |
| - name: get cache | |
| run: lake exe cache get | |
| - name: build | |
| uses: liskin/gh-problem-matcher-wrap@v2 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake build | |
| # - name: build library_search cache | |
| # run: lake build MathlibExtras | |
| # | |
| # - name: upload cache | |
| # if: always() | |
| # run: | | |
| # lake exe cache commit || true | |
| # lake exe cache put || true | |
| # env: | |
| # MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| # | |
| # - name: test mathlib | |
| # run: make -j 8 test | |
| # | |
| # - name: lint mathlib | |
| # run: env LEAN_ABORT_ON_PANIC=1 make lint | |
| # final: | |
| # name: Post-CI job (fork) | |
| # if: github.repository != 'leanprover-community/mathlib4' | |
| # needs: [style_lint, build, check_imported] | |
| # runs-on: ubuntu-latest | |
| # steps: | |
| # - uses: actions/checkout@v3 | |
| # | |
| # - id: PR | |
| # uses: 8BitJonny/[email protected] | |
| # # TODO: this may not work properly if the same commit is pushed to multiple branches: | |
| # # https://github.com/8BitJonny/gh-get-current-pr/issues/8 | |
| # with: | |
| # github-token: ${{ secrets.GITHUB_TOKEN }} | |
| # # Only return if PR is still open | |
| # filterOutClosed: true | |
| # | |
| # - id: remove_labels | |
| # name: Remove "awaiting-CI" | |
| # # we use curl rather than octokit/request-action so that the job won't fail | |
| # # (and send an annoying email) if the labels don't exist | |
| # run: | | |
| # curl --request DELETE \ | |
| # --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \ | |
| # --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' |