mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
chore: make doc-gen4 release depend on mathlib4 (#12516)
This PR reorders doc-gen4 after mathlib4 in the release process. Previously doc-gen4 was processed before mathlib4, but its benchmarks reference the mathlib tag which doesn't exist yet at that point, causing CI failures (https://lean-fro.zulipchat.com/#narrow/channel/530199-rss/topic/Significant.20commits.20to.20doc-gen4/near/574125422). 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
@@ -65,13 +65,6 @@ repositories:
|
||||
branch: master
|
||||
dependencies: [lean4-unicode-basic]
|
||||
|
||||
- name: doc-gen4
|
||||
url: https://github.com/leanprover/doc-gen4
|
||||
toolchain-tag: true
|
||||
stable-branch: false
|
||||
branch: main
|
||||
dependencies: [lean4-cli, BibtexQuery]
|
||||
|
||||
- name: reference-manual
|
||||
url: https://github.com/leanprover/reference-manual
|
||||
toolchain-tag: true
|
||||
@@ -107,10 +100,16 @@ repositories:
|
||||
- lean4checker
|
||||
- batteries
|
||||
- lean4-cli
|
||||
- doc-gen4
|
||||
- import-graph
|
||||
- plausible
|
||||
|
||||
- name: doc-gen4
|
||||
url: https://github.com/leanprover/doc-gen4
|
||||
toolchain-tag: true
|
||||
stable-branch: false
|
||||
branch: main
|
||||
dependencies: [lean4-cli, BibtexQuery, mathlib4]
|
||||
|
||||
- name: cslib
|
||||
url: https://github.com/leanprover/cslib
|
||||
toolchain-tag: true
|
||||
|
||||
Reference in New Issue
Block a user