Toolchain help

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

If someone understands how to do this:

#general > Project dashboard @ 💬

in particular this:

Kim Morrison said:

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

(paging @Ian Jauslin?), could they please PR it to the repo? I know we're doing a bunch of things by hand, but I thought that was necessary because we have some non-standard extra bells and whistles...?

[Kim Morrison]

Nothing here is urgent: it's fine if you want to continue as you were. But there are lots of modern replacements for the "by hand" way of setting things up, and these reports are meant to be helpful alerting people to the existence of these replacements.

Each of the emoji-marked items above is essentially a separate suggestion: you could implement any subset.

[Ian Jauslin]

Cool! Thank you @Kim Morrison !
I think we should use the lean-action actions. We had set up our own system because these tools were not available when we got started, but at the moment I don't see an issue with switching over. In fact, I think it is good for the project to try to be as standard as possible. I can have a closer look next week.

[Kim Morrison]

Amazing -- yes, having high profile projects both exercise (and complain about!) the new tools, and set an example for everyone to follow, will really help the ecosystem grow in healthy ways.