Skip to content

Commit e2db97e

Browse files
joelrioujoelriou
committed
Merge remote-tracking branch 'origin/master' into presheaf-of-modules-pullback-more-api
2 parents 85f2f72 + 64ce1d7 commit e2db97e

7,207 files changed

Lines changed: 593412 additions & 321617 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 & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ FROM mcr.microsoft.com/devcontainers/base:jammy
33
USER vscode
44
WORKDIR /home/vscode
55

6-
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
6+
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
77

88
ENV PATH="/home/vscode/.elan/bin:${PATH}"

‎.devcontainer/devcontainer.json‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
{
22
"name": "Mathlib4 dev container",
33

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

86
"onCreateCommand": "lake exe cache get!",
97

‎.docker/gitpod-blueprint/Dockerfile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,13 @@ SHELL ["/bin/bash", "-c"]
2424
RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
2525

2626
# install elan
27-
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
27+
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
2828

2929
# install whichever toolchain mathlib is currently using
3030
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
3131

3232
# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
33-
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
33+
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux-x86_64.tar.gz | tar xzf - && sudo mv nvim-linux-x86_64 /opt/nvim
3434

3535
ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
3636

‎.docker/gitpod/Dockerfile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,13 @@ SHELL ["/bin/bash", "-c"]
2323
RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
2424

2525
# install elan
26-
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
26+
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
2727

2828
# install whichever toolchain mathlib is currently using
2929
RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
3030

3131
# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
32-
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
32+
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux-x86_64.tar.gz | tar xzf - && sudo mv nvim-linux-x86_64 /opt/nvim
3333

3434
ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
3535

‎.docker/lean/Dockerfile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ ENTRYPOINT ["/bin/bash", "-l"]
2727
ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
2828

2929
# install elan
30-
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
30+
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
3131
. ~/.profile && \
3232
elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
3333
elan default stable

‎.github/PULL_REQUEST_TEMPLATE.md‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,13 @@ In particular, note that most reviewers will only notice your PR
1111
if it passes the continuous integration checks.
1212
Please ask for help on https://leanprover.zulipchat.com if needed.
1313
14-
To indicate co-authors, include lines at the bottom of the commit message
15-
(that is, before the `---`) using the following format:
14+
To indicate co-authors, include at least one commit authored by each
15+
co-author among the commits in the pull request. If necessary, you may
16+
create empty commits to indicate co-authorship, using commands like so:
17+
18+
git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"
1619
17-
Co-authored-by: Author Name <author@email.com>
20+
When merging, all the commits will be squashed into a single commit listing all co-authors.
1821
1922
If you are moving or deleting declarations, please include these lines at the bottom of the commit message
2023
(that is, before the `---`) using the following format:

‎.github/actionlint.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,4 @@ self-hosted-runner:
22
labels:
33
- bors
44
- pr
5+
- doc-gen

0 commit comments

Comments
 (0)