Skip to content

feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors #314278

feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors

feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors #314278

Workflow file for this run

name: continuous integration (mathlib forks)
on:
pull_request_target:
branches-ignore:
# ignore tmp branches used by bors
- 'staging.tmp*'
- 'trying.tmp*'
- 'staging*.tmp'
- 'nolints'
paths-ignore:
# pull_request_target runs the workflow and its actions from the target branch, not
# the PR, so PR changes under these dirs can't affect the run — triggering is wasteful.
- '.github/**'
concurrency:
# label each workflow run; only the latest with each label will run
# workflows on master get more expressive labels
group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
# cancel any running workflow with the same label
cancel-in-progress: true
# Limit permissions for GITHUB_TOKEN for the entire workflow
permissions:
contents: read
id-token: write
actions: read # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
pull-requests: write # Only allow PR comments/labels
# All other permissions are implicitly 'none'
jobs:
build:
name: ci (fork)
if: ${{ github.event.pull_request.head.repo.fork && github.repository != 'leanprover-community/mathlib4-nightly-testing' }}
uses: ./.github/workflows/build_template.yml
with:
concurrency_group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
pr_branch_ref: ${{ github.event.pull_request.head.sha }}
cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
cache_environment: cache-upload-forks
runs_on: pr
secrets: inherit