Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
Merge remote-tracking branch 'origin/master' into eric-wieser/trivial…
Browse files Browse the repository at this point in the history 
…-basis.parallelepiped-lemmas
  • Loading branch information
@eric-wieser
eric-wieser committed May 12, 2023
2 parents 6ed508e + bd15ff4 commit f8ab07b
Show file tree
Hide file tree
Showing 460 changed files with 12,693 additions and 7,371 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/add_port_comment.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ jobs:
- uses: actions/checkout@v3

- name: install Python
uses: actions/setup-python@v3
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/add_ported_warnings.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ jobs:
- uses: actions/checkout@v3

- name: install Python
uses: actions/setup-python@v3
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -22,7 +22,7 @@ jobs:
# TODO: is this really faster than just calling git from python?
- name: Get changed files
id: changed-files
uses: Ana06/get-changed-files@v1.2
uses: Ana06/get-changed-files@v2.2.0

- name: run the script
id: script
Expand Down
24 changes: 12 additions & 12 deletions .github/workflows/bors.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ jobs:
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/cancel-workflow-action@0.9.0
- uses: styfle/cancel-workflow-action@0.11.0
with:
all_but_latest: true
access_token: ${{ github.token }}
Expand All @@ -32,7 +32,7 @@ jobs:
name: Lint style
runs-on: bors
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- name: Install bibtool
if: ${{ 'bors' == 'ubuntu-latest' }}
Expand All @@ -42,7 +42,7 @@ jobs:
- name: install Python
if: ${{ 'bors' == 'ubuntu-latest' }}
uses: actions/setup-python@v2
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -64,7 +64,7 @@ jobs:
outputs:
artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}

Expand All @@ -78,7 +78,7 @@ jobs:
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -90,7 +90,7 @@ jobs:
run: |
set -o pipefail
leanpkg configure
echo "::set-output name=started::true"
echo "started=true" >> $GITHUB_OUTPUT
lean --json -T100000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
Expand All @@ -111,7 +111,7 @@ jobs:
touch workspace.tar
tar -cf workspace.tar --exclude=*.tar* .
git_hash="$(git log -1 --pretty=format:%h)"
echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT
- name: upload precompiled mathlib zip file
if: always() && steps.build.outputs.started == 'true'
Expand Down Expand Up @@ -143,7 +143,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand Down Expand Up @@ -180,7 +180,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand All @@ -196,7 +196,7 @@ jobs:
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand Down Expand Up @@ -257,10 +257,10 @@ jobs:
needs: [style_lint, build, lint, tests]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- id: PR
uses: 8BitJonny/gh-get-current-pr@1.2.0
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:
Expand Down
24 changes: 12 additions & 12 deletions .github/workflows/build.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ jobs:
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/cancel-workflow-action@0.9.0
- uses: styfle/cancel-workflow-action@0.11.0
with:
all_but_latest: true
access_token: ${{ github.token }}
Expand All @@ -40,7 +40,7 @@ jobs:
name: Lint style
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- name: Install bibtool
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
Expand All @@ -50,7 +50,7 @@ jobs:
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v2
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -72,7 +72,7 @@ jobs:
outputs:
artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}

Expand All @@ -86,7 +86,7 @@ jobs:
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -98,7 +98,7 @@ jobs:
run: |
set -o pipefail
leanpkg configure
echo "::set-output name=started::true"
echo "started=true" >> $GITHUB_OUTPUT
lean --json -T100000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
Expand All @@ -119,7 +119,7 @@ jobs:
touch workspace.tar
tar -cf workspace.tar --exclude=*.tar* .
git_hash="$(git log -1 --pretty=format:%h)"
echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT
- name: upload precompiled mathlib zip file
if: always() && steps.build.outputs.started == 'true'
Expand Down Expand Up @@ -151,7 +151,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand Down Expand Up @@ -188,7 +188,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand All @@ -204,7 +204,7 @@ jobs:
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand Down Expand Up @@ -265,10 +265,10 @@ jobs:
needs: [style_lint, build, lint, tests]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- id: PR
uses: 8BitJonny/gh-get-current-pr@1.2.0
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:
Expand Down
24 changes: 12 additions & 12 deletions .github/workflows/build.yml.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ jobs:
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/cancel-workflow-action@0.9.0
- uses: styfle/cancel-workflow-action@0.11.0
with:
all_but_latest: true
access_token: ${{ github.token }}
Expand All @@ -18,7 +18,7 @@ jobs:
name: Lint styleJOB_NAME
runs-on: STYLE_LINT_RUNNER
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- name: Install bibtool
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
Expand All @@ -28,7 +28,7 @@ jobs:

- name: install Python
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
uses: actions/setup-python@v2
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -50,7 +50,7 @@ jobs:
outputs:
artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}

Expand All @@ -64,7 +64,7 @@ jobs:

- name: install Python
if: ${{ ! IS_SELF_HOSTED }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand All @@ -76,7 +76,7 @@ jobs:
run: |
set -o pipefail
leanpkg configure
echo "::set-output name=started::true"
echo "started=true" >> $GITHUB_OUTPUT
lean --json -T100000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py

Expand All @@ -97,7 +97,7 @@ jobs:
touch workspace.tar
tar -cf workspace.tar --exclude=*.tar* .
git_hash="$(git log -1 --pretty=format:%h)"
echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT

- name: upload precompiled mathlib zip file
if: always() && steps.build.outputs.started == 'true'
Expand Down Expand Up @@ -129,7 +129,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand Down Expand Up @@ -166,7 +166,7 @@ jobs:
run: rm -rf ./* ./.??*

- name: retrieve build
uses: actions/download-artifact@v2
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}

Expand All @@ -182,7 +182,7 @@ jobs:

- name: install Python
if: ${{ ! IS_SELF_HOSTED }}
uses: actions/setup-python@v1
uses: actions/setup-python@v4
with:
python-version: 3.8

Expand Down Expand Up @@ -243,10 +243,10 @@ jobs:
needs: [style_lint, build, lint, tests]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3

- id: PR
uses: 8BitJonny/gh-get-current-pr@1.2.0
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:
Expand Down
Loading

0 comments on commit f8ab07b

Please sign in to comment.