issues
search
leanprover-community
/
repl
A simple REPL for Lean 4, returning information about errors and sorries.
54
stars
12
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
chore: bump toolchain to v4.10.0-rc1
#48
semorrison
closed
4 days ago
0
chore: bump toolchain to v4.9.0
#47
semorrison
closed
4 days ago
0
chore: move to v4.9.0-rc1
#46
semorrison
closed
4 weeks ago
0
chore: bump toolchain to v4.8.0
#45
semorrison
closed
4 weeks ago
0
[BUG] REPL accepts incorrect proofs
#44
amit9oct
opened
1 month ago
6
Issues while executing tactics with `;` in them.
#43
amit9oct
opened
1 month ago
1
Bugs for metavariable '?[anonymous]' when setting "allTactics" as true
#42
xinhjBrant
opened
1 month ago
0
fix: duplicated and misaligned messages and info trees in output
#41
utensil
closed
1 month ago
1
Messages accumulate with wrong positions
#40
utensil
closed
1 month ago
2
chore: bump to v4.8.0-rc1
#39
semorrison
closed
2 months ago
0
chore: bump toolchain to v4.7.0
#38
david-christiansen
closed
3 months ago
0
feat: basic full file mode
#37
semorrison
closed
3 months ago
0
Bug for long commands
#36
xinhjBrant
closed
4 months ago
2
chore: move to v4.7.0-rc1
#35
semorrison
closed
4 months ago
0
chore: bump toolchain to v4.6.0
#34
semorrison
closed
4 months ago
0
fix: NameGenerator bug
#32
semorrison
closed
5 months ago
0
feat: JSON representation of InfoTree in output
#31
semorrison
closed
5 months ago
0
feat: report sorries in tactic mode
#30
semorrison
closed
5 months ago
0
chore: bump for lean4#3159
#29
mhuisi
closed
5 months ago
1
current repl maybe cannot recognize mathcal letter?
#28
ohyeat
opened
6 months ago
7
chore: bump to v4.5.0-rc1
#27
semorrison
closed
6 months ago
0
chore: bump to v4.4.0
#26
semorrison
closed
6 months ago
0
Failed to input the tactics step-by-step within a case block
#25
ohyeat
opened
6 months ago
3
feat: activate scopes when unpickling
#24
semorrison
closed
6 months ago
0
chore: build all of Mathlib in Mathlib tests in case cache is not present
#23
semorrison
closed
7 months ago
0
chore: bump toolchain to v4.4.0-rc1
#22
semorrison
closed
7 months ago
0
chore: bump toolchain to v4.3.0
#21
semorrison
closed
7 months ago
0
chore: bump toolchain to v4.3.0
#20
semorrison
closed
7 months ago
0
Is it possible to query the goal texts in a tactic state?
#19
UltimatePea
closed
7 months ago
3
add more tests
#18
semorrison
closed
7 months ago
0
ensuring failing tests actually fail CI
#17
semorrison
closed
7 months ago
0
Repl doesn't return any output?
#16
Kreijstal
opened
8 months ago
6
feat: support `variable` commands
#15
semorrison
closed
8 months ago
0
feat: add test suite depending on mathlib
#14
semorrison
closed
8 months ago
0
chore: bump lean-toolchain to v4.2.0-rc4
#13
semorrison
closed
8 months ago
0
feat: pickle proof states
#12
semorrison
closed
8 months ago
0
feat: pickle and unpickle Environments
#11
semorrison
closed
8 months ago
0
feat: tactic mode
#10
semorrison
closed
8 months ago
0
bump Lean4; set search path; verify compiled version works
#9
semorrison
closed
10 months ago
0
feat: use Lean.initSearchPath; now works when compiled
#8
semorrison
closed
1 year ago
0
Long inputs
#7
wellecks
closed
1 year ago
3
Iterative execution of proofs
#6
zhangir-azerbayev
opened
1 year ago
2
Python package
#5
zhangir-azerbayev
opened
1 year ago
2
Sorry reporting should pick up term mode sorries as well.
#4
semorrison
opened
1 year ago
0
segfault and panic
#3
zhangir-azerbayev
closed
1 year ago
8
Infinite recursion on empty input
#2
gebner
closed
1 year ago
1
REPL does not enable initialization
#1
gebner
closed
1 year ago
1