Test Lean-Repl bugs #238

New Issue

aniva · 2025-07-11T23:30:40-07:00

aniva commented

2025-07-11 23:30:40 -07:00

We should see if these affect Pantograph:

Sorry capture with local instances: https://github.com/leanprover-community/repl/issues/107
Panic during goal state pickling https://github.com/leanprover-community/repl/issues/81
Referring to self https://github.com/leanprover-community/repl/issues/44

We should see if these affect Pantograph: - Sorry capture with local instances: https://github.com/leanprover-community/repl/issues/107 - Panic during goal state pickling https://github.com/leanprover-community/repl/issues/81 - Referring to self https://github.com/leanprover-community/repl/issues/44

aniva added this to the v0.3.5 milestone 2025-07-11 23:30:40 -07:00

aniva added the

part/Goal

category

bug

labels 2025-07-11 23:30:40 -07:00

aniva self-assigned this 2025-07-11 23:30:40 -07:00

aniva changed title from ~~Test capture of local instances~~ to Test Lean-Repl bugs

2025-07-11 23:34:52 -07:00

aniva added a new dependency 2025-07-12 12:09:05 -07:00

#239 Pending mvars cause generation of closures

Sign in to join this conversation.