Skip to content

Commit e1c5114

Browse files
b-mehtab-mehta
authored
Merge branch 'master' into finset-ring-lemmas
2 parents 15964ec + efc0e39 commit e1c5114

1,134 files changed

Lines changed: 23834 additions & 17250 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.devcontainer/Dockerfile‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
FROM mcr.microsoft.com/devcontainers/base:jammy
1+
FROM mcr.microsoft.com/devcontainers/base:ubuntu
22

33
USER vscode
44
WORKDIR /home/vscode
55

66
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
7-
8-
ENV PATH="/home/vscode/.elan/bin:${PATH}"

‎.devcontainer/devcontainer.json‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,20 @@
11
{
22
"name": "Mathlib4 dev container",
33

4-
"image": "ghcr.io/leanprover-community/mathlib4/gitpod",
4+
"build": {
5+
"dockerfile": "Dockerfile"
6+
},
57

68
"onCreateCommand": "lake exe cache get!",
79

810
"hostRequirements": {
9-
"cpus": 4
11+
"cpus": 4,
12+
"memory": "8gb"
1013
},
1114

1215
"customizations": {
13-
"vscode" : {
14-
"extensions" : [ "leanprover.lean4" ]
16+
"vscode": {
17+
"extensions": ["leanprover.lean4"]
1518
}
1619
}
1720
}

‎.github/dependabot.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ version: 2 # Specifies the version of the Dependabot configuration file format
33
updates:
44
# Configuration for dependency updates
55
- package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates
6-
directories:
7-
- "/.github/*" # covers `build.in.yml` as well, which is not in `.github/workflows/` because it shouldn't be run in CI.
6+
directories:
7+
- "/.github/workflows"
88
schedule:
99
# Check for updates to GitHub Actions every month
1010
interval: "monthly"
1111
groups:
12-
# group updates into single PRs since we want to update both build.in.yml and its outputs at the same time
12+
# group updates into single PRs
1313
actions-version-updates:
1414
applies-to: version-updates
1515
patterns:

‎.github/workflows/PR_summary.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,15 +17,15 @@ jobs:
1717

1818
steps:
1919
- name: Checkout code
20-
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
20+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
2121
with:
2222
ref: ${{ github.event.pull_request.head.sha }}
2323
fetch-depth: 0
2424
path: pr-branch
2525

2626
# Checkout the master branch into a subdirectory
2727
- name: Checkout master branch
28-
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
28+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
2929
with:
3030
# When testing the scripts, comment out the "ref: master"
3131
ref: master
@@ -60,7 +60,7 @@ jobs:
6060
fi
6161
6262
- name: Set up Python
63-
uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.0
63+
uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
6464
with:
6565
python-version: 3.12
6666

‎.github/workflows/actionlint.yml‎

Lines changed: 2 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -10,27 +10,10 @@ jobs:
1010
runs-on: ubuntu-latest
1111
steps:
1212
- name: Checkout
13-
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
13+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
1414

1515
- name: suggester / actionlint
16-
uses: reviewdog/action-actionlint@83e4ed25b168066ad8f62f5afbb29ebd8641d982 # v1.69.1
16+
uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
1717
with:
1818
tool_name: actionlint
1919
fail_level: error
20-
21-
check_build_yml:
22-
name: check workflows generated by build.in.yml
23-
runs-on: ubuntu-latest
24-
steps:
25-
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
26-
27-
- name: update workflows
28-
run: |
29-
cd .github/workflows/
30-
./mk_build_yml.sh
31-
32-
- name: suggester / build.in.yml
33-
uses: reviewdog/action-suggester@aa38384ceb608d00f84b4690cacc83a5aba307ff # v1.24.0
34-
with:
35-
tool_name: mk_build_yml.sh
36-
fail_level: error

‎.github/workflows/add_label_from_diff.yaml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,12 +22,12 @@ jobs:
2222
if: github.repository == 'leanprover-community/mathlib4'
2323
steps:
2424
- name: Checkout code
25-
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
25+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
2626
with:
2727
ref: ${{ github.event.pull_request.head.sha }}
2828
fetch-depth: 0
2929
- name: Configure Lean
30-
uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
30+
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
3131
with:
3232
auto-config: false
3333
use-github-cache: false

‎.github/workflows/auto_assign_reviewers.yaml‎

Lines changed: 0 additions & 29 deletions
This file was deleted.

0 commit comments

Comments
 (0)