WIPenhancementgood first issuehelp-wanted
Metriche repository
- Star
- (642 stelle)
- Metriche merge PR
- (Metriche PR in attesa)
Descrizione
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.