This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 299
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into polyrith-radical
- Loading branch information
Showing
3,489 changed files
with
337,983 additions
and
154,321 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
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
Validating CODEOWNERS rules …
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
# By default, the mathlib maintainers own everything in the repo. | ||
# Later matches will take precedence over this match. | ||
|
||
# Disabled until we have better coverage by other patterns. Reenable in the future. | ||
# * @leanprover-community/mathlib-maintainers | ||
|
||
src/category_theory/ @leanprover-community/mathlib-CT | ||
|
||
src/measure_theory/ @leanprover-community/mathlib-meas | ||
|
||
src/algebraic_topology/ @leanprover-community/mathlib-CT # for now the category theory team can take care of this | ||
|
||
src/algebraic_geometry/ @leanprover-community/mathlib-AG | ||
|
||
src/combinatorics/ @leanprover-community/mathlib-CO | ||
|
||
src/probability/ @leanprover-community/mathlib-PR | ||
|
||
src/tactic/ @leanprover-community/mathlib-meta |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
name: Add mathlib4 porting comments | ||
|
||
on: | ||
schedule: | ||
- cron: "0 0 * * *" | ||
workflow_dispatch: | ||
|
||
jobs: | ||
build: | ||
name: Update comments | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/checkout@v3 | ||
|
||
- name: install Python | ||
uses: actions/setup-python@v4 | ||
with: | ||
python-version: 3.8 | ||
|
||
- name: install latest mathlibtools | ||
run: | | ||
pip install git+https://github.com/leanprover-community/mathlib-tools | ||
# multiline outputs are only supported in javascript | ||
- name: update docstrings and generate message | ||
uses: actions/github-script@v5 | ||
id: generate-message | ||
with: | ||
script: | | ||
proc = await exec.getExecOutput("python", ["./scripts/add_port_comments.py"]); | ||
console.log(proc.stdout); | ||
core.setOutput("FILE_LIST", proc.stdout); | ||
- name: Create Pull Request | ||
uses: peter-evans/create-pull-request@v4 | ||
with: | ||
base: master | ||
commit-message: "chore(*): add mathlib4 synchronization comments" | ||
title: "chore(*): add mathlib4 synchronization comments" | ||
author: leanprover-community-bot <leanprover.community@gmail.com> | ||
body: | | ||
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). | ||
Relates to the following files: | ||
${{ steps.generate-message.outputs.FILE_LIST }} | ||
--- | ||
I am a bot; please check that I have not put a comment in a bad place before running `bors merge`! | ||
labels: | | ||
easy | ||
awaiting-review | ||
mathlib4-synchronization |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,54 @@ | ||
name: Add mathlib4 porting warnings | ||
|
||
on: | ||
pull_request: | ||
|
||
jobs: | ||
build: | ||
name: Check for modifications to ported files | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/checkout@v3 | ||
|
||
- name: install Python | ||
uses: actions/setup-python@v4 | ||
with: | ||
python-version: 3.8 | ||
|
||
- name: install latest mathlibtools | ||
run: | | ||
pip install git+https://github.com/leanprover-community/mathlib-tools | ||
# TODO: is this really faster than just calling git from python? | ||
- name: Get changed files | ||
id: changed-files | ||
uses: Ana06/get-changed-files@v2.2.0 | ||
|
||
- name: run the script | ||
id: script | ||
run: | | ||
python scripts/detect_ported_files.py ${{ steps.changed-files.outputs.all }} | ||
- id: PR | ||
uses: 8BitJonny/gh-get-current-pr@2.2.0 | ||
# 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 }} | ||
sha: ${{ github.event.pull_request.head.sha }} | ||
# Only return if PR is still open | ||
filterOutClosed: true | ||
|
||
- if: steps.script.outputs.modifies_ported == 'True' | ||
id: add_label | ||
name: add "modifies-synchronized-file" | ||
# 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 -L \ | ||
-X POST \ | ||
-H "Accept: application/vnd.github+json" \ | ||
-H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}"\ | ||
-H "X-GitHub-Api-Version: 2022-11-28" \ | ||
https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels \ | ||
-d '{"labels":["modifies-synchronized-file"]}' |
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
Oops, something went wrong.