Did y'all know ghci supports commands like :loc-at to support definition at cursor, :type-at for types of expressions at cursor, and :uses-of to find uses at cursor????
I supposed this is how Dante works, and to some degree how Intero works. Interestingly this is similar to how Lean works -- they have a "server" mode that listens for commands on a local port and it speaks JSON.
They're really focused on making Lean usable for pure mathematicians doing research. I'm more interested in programming and program verification so I've felt the documentation was a bit lacking for that audience as well. :)
Did y'all know ghci supports commands like
:loc-atto support definition at cursor,:type-atfor types of expressions at cursor, and:uses-ofto find uses at cursor????Waaaat
and APPARENTLY HAS SINCE 8.01
How am I supposed to use it in the repl though?
you aren't
you're supposed to pipe an editor to the repl
ohhh makes sense!
I supposed this is how Dante works, and to some degree how Intero works. Interestingly this is similar to how Lean works -- they have a "server" mode that listens for commands on a local port and it speaks JSON.
And if you haven't tried it, the developer experience of using Lean is next level. Highly interactive, very cool.
this is amazing! i wrote some shitty vim/tmux/ghci bindings that play together
but my type-of button just pastes in the name
idk if you've tried it, but ghcide also works pretty good and has all these features
Asad Saeeduddin said:
how so? except for the type and local definitions
yes, except for the features it has, it doesn't have any features
well, it's a very small subset of what @Sandy Maguire reported
You're right. It doesn't support
:uses-at. I'm not sure I agree that 2/3 is a very small subset thoughmy point was that it doesn't support definition at cursor for dependencies, which, in my experience, is much more substantial than local definitions
mainly because keeping track of the sources of dependencies, indexing and so on, is a non-trivial task regarding performance and memory usage
@James King What's lean? Haskell ide type of thing? Is there a github for this?
Nvm, found it lol
https://github.com/leanprover/lean
It's a depently typed language and theorem prover: https://leanprover.github.io/
I've been writing a guide for hackers: https://agentultra.github.io/lean-for-hackers/
To me it represents the pinnacle in interactive development.
Hey, thats an awesome write up! The official documentation I found made lean seem like not very attainable. Thats really cool
They're really focused on making Lean usable for pure mathematicians doing research. I'm more interested in programming and program verification so I've felt the documentation was a bit lacking for that audience as well. :)
I would love to see some stuff from agda/lean get brought to haskell tools
Especially the hole interactions for agda