Merge branch 'erdos-stone-1' into erdos-stone-2

Author: mitchell-horner

.devcontainer/Dockerfile

@@ -1,8 +1,6 @@
-FROM mcr.microsoft.com/devcontainers/base:jammy
+FROM mcr.microsoft.com/devcontainers/base:ubuntu
 
 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

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

.docker/gitpod-blueprint/Dockerfile

@@ -10,7 +10,7 @@ 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 apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev tzdata 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

.docker/gitpod/Dockerfile

@@ -9,7 +9,7 @@ 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 apt-get update && apt-get install sudo git curl git tzdata 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

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,8 +1,11 @@
 
 ---
-<!-- 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.
+<!-- Your PR title will become the first line of the commit message.
+
+In this box, the text above the `---` (if not empty) will be appended
+to the commit message, and can be used to give additional context or
+details. 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
@@ -11,16 +14,26 @@ 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:
+When merging, all the commits will be squashed into a single commit
+listing all co-authors.
+
+Co-authors in the squash commit are gathered from two sources:
+
+First, all authors of commits to this PR branch are included. Thus,
+one way to add co-authors is to 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.
+Second, co-authors can also be listed in lines at the very bottom of
+the commit message (that is, directly before the `---`) using the following format:
+
+Co-authored-by: Author Name <author@email.com>
 
-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:
+If you are moving or deleting declarations, please include these lines
+at the bottom of the commit message (before the `---`, and also before
+any "Co-authored-by" lines) using the following format:
 
 Moves:
 - Vector.* -> List.Vector.*

.github/actionlint.yml

@@ -2,3 +2,5 @@ self-hosted-runner:
   labels:
     - bors
     - pr
+    - doc-gen
+    - lean4checker

.github/actions/get-mathlib-ci/README.md

@@ -0,0 +1,75 @@
+# get-mathlib-ci
+
+This action is the source of truth for how workflows in this repository check out
+`leanprover-community/mathlib-ci`.
+
+## Policy
+
+Any workflow that needs `mathlib-ci` should use this action instead of writing its
+own `actions/checkout` block for `leanprover-community/mathlib-ci`.
+
+The default `ref` in [`action.yml`](./action.yml) is the single canonical pinned
+`mathlib-ci` commit for this repository. This is auto-updated regularly by the
+[`update_dependencies.yml` workflow](../../workflows/update_dependencies.yml).
+
+## Why
+
+- Keep the pinned `mathlib-ci` ref in one place.
+- Avoid drift and copy/paste mistakes across many workflows.
+- Make ref bumps a one-file update.
+
+## Usage
+
+In workflows, check out this repository's actions from the running workflow commit,
+then use the local action:
+
+```yaml
+- name: Checkout local actions
+  uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+  with:
+    ref: ${{ github.workflow_sha }}
+    fetch-depth: 1
+    sparse-checkout: .github/actions
+    path: workflow-actions
+
+- name: Get mathlib-ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+```
+
+Override the ref only when needed:
+
+```yaml
+- name: Get mathlib-ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+  with:
+    ref: master
+```
+
+## Outputs
+
+This action also exposes values that later workflow steps can reuse:
+
+- `ref`: the effective `mathlib-ci` ref that was checked out. If the workflow did
+  not pass `with.ref`, this is the action's default pinned commit.
+- `path`: the checkout path used for `mathlib-ci`.
+- `scripts_dir`: the absolute path to the checked out `scripts` directory.
+
+The action also exports these environment variables for subsequent steps:
+
+- `CI_CHECKOUT_PATH`: the absolute path to the checked out `mathlib-ci` repository.
+- `CI_SCRIPTS_DIR`: the absolute path to the checked out `mathlib-ci/scripts` directory.
+
+If a workflow needs to refer to the exact resolved `mathlib-ci` ref later, use the
+action output instead of duplicating the pinned SHA in the workflow:
+
+```yaml
+- name: Get mathlib-ci
+  id: get_mathlib_ci
+  uses: ./workflow-actions/.github/actions/get-mathlib-ci
+
+- name: Use resolved ref
+  run: |
+    echo "Resolved ref: ${{ steps.get_mathlib_ci.outputs.ref }}"
+    echo "Scripts dir: ${{ steps.get_mathlib_ci.outputs.scripts_dir }}"
+    echo "Raw URL: https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh"
+```

.github/actions/get-mathlib-ci/action.yml

@@ -0,0 +1,52 @@
+# Source of truth for `mathlib-ci` checkout settings in this repository.
+# Workflows should use this action instead of duplicating the checkout block
+# and hardcoded ref in multiple places.
+name: Get mathlib-ci
+description: Checkout leanprover-community/mathlib-ci at a shared ref.
+inputs:
+  ref:
+    description: Git ref (branch, tag, or SHA) for mathlib-ci.
+    required: false
+    # Default pinned commit used by workflows unless they explicitly override.
+    # Update this ref as needed to pick up changes to mathlib-ci scripts
+    # This is also updated automatically by .github/workflows/update_dependencies.yml
+    default: 8c3d31d2beba80d86de30b6ccd373d2c3a76b26e
+  path:
+    description: Checkout destination path.
+    required: false
+    default: ci-tools
+  fetch-depth:
+    description: Number of commits to fetch.
+    required: false
+    default: '1'
+outputs:
+  ref:
+    description: Effective ref used for the checkout.
+    value: ${{ inputs.ref }}
+  path:
+    description: Checkout path used.
+    value: ${{ inputs.path }}
+  scripts_dir:
+    description: Absolute path to the scripts directory.
+    value: ${{ steps.paths.outputs.scripts_dir }}
+runs:
+  using: composite
+  steps:
+    - name: Get mathlib-ci
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        repository: leanprover-community/mathlib-ci
+        ref: ${{ inputs.ref }}
+        fetch-depth: ${{ inputs.fetch-depth }}
+        path: ${{ inputs.path }}
+
+    - name: Setup CI Scripts Paths
+      id: paths
+      shell: bash
+      run: |
+        checkout_path="${GITHUB_WORKSPACE}/${{ inputs.path }}"
+        scripts_dir="${checkout_path}/scripts"
+        echo "checkout_path=${checkout_path}" >> "$GITHUB_OUTPUT"
+        echo "scripts_dir=${scripts_dir}" >> "$GITHUB_OUTPUT"
+        echo "CI_CHECKOUT_PATH=${checkout_path}" >> "$GITHUB_ENV"
+        echo "CI_SCRIPTS_DIR=${scripts_dir}" >> "$GITHUB_ENV"