issues
search
PatrickMassot
/
leanblueprint
plasTeX plugin to build formalization blueprints.
Apache License 2.0
131
stars
23
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
`\ref` in chapter names causes newline in sidebar
#30
fpvandoorn
opened
5 hours ago
0
fix: use encoding argument
#29
fpvandoorn
opened
1 week ago
0
fix: don't build Lean files twice
#28
fpvandoorn
opened
1 week ago
0
Outdated/deprecated versions of actions used in `templates/blueprint.yml`
#27
MAO3J1m0Op
opened
1 week ago
0
feat: add cleanup step
#26
fpvandoorn
opened
1 week ago
1
Suggestion: link to index
#25
fpvandoorn
opened
2 weeks ago
0
lakeblueprint pdf not working on fresh blueprint
#24
mdgeorge4153
closed
3 weeks ago
1
TOML support for leanblueprint
#23
mdgeorge4153
closed
2 weeks ago
0
cut and paste access to LaTeX and lean labels?
#22
kbuzzard
opened
2 months ago
0
typos in README.md
#21
mo271
closed
2 months ago
1
Remove "." in bullet list
#20
pitmonticone
closed
3 weeks ago
0
Add FLT3
#19
pitmonticone
closed
2 months ago
0
add upgrade instructions
#18
kbuzzard
closed
2 months ago
0
add a lake update at blueprint initialization, remove it from CI
#17
RemyDegenne
closed
2 months ago
1
fix workflow issues and typos in console.printed messages
#16
pitmonticone
closed
2 months ago
5
Fix pip install instruction in README.md
#15
RemyDegenne
closed
2 months ago
1
Feature Request: Full Mathlibok Support
#14
Bergschaf
opened
3 months ago
1
Neutralize the mathlibok command
#13
Bergschaf
closed
3 months ago
1
bibtex and client
#12
PatrickMassot
opened
3 months ago
2
Fix coloring of definitions
#11
ianjauslin-rutgers
closed
4 months ago
0
Do not fail when there is an empty `userdata` in the tree
#10
ianjauslin-rutgers
closed
5 months ago
3
Feature requests for more types of nodes and their behavior
#9
utensil
closed
2 months ago
2
Triangle before proof not correctly shown if `showmore` is enabled
#8
utensil
opened
7 months ago
1
Dependency graph is not properly generated if there is no empty line above '\begin{theorem}'
#7
ianjauslin-rutgers
opened
7 months ago
4
RFC: Absorb scattered functionalities back into leanblueprint
#6
utensil
closed
2 months ago
3
Add support for Lean 4 projects
#5
utensil
closed
7 months ago
2
Disconnect dependence on Lean 3
#4
mpenciak
opened
1 year ago
0
Emit errors if labels could not be resolved
#3
zeramorphic
closed
6 months ago
1
chore(leanblueprint/static/dep_graph.css): add `cursor: pointer` to nodes.
#2
ocfnash
closed
2 years ago
0
Use tag selector in case title has a space in
#1
alexjbest
opened
2 years ago
0