Closed ericrbg closed 2 years ago
I have merged the multi-language support in master, so the lean branch now only has lean-specific commits (yay). The rebase should be straightforward (just pick the top two commits).
I pushed some cleanup patches on top of your branch, please have a look and let me know (things didn't compile for me as-is). I also removed the __repr__
of Position
since it broke some doctests.
I think the last major step is to adjust the --ast
call so that it uses run_cli
(and so that it doesn't show the debug output). One question: does the code prevent a goal from proof n+1
from being displayed on the last sentence of proof n
? (Maybe we should handle each top-level proof block separately?)
I will look at the transform issue tomorrow.
Your changes all seem reasonable, yeah :) there's a couple more todos that I'll sort after lunch, then I'll get onto lean4 :)
omg I just realised I didn't push the work that I did before the weekend! So sorry :( let me at least push this whilst I finish off the literate support right now
also a core problem: at the end of files, if there's no space and you're just hovering, you'll get dodgy scroll behviour (try hover over the end
at the very end here). i can dig for a fix, but not sure if/how you want to fix it
Rebased, cleaned up, and merged into master; thanks Eric!
This is a very light PR for now. This breaks Lean support for all Lean versions not including leanprover-community/lean#612, but in exchange gives far more reliable parsing of tactics. Some future work to improve: