issues
search
lean-dojo
/
LeanDojo
Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
532
stars
77
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF
#201
njuyxw
opened
7 hours ago
1
Support asyncio for Dojo
#200
yangky11
closed
18 hours ago
0
minor bugfix
#198
yangky11
closed
1 week ago
0
fix minor bug
#197
yangky11
closed
1 week ago
0
Fix mypy Typing Errors
#196
yangky11
opened
1 week ago
0
fix minor bugs
#195
yangky11
closed
1 week ago
0
Unable to find Lean4Repl.lean in the traced repo
#194
LuoKaiGSW
closed
1 week ago
0
Failed trace because of lean4 dependency
#193
Adarsh321123
closed
3 days ago
3
Incorporate Recent Commits
#192
yangky11
closed
2 weeks ago
3
LeanDojo should not be run as root
#191
yyyhz
closed
1 week ago
1
Extend function features to allow new repo types
#190
RexWzh
closed
3 weeks ago
2
Fix git method & add more tests
#188
RexWzh
closed
1 month ago
2
Error Loading `lean_dojo` due to Git Version Parsing Issue[Windows]
#186
RexWzh
closed
1 month ago
2
Alternative function to LeanGitRepo
#185
LuoKaiGSW
closed
3 weeks ago
2
Alternative function to LeanGitRepo
#184
LuoKaiGSW
closed
1 month ago
0
Buggy Benchmark Generation
#183
Adarsh321123
closed
3 days ago
10
LeanDojo Benchmark 4 Version
#182
Adarsh321123
closed
1 month ago
0
minor change in tests
#181
yangky11
closed
1 month ago
0
Use `pexpect` instead of `signal` in dojo.py
#180
yangky11
closed
1 month ago
0
Add Support for Local and Remote Repositories
#179
RexWzh
closed
3 weeks ago
26
Minor fix to remove CI node warning
#178
Peiyang-Song
closed
1 month ago
0
Errors tracing older repos
#177
AG161
closed
3 weeks ago
6
fix warnings in docs
#176
yangky11
closed
1 month ago
0
Reduce the Initialization Time When Interacting with Lean
#175
yangky11
closed
1 month ago
0
Fix a minor bug in AST formats
#174
yangky11
closed
1 month ago
0
Ignore rmtree Errors
#173
yangky11
closed
1 month ago
2
Do we have a script to reproduce the numbers in the paper?
#172
hongjin-su
closed
2 months ago
1
"Missing $PATH/Main_dep.paths" during tracing of repo
#171
realharryhero
closed
2 months ago
1
build_lean4_repo.py exit with error
#170
OctoberFox11
closed
2 months ago
3
ReProver Warning
#169
IanWangg
closed
2 months ago
3
a potential bug in container.py
#168
OakYU
closed
2 months ago
2
fix the bug related to relative paths
#167
yangky11
closed
2 months ago
0
V1.9.0
#166
yangky11
closed
3 months ago
0
demo-lean4: Dojo() does not recognize traced repo
#165
jganten
closed
2 months ago
3
V1.8.3
#164
yangky11
closed
3 months ago
0
Update README.md
#163
yangky11
closed
3 months ago
0
Fix typo in notebook
#162
pitmonticone
closed
3 months ago
0
Issue with demo-lean3.ipynb when creating LeanGitRepo
#161
ahayat16
closed
4 months ago
3
get_namespaces() method callable but not implemented
#160
AG161
closed
4 months ago
1
EOF error when additional_imports = ['Mathlib']
#158
wclsn
closed
4 months ago
5
Update getting-started.rst
#157
yangky11
closed
4 months ago
0
Update README.md
#156
yangky11
closed
4 months ago
0
Update getting-started.rst
#155
yangky11
closed
4 months ago
0
Support Repositories with Inner Lakefile
#153
andrewmw94
opened
4 months ago
1
[WIP] Support cedar-lean
#152
andrewmw94
opened
4 months ago
2
(Willing to PR) Support async Python
#151
fzyzcjy
closed
4 months ago
1
Error when entering theorem with doc comment
#149
vasnesterov
closed
3 months ago
2
Tiny change to support Python 3.11
#147
fzyzcjy
closed
4 months ago
2
Minor bug about transitive_dep_graph missing '/lake/packages/std/Std/WF.lean' during locate_premise
#145
zoryzhang
closed
5 months ago
2
v1.7.0
#143
yangky11
closed
5 months ago
0
Next