WIPenhancementgood first issuehelp-wanted
仓库指标
- 星标
- (642 个星标)
- PR 合并指标
- (PR 指标待抓取)
描述
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.