-
Notifications
You must be signed in to change notification settings - Fork 14
Insights: leanprover/verso
Overview
-
- 20 Merged pull requests
- 0 Open pull requests
- 2 Closed issues
- 3 New issues
Could not load contribution data
Please try again later
1 Release published by 1 person
-
latest Verso manual (PDF and HTML)
published
Jan 6, 2025
20 Pull requests merged by 2 people
-
chore: bump SubVerso for bugfix
#282 merged
Jan 31, 2025 -
fix: allow multi-arg roles when generating string previews
#281 merged
Jan 31, 2025 -
fix: don't show _root_ in code hovers when not needed
#280 merged
Jan 31, 2025 -
feat: automatically track open-source libraries for web frontend
#279 merged
Jan 31, 2025 -
fix: Set toc-backdrop z-index to 9, restore toc to 10
#278 merged
Jan 30, 2025 -
feat: allow manual genre to add custom elements to HTML <head>
#267 merged
Jan 30, 2025 -
fix: docstring heuristic rendering should skip Lake commands
#276 merged
Jan 21, 2025 -
chore: use upstream version of MD4Lean
#275 merged
Jan 17, 2025 -
feat: docstring splicing
#273 merged
Jan 17, 2025 -
feat: add the ability to replace tactic docstrings
#272 merged
Jan 16, 2025 -
chore: bump md4lean dependency
#271 merged
Jan 14, 2025 -
chore: bump to v4.16.0-rc2
#270 merged
Jan 14, 2025 -
perf: use a better data structure for the index
#269 merged
Jan 13, 2025 -
feat: track progress of root namespace
#268 merged
Jan 13, 2025 -
feat: small quality of life improvements in progress tracker
#265 merged
Jan 9, 2025 -
feat: heuristic Markdown docstring rendering
#255 merged
Jan 7, 2025 -
fix: use declared syntax for all Verso syntax
#264 merged
Jan 7, 2025 -
chore: improve CI parallelism
#263 merged
Jan 6, 2025 -
chore: bump toolchain to 4.16.0-rc1
#262 merged
Jan 6, 2025 -
chore: bump toolchain to v4.15.0
#260 merged
Jan 4, 2025
2 Issues closed by 1 person
-
error loading library, libleanmd4c.so
#132 closed
Jan 14, 2025 -
Antiquotes in `block` category do not work
#257 closed
Jan 7, 2025
3 Issues opened by 3 people
-
bug(tactic): Unexpected horizontal rule (thematic break) in parsed Markdown
#277 opened
Jan 26, 2025 -
Syntax-highlight comments in verso code
#274 opened
Jan 17, 2025 -
Manual genre: add a page-local table of contents to every page
#266 opened
Jan 10, 2025