WIPenhancementgood first issuehelp-wanted
Métricas do repositório
- Stars
- (642 estrelas)
- Métricas de merge de PR
- (Métricas PR pendentes)
Description
It's preferable to align the workflows of HepLean with that of Mathlib. Here's the task breakdown:
- Automatically tag and release after a version bump.
- Move the dependency of doc-gen4 from the top-level lakefile to a separate
docleandirectory as suggested by doc-gen4, and create a workflow that is triggered when a PR merges similar to the documentation generation of Mathlib barring the separate repo. This preventslake, called from the top-level, from pulling and building doc-gen4 and its dependencies. - Incorporate Mathlib linters.
If more tasks are required, feel free to add them to the list above, and link related PRs to the "Development" section on the right of the GitHub web UI.