Merge branch 'leanprover-community:master' into unique_riesz

Author: CoolRmal

.devcontainer/Dockerfile

@@ -0,0 +1,8 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -0,0 +1,17 @@
+{
+  "name": "Mathlib4 dev container",
+
+  "image": "ghcr.io/leanprover-community/mathlib4/gitpod",
+
+  "onCreateCommand": "lake exe cache get!",
+
+  "hostRequirements": {
+     "cpus": 4
+  },
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [ "leanprover.lean4" ]
+    }
+  }
+}

.docker/gitpod-blueprint/Dockerfile

@@ -0,0 +1,47 @@
+# This is the Dockerfile for `leanprovercommunity/gitpod4-blueprint`.
+# As well as elan, we also install leanblueprint and all of its dependencies.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
+
+FROM ubuntu:jammy
+
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev python3 python3-pip python3-requests -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
+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
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
+
+# install leanblueprint
+RUN python3 -m pip install leanblueprint invoke
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.docker/gitpod/Dockerfile

@@ -0,0 +1,43 @@
+# This is the Dockerfile for `leanprovercommunity/gitpod4`.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
+
+FROM ubuntu:jammy
+
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-pip python3-requests -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
+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
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.docker/lean/Dockerfile

@@ -0,0 +1,36 @@
+# This is the Dockerfile for `leanprovercommunity/lean4`.
+# It is based on the generic `debian` image, and installs `elan` and the current stable version of `lean`.
+
+# This container does not come with a pre-installed version of mathlib;
+# you should call `lake exe cache get` which will download the most recent version.
+# The only difference between this Dockerfile and leanprovercommunity/lean4 is that this image
+# bypasses a warning that could occur when trying to connect to github for the first time.
+
+# NOTE: to run this docker image on macos or windows,
+# you will need to increase the allowed memory (in the docker GUI) beyond 2GB
+
+FROM debian
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+# install elan
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan default stable
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

.github/CONTRIBUTING.md

@@ -0,0 +1 @@
+Please see [our contribution guide](https://leanprover-community.github.io/contribute/index.html) on our website.

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,44 @@
+
+---
+<!-- The text above the `---` will become the commit message when your
+PR is merged. Please leave a blank newline before the `---`, otherwise
+GitHub will format the text above it as a title.
+
+For details on the "pull request lifecycle" in mathlib, please see:
+https://leanprover-community.github.io/contribute/index.html
+
+In particular, note that most reviewers will only notice your PR
+if it passes the continuous integration checks.
+Please ask for help on https://leanprover.zulipchat.com if needed.
+
+To indicate co-authors, include at least one commit authored by each
+co-author among the commits in the pull request. If necessary, you may 
+create empty commits to indicate co-authorship, using commands like so:
+
+git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"
+
+When merging, all the commits will be squashed into a single commit listing all co-authors.
+
+If you are moving or deleting declarations, please include these lines at the bottom of the commit message
+(that is, before the `---`) using the following format:
+
+Moves:
+- Vector.* -> List.Vector.*
+- ...
+
+Deletions:
+- Nat.bit1_add_bit1
+- ...
+
+Any other comments you want to keep out of the PR commit should go
+below the `---`, and placed outside this HTML comment, or else they
+will be invisible to reviewers.
+
+If this PR depends on other PRs, please list them below this comment,
+using the following format:
+- [ ] depends on: #abc [optional extra text]
+- [ ] depends on: #xyz [optional extra text]
+
+-->
+
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

.github/actionlint.yml

@@ -0,0 +1,4 @@
+self-hosted-runner:
+  labels:
+    - bors
+    - pr