Project dashboard

Stream: general

[Anne Baanen]

Dear developers of Lean projects: we have created a project dashboard that keeps track of technical infrastructure such as GitHub workflows and the use of linters. Based on the scan results, the dashboard suggests tools you can install to automate maintenance tasks. This is especially useful for projects depending on Mathlib, that want to reuse all the infrastructure Mathlib provides. Add your repository to the machine-readable list at downstream-repos.yml. There is a huge variety of projects and I'd love to make that evident to scripts as well!

The dashboard currently is being incubated as a script in Mathlib, and we'd like to turn it into a proper web page eventually.

[Kim Morrison]

Here's the current output:

% scripts/downstream_dashboard.py
Checking downstream repository setup

---

Repository Fermat's Last Theorem
:check: Latest toolchain tag: v4.22.0-rc4
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:check: Detected workflow update, using the action: leanprover-community/mathlib-update-action
:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository Carleson operators on doubling metric measure spaces
:check: Latest toolchain tag: v4.22.0-rc4
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/fpvandoorn/carleson
name: Carleson operators on doubling metric measure spaces
workflows:
  build: push.yml
  docs: push.yml
  release-tag: create-release.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository ∞-Cosmos
:check: Latest toolchain tag: v4.21.0-rc3
:check: Detected workflow build, using the action: leanprover/lean-action
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:check: Detected workflow update, using the action: leanprover-community/mathlib-update-action
:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository The Polynomial Freiman-Ruzsa Conjecture
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/teorth/pfr
name: The Polynomial Freiman-Ruzsa Conjecture
workflows:
  build: push.yml
  docs: push.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/teorth/pfr
name: The Polynomial Freiman-Ruzsa Conjecture
workflows:
  build: push.yml
  docs: push.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository Prime Number Theorem and ...
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: main
github: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
name: Prime Number Theorem and ...
workflows:
  build: push.yml
  docs: push.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: main
github: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
name: Prime Number Theorem and ...
workflows:
  build: push.yml
  docs: push.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

[Kim Morrison]

Repository The sphere eversion project
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/leanprover-community/sphere-eversion
name: The sphere eversion project
workflows:
  build: blueprint.yml
  docs: blueprint.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/leanprover-community/sphere-eversion
name: The sphere eversion project
workflows:
  build: blueprint.yml
  docs: blueprint.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository Cambridge Combinatorics in Lean
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/YaelDillies/LeanCamCombi
name: Cambridge Combinatorics in Lean
workflows:
  build: push_master.yml
  docs: push_master.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/YaelDillies/LeanCamCombi
name: Cambridge Combinatorics in Lean
workflows:
  build: push_master.yml
  docs: push_master.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository add-combi
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/YaelDillies/add-combi
name: add-combi
workflows:
  build: build.yml
  docs: build.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/YaelDillies/add-combi
name: add-combi
workflows:
  build: build.yml
  docs: build.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Repository Combinatorial Games in Lean
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:check: Detected workflow build, using the action: leanprover/lean-action
:working_on_it: Consider adding a docs workflow.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file docs.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  docs: docs.yml

:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

[Edward van de Meent]

if this is something that will be automatically posted to zulip on occasion, might i propose formatting this with each repos information in its own spoiler section?

[Edward van de Meent]

because right now it's hard to see where one repo ends and another begins

[Edward van de Meent]

and it's also long

[Edward van de Meent]

(note that since these suggestions contain code blocks, the spoiler blocks will need 4 (four) backticks, and the code blocks will need to be marked with lean4 for lean4 highlighting to apply)

[Edward van de Meent]

here's what that would look like:

% scripts/downstream_dashboard.py
Checking downstream repository setup

---

Fermat's Last Theorem

Repository Fermat's Last Theorem
:check: Latest toolchain tag: v4.22.0-rc4
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:check: Detected workflow update, using the action: leanprover-community/mathlib-update-action
:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Carleson

Repository Carleson operators on doubling metric measure spaces
:check: Latest toolchain tag: v4.22.0-rc4
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/fpvandoorn/carleson
name: Carleson operators on doubling metric measure spaces
workflows:
  build: push.yml
  docs: push.yml
  release-tag: create-release.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

infinity-cosmos

Repository ∞-Cosmos
:check: Latest toolchain tag: v4.21.0-rc3
:check: Detected workflow build, using the action: leanprover/lean-action
:check: Detected workflow docs, using the action: leanprover-community/docgen-action
:check: Detected workflow release-tag, using the action: leanprover-community/lean-release-tag
:check: Detected workflow update, using the action: leanprover-community/mathlib-update-action
:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

The Polynomial Freiman-Ruzsa Conjecture

Repository The Polynomial Freiman-Ruzsa Conjecture
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/teorth/pfr
name: The Polynomial Freiman-Ruzsa Conjecture
workflows:
  build: push.yml
  docs: push.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/teorth/pfr
name: The Polynomial Freiman-Ruzsa Conjecture
workflows:
  build: push.yml
  docs: push.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

PNT+

Repository Prime Number Theorem and ...
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: main
github: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
name: Prime Number Theorem and ...
workflows:
  build: push.yml
  docs: push.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: main
github: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
name: Prime Number Theorem and ...
workflows:
  build: push.yml
  docs: push.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

[Edward van de Meent]

Sphere Eversion Project

Repository The sphere eversion project
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/leanprover-community/sphere-eversion
name: The sphere eversion project
workflows:
  build: blueprint.yml
  docs: blueprint.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/leanprover-community/sphere-eversion
name: The sphere eversion project
workflows:
  build: blueprint.yml
  docs: blueprint.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:check: Linting to Mathlib's standards.
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Cambridge Combinatorics in Lean

Repository Cambridge Combinatorics in Lean
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/YaelDillies/LeanCamCombi
name: Cambridge Combinatorics in Lean
workflows:
  build: push_master.yml
  docs: push_master.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/YaelDillies/LeanCamCombi
name: Cambridge Combinatorics in Lean
workflows:
  build: push_master.yml
  docs: push_master.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

add-combi

Repository add-combi
:check: Latest toolchain tag: v4.21.0
:light_bulb: Detected a workflow build set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover/lean-action/blob/HEAD/README.md for installation instructions.
:light_bulb: Detected a workflow docs set up by hand.
A GitHub Action exists to handle this workflow for you.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/YaelDillies/add-combi
name: add-combi
workflows:
  build: build.yml
  docs: build.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/YaelDillies/add-combi
name: add-combi
workflows:
  build: build.yml
  docs: build.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

Combinatorial Games in Lean

Repository Combinatorial Games in Lean
:working_on_it: No toolchain tags found.
Adding a tag for new releases helps users of your project to synchronize versions.
A GitHub Action exists to handle tagging new releases for you.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
:check: Detected workflow build, using the action: leanprover/lean-action
:working_on_it: Consider adding a docs workflow.
See https://github.com/leanprover-community/docgen-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file docs.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  docs: docs.yml

:working_on_it: Consider adding a release-tag workflow.
See https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file release-tag.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  release-tag: release-tag.yml

:working_on_it: Consider adding a update workflow.
See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md for installation instructions.
After installing a workflow, please add an entry to scripts/downstream_repos.yml in Mathlib.
For example, assuming you call the workflow file update.yml:

default_branch: master
github: https://github.com/vihdzp/combinatorial-games
name: Combinatorial Games in Lean
workflows:
  build: lean_action_ci.yml
  update: update.yml

:check: License: Apache License
:working_on_it: Consider adding a lint driver.
You can configure the lake lint command to automatically report code quality suggestions.
Linters are included with Mathlib or Batteries.
For instructions on enabling a linter, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-linter
:light_bulb: Consider adding a test driver.
You can configure the lake test command to build and run test files.
For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

[Ruben Van de Velde]

I mean, it's still not very readable with the spoilers. Maybe we could focus on the website?

[Edward van de Meent]

is there one?

[Edward van de Meent]

or are you saying this should be displayed on the lean community website?

[Anne Baanen]

There is not yet a website - help is very much appreciated!

[Edward van de Meent]

ah, but that is amongst your plans then?

[Anne Baanen]

I was thinking something like a grid of checkmarks, and clicking on / hovering over each checkmark gave the additional information that is now just displayed inline

[Ruben Van de Velde]

I was referring to:

Anne Baanen said:

The dashboard currently is being incubated as a script in Mathlib, and we'd like to turn it into a proper web page eventually.

[Edward van de Meent]

ah, i missed that

[Anne Baanen]

Edward van de Meent said:

ah, but that is amongst your plans then?

Perhaps more of a vision than a plan right now, but yes, I'd like to see this happen!

[Kim Morrison]

Website is going to require some engineering work and background setup that probably is best done by the Mathlib Initiative once they are running.

Let's iterate on what would be useful output from this in script mode for a bit first.

[Kim Morrison]

But I think a PR that adds more bullet points for readability, and/or a PR that divides the section better (whether just with a horizontal rule, or spoiler tags) would be great.

[Kim Morrison]

A PR that adds a cron job to mathlib to run this and post the results to zulip weekly or monthly would be awesome too!

[Yaël Dillies]

I appreciate the effort, that's definitely going in the right direction! However, do you not think it's a bit early to push for adoption of some of these scripts? For example, the upstreaming dashboard which I've been pushing for is nowhere to be found in the scripts you're suggesting

[Yaël Dillies]

I consider the lean-release-tag script very problematic in its current form: It puts the v4.X tag on whichever commit uses the v4.X toolchain first, but what we really want to have is to put it on the (potentially missing) commit that bumps to versionv4.X of the dependencies.

[Yaël Dillies]

This could lead to cases where projects A and B both have a v4.19.0-rc3 tag, but they don't actually depend on the same mathlib commit between tags v4.19.0-rc3 and v4.20.0. The two projects are therefore incompatible, but a project C that naïvely looks at the tags and says "Ah! They are the same" and try to depend on them both will suffer broken cache and issues in the dependencies.

[Yaël Dillies]

In such cases, I would rather either project A or B to not have had a v4.19.0-rc3 label in the first place. I would like the presence of two identical labels in different repos be guarantee that the dependencies of the two repos are compatible. In other words, I believe that we should not claim compatibility when compatibility isn't guaranteed.

[Anne Baanen]

Genuine thanks for the critical response! I absolutely agree that we do not have a good system to guarantee compatibility between different projects. I am convinced that this is necessary, and also that this is not something we can achieve by simply building better tooling.

The diamond dependency problem you describe can only really be fixed if the authors of projects A and B agree to update to the same version of Mathlib, regularly enough that project C who wants fresh A, B and Mathlib to be able to update all of them at once. And "regularly enough" is much more frequent than "every new Lean release". So the current release tagging is not the ultimate solution to this issue. We need, as a community, to agree to an update system where every project can enjoy fresh and consistent updates.

(Tagging Mathlib every day and telling project maintainers to update whenever they have time is also problematic: imagine A updates every 7 days and B every 10 days, then it takes 70 days for them to get in sync and project C to be able to update A, B and Mathlib. That's even worse than updating only for a new Lean release!)

But mathlib-update-action can already do some of what you describe: first it will try to update your project to each Lean release tag of Mathlib in turn, and only then update to the latest Mathlib commit.

[Anne Baanen]

every project can enjoy fresh and consistent updates

And it would be a very important feature to do this without burning out the maintainers by having them constantly deal with breakages in their projects!

[Yaël Dillies]

Anne Baanen said:

But mathlib-update-action can already do some of what you describe: first it will try to update your project to each Lean release tag of Mathlib in turn, and only then update to the latest Mathlib commit.

Aha, so is the idea that using both mathlib-update-action and lean-release-tag is the happy place?

[Anne Baanen]

Yes! Or at least the current local minimum of suffering :)

[Kim Morrison]

Yaël Dillies said:

In such cases, I would rather either project A or B to not have had a v4.19.0-rc3 label in the first place. I would like the presence of two identical labels in different repos be guarantee that the dependencies of the two repos are compatible. In other words, I believe that we should not claim compatibility when compatibility isn't guaranteed.

Yes please! Implementation of improvements to lean-release-tag would be awesome, and I strongly encourage you, or anyone else, to tackle this.

No one has ever suggested that the current behaviour is optimal, it's just optimal given the implementation time that has been available so far. :-)

[Kim Morrison]

Yaël Dillies said:

I appreciate the effort, that's definitely going in the right direction! However, do you not think it's a bit early to push for adoption of some of these scripts? For example, the upstreaming dashboard which I've been pushing for is nowhere to be found in the scripts you're suggesting

Could you add the upstreaming dashboard to this script?

[Yaël Dillies]

Let's try!

[Rémy Degenne]

I opened a PR to add the Brownian motion project to that dashboard: #28459

[Yaël Dillies]

I am trying to use the lean-release-tag in Toric, to no avail: https://github.com/YaelDillies/Toric/actions/runs/17068653433/workflow

[Yaël Dillies]

@Anne Baanen, it seems like the README is incorrect, and should instead suggest to use leanprover-community/lean-release-tag@commitname

[Yaël Dillies]

With uses: leanprover-community/lean-release-tag@9ca7ed09e240259871327bfc3a3a8d8c4bcb41aa on L.17, it works as expected :tada:

[Anne Baanen]

Thanks for the report, fixed!

[Yaël Dillies]

I've switched out all 11 projects I maintain to use lean-release-tag. I've found that not a single one of them hadn't broken in the past month (except for add-combi, which is currently empty), so I have not yet switched to mathlib-update-action.

[Yaël Dillies]

Furthermore, I don't understand yet how exactly it will switch to intermediate versions: Will it modify the lakefile to pin the correct version, then run lake update? What would happen in the case PFR, which depends on APAP?

[Anne Baanen]

The mathlib-update-action will only update the Mathlib dependency. But it should not be hard to detect/input other dependencies to update similarly.

(Is that going to work directly though? I wonder what the intended behaviour is when the Lean 4.37.0 version bump hasn't been merged into APAP and mathlib-update-action fires on PFR. Retry every so often until all the dependencies have been bumped?)

[Yaël Dillies]

My plan would be to set the PFR bump action to fire one day after the APAP bump version, so as to make likely it succeeds

[Anne Baanen]

I see! Yes, that's what I thought would be the best, assuming the Lean version bump just works:tm:.

[Anne Baanen]

So I'll add a feature request to the action for bumping other dependencies too. :)

[Anne Baanen]

Also I merged all the outstanding PRs and made sure I actually get a notification when a PR is openend. :)

[Asei Inoue]

You want lean-update action?

https://github.com/leanprover-community/lean-update

[Yaël Dillies]

Yaël Dillies said:

I've switched out all 11 projects I maintain to use lean-release-tag.

Oh btw I've opened #28655 to add them all to the project dashboard

[Yaël Dillies]

@Asei Inoue, I believe mathlib-update-action is supposed to be an iteration over your lean-update

[Anne Baanen]

Yes, the goal is slightly different. lean-update updates to the latest Lean release, while mathlib-update is intended to keep a project in sync with Mathlib (and other dependencies, if the feature request above is implemented).

[Eric Wieser]

Kim Morrison said:

Website is going to require some engineering work and background setup that probably is best done by the Mathlib Initiative once they are running.

A very lightweight option would be to a have a repo like mathlib4_docs that just runs the script on a cronjob and publishes a static page to github pages (which is also how we ran the porting dashboard)

[Kim Morrison]

I made some updates to these scripts in #31839.

[Kim Morrison]

Now for example

scripts/downstream_dashboard.py --license

outputs the following:

[Kim Morrison]

Repositories missing LICENSE file:

---

:working_on_it: Gibbs Measures
https://github.com/james18lpc/GibbsMeasure
Contact: @Kin Yau James Wong
:working_on_it: Decomposition of Persistence Modules
https://github.com/Paul-Lez/PersistentDecomp
Contact: @Paul Lezeau
:working_on_it: Brauer Group
https://github.com/Whysoserioushah/BrauerGroup_new
Contact: @Edison Xie

See https://docs.github.com/en/communities/setting-up-your-project-for-healthy-contributions/adding-a-license-to-a-repository for installation instructions.

[Kim Morrison]

Let's see if that has any effect. :-)

[Yaël Dillies]

Hmm actually I should also be a contact for all of these... :innocent:

[Yaël Dillies]

I've done the first two, and leaving Edison to do the last

[Kim Morrison]

I've updated the zulip-contact field for Gibbs and PersistentDecomp to @Yaël Dillies in #31839.

[Kim Morrison]

In the hope of eventually making it possible to turn on the default (environment) linter framework everywhere downstream, I had Claude clean up all the unusedArgument violations for projects in downstream_repos.yml.

1. ∞-Cosmos (@Emily Riehl) - https://github.com/emilyriehl/infinity-cosmos/pull/154

   • fix: silence unusedArguments linter warnings

2. Fermat's Last Theorem for regular primes (@Riccardo Brasca) - https://github.com/leanprover-community/flt-regular/pull/104

   • Fix unusedArguments linter warnings

3. The sphere eversion project (Patrick Massot) - https://github.com/leanprover-community/sphere-eversion/pull/128

   • chore: fix unusedArguments linter warnings

4. Chandra-Furst-Lipton (@Yaël Dillies) - https://github.com/YaelDillies/ChandraFurstLipton/pull/2

   • fix: remove unused NeZero d instance in broadcast_eq

5. Forbidden Matrix Theory (@Yaël Dillies) - https://github.com/YaelDillies/ForbiddenMatrix/pull/1

   • fix: add nolint unusedArguments to AllPattern

6. The Polynomial Freiman-Ruzsa Conjecture (@Terence Tao) - https://github.com/teorth/pfr/pull/262

   • fix: add nolint unusedArguments to Config structure

7. Arithmetic Progressions - Almost Periodicity (@Yaël Dillies) - https://github.com/YaelDillies/LeanAPAP/pull/11

   • fix: remove unused IsScalarTower instances

8. Gibbs Measures (@Yaël Dillies) - https://github.com/james18lpc/GibbsMeasure/pull/14

   • fix: remove unused typeclass instances

9. Toric varieties (@Yaël Dillies) - https://github.com/YaelDillies/Toric/pull/47

   • fix: add nolint unusedArguments to inv_def and inv_apply

10. Cambridge Combinatorics in Lean (@Yaël Dillies) - https://github.com/YaelDillies/LeanCamCombi/pull/44

    - fix: remove unused arguments from theorem statements

11. Decomposition of Persistence Modules (@Yaël Dillies) - https://github.com/Paul-Lez/PersistentDecomp/pull/4

    - fix: add nolint unusedArguments to incomplete definitions

12. Combinatorial Games in Lean (@Violeta Hernández) - https://github.com/vihdzp/combinatorial-games/pull/250

    - Fix unusedArguments linter warnings

[Kevin Buzzard]

What is this downstream_repos.yml and can my project be in it? There is also https://github.com/kbuzzard/ClassFieldTheory .

[Michael Rothgang]

It's a .yml file in mathlib: https://github.com/leanprover-community/mathlib4/blob/master/scripts/downstream_repos.yml

[Michael Rothgang]

To add a project, make a PR to mathlib adding it - I'm sure people will be quick to merge it.

[Michael Rothgang]

Thanks for the PR to sphere-eversion, that was very helpful. All the fixes are on master now.

[Yaël Dillies]

Kim Morrison said:

In the hope of eventually making it possible to turn on the default (environment) linter framework everywhere downstream, I had Claude clean up all the unusedArgument violations for projects in downstream_repos.yml.

Thanks! But maybe more useful would be to teach people how to turn on the linters in their projects to see the linter warnings themselves?

[Michael Rothgang]

Isn't that simply lake exe runLinter, i.e. very possible today?

[Michael Rothgang]

Speaking about the sphere eversion project, the issue is not "run all environment linters", but "deal with the pre-existing exceptions" --- i.e., you can ignore the docBlame linter, but want to run everything else. Though adding this step to CI would certainly help, so perhaps the issue was more "nobody set up CI like this"? :thinking:

[Michael Rothgang]

Put differently: I would certainly welcome a PR to sphere-eversion adding the linting step to CI.

[Yaël Dillies]

Sure, I know the solution, but it has changed several times over the past year, so it would be good to make people aware of what the state of the art solution is.

[Michael Rothgang]

Right now, you cannot globally run "all environment linter, but with linter X disabled" (or with Y enabled).

[Chris Henson]

Michael Rothgang said:

Right now, you cannot globally run "all environment linter, but with linter X disabled" (or with Y enabled).

In CSLib we currently do this by having a test with #lint only ... for each linter we want, but I agree it would be nice to be able to configure more easily.

[Kim Morrison]

It should be trivial to upgrade runLinter to take command line arguments to control which do/do not run.

[Michael Rothgang]

#14654 did this - help resurrecting it is welcome.

[Michael Rothgang]

That PR also rewrote the CLI to use lean-cli, which would mean a new dependency for batteries: that part might need to get rewritten, but the remainder of the implementation can probably be reused. If there's interest, I can update that to current mathlib on Friday.

[Kim Morrison]

Nice! Do I dare ask what happened to the diff? There are lots of spurious changes. I wonder if we could just make this a separate repo (with all the environment linters extracted from batteries) depending on lean4-cli.

[Michael Rothgang]

Ah, good that you're reminding me. I also started fixing some of the environment linters on mathlib, which obscured the diff. I have just made #32094 which has just the new linter implementation and is updated on current master.

[Kevin Buzzard]

If I run

Michael Rothgang said:

To add a project, make a PR to mathlib adding it - I'm sure people will be quick to merge it.

Oh -- I now see that both FLT and ClassFieldTheory are already in this yml file; I was confused because they weren't in the list Kim posted a few days ago, but this is presumably simply because my projects don't have unused argument violations :-)

[Kevin Buzzard]

If I run scripts/downstream_dashboard.py in Mathlib then FLT is almost all green ticks, apart from

  💡 Consider adding a test driver.
    You can configure the `lake test` command to build and run test files.
    For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

I thought of a test which FLT might want. My instinct when developing FLT is just to import Mathlib everywhere but this has the serious deficiency that it makes doc-gen take forever because doc-gen compiles all of mathlib as well as FLT. So we now lint against import Mathlib. However this does also mean that FLT might become incompatible with Mathlib because e.g. we might both define the same declaration. So I figured I would add a test file which just did

import Mathlib
import FLT

within the testing framework, and lo and behold the test failed and I fixed it :-) The resulting PR is FLT#778 . However CI is failing for a reason which I don't understand and which is probably easy to explain. I followed the instructions at the website mentioned above and in particular I added

[[lean_lib]]
name = "FLTTest"
globs = ["FLTTest.+"] # Build all files in the directory `FLTTest`.

to the bottom of my lakefile.toml. I then added one file FLTTest/MathlibCompatibility.lean into my new FLTTest directory, and then CI failed with the complaint File 'FLTTest.lean' does not exist. I don't know what a glob is and I am unclear about the role of FLTTest.lean. Is the idea that this file is supposed to contain all of my tests? If so, do I have to manually keep this file up to date if I add new tests? I had assumed from the comment on the website that I would not need such a thing. I'm sure this is an easy fix but I thought I'd followed the instructions on the website to the letter so I thought I'd report here. Maybe I don't understand what "The command lake test will build and run the executable specified by testDriver" means. Can I just add a blank FLTTest/FLTTest.lean and it will still build FLTTest/MathlibCompatibility.lean? I tried to figure out what Mathlib was doing, and it has testDriver := "MathlibTest" but no MathlibTest/MathlibTest.lean so I thought I'd just give up and ask.

[Ruben Van de Velde]

A glob is a thing with * or +

[Kevin Buzzard]

So that's not the reason it's looking for FLTTest.lean by the sound of it. And the other possible reason I could think of ("it looks for $name.lean") seems to be ruled out by mathlib's setup, so I'm confused about the error.

[Kevin Buzzard]

Oh! I've just realised that it is lake exe mk_all failing! I am not clear why lake exe mk_all is making FLTTest.lean -- have I told it to somehow? Again I note that there is no MathlibTest.lean in Mathlib. I think I'll just add the auto-generated FLTTest.lean to the PR and I bet this will fix it.

[Kevin Buzzard]

So I conjecture that adding a new [[lean_lib]] to your lakefile.toml has consequences which are not mentioned pn the website, for example it changes the behaviour of lake exe mk_all, which needs to be accounted for.

[Damiano Testa]

mk_all makes an effort to find all dependencies of a project and creates all the import-all files. Mathlib's dependencies are special-cased to not generate all the import-all files, but to skip some.

[Damiano Testa]

This is where the docs mention this behaviour.

[Damiano Testa]

(I only know this, because I was involved in writing the code, not because it should be obvious!)

[Kevin Buzzard]

Gaargh, now checkdecls is failing:

Run ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
  env:
    LAKE_PACKAGE_DIRECTORY: .
    API_DOCS: true
    BUILD_ARGS: --log-level=warning
    DOCS_EXISTS: true

✔ [2/4] Built Main (673ms)
✔ [3/4] Built Main:c.o (207ms)
✔ [4/4] Built checkdecls:exe (570ms)
uncaught exception: object file '/home/runner/work/FLT/FLT/.lake/build/lib/lean/FLTTest.olean' of module FLTTest does not exist

[Kevin Buzzard]

OK I give up on this for today; the tl;dr is that if I run mathlib's scripts/downstream_dashboard.py then I get this

  💡 Consider adding a test driver.
    You can configure the `lake test` command to build and run test files.
    For instructions on creating a test suite, please see: https://github.com/leanprover-community/mathlib4/wiki/Setting-up-linting-and-testing-for-your-Lean-project#adding-a-test-driver

for FLT, and my attempt to add the test driver in FLT#778 following the instructions in the URL mentioned in the message is failing -- docgen-action is failing in CI. Originally it failed because lake exe mk_all complained that there was no FLTTest.lean and when I fixed that with lake exe mk_all I got a new complaint from checkdecls that there was no /home/runner/work/FLT/FLT/.lake/build/lib/lean/FLTTest.olean. If someone who understands tests can give me a hint that would be great. This is not remotely urgent.

[Kevin Buzzard]

I've now turned to ClassFieldTheory and this needs more work. I'm trying to make sure we are using lean-action. The website says that CI should say

...
    steps:
      - uses: actions/checkout@v4
      # uses lean standard action with all default input values
      - uses: leanprover/lean-action@v1

but right now CI for ClassFieldTheory says

...
    steps:
      - name: Checkout project
        uses: actions/checkout@v5
        with:
          fetch-depth: 0 # Fetch all history for all branches and tags

      - name: Build and lint the project
        id: build-lean
        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0

and this code was partly written by Yael and partly by something called dependabot.

To make things even more confusing, the README at https://github.com/leanprover-community/docgen-action says

...
      - name: Checkout project
        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
        with:
          fetch-depth: 0 # Fetch all history for all branches and tags

      - name: Build and lint the project.
        id: build-lean
        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0

I am thus not entirely clear what the canonical spelling of the recommended way to do "Build and lint the project" in CI is.

[Chris Henson]

To clarify, the only differences I see are

• the fetch depth (maybe needed if you have any testing comparing commits)
• pinned commit for actions
• some cosmetic naming of steps

so all of these seem fairly close to me?

[Kevin Buzzard]

Yeah it was the pinned commit for actions which I was worried about. The community seems to be saying different things in different places, and my repos are saying more different things. I would ideally just like to have something in my repos that works, is community-recommended, and that I never have to think about again (because right now I understand a bit about github workflows but in 6 months' time I will have forgotten everything I figured out today and the files will be gobble-de-gook again, and, unlike when I was younger, it will take me just as long to work everything out again, and I might well have even forgotten that I had this discussion here).