[racket] DrRacket, Emacs, REPL [was: Sending s-expr to repl]

> See
> http://blog.racket-lang.org/2009/03/drscheme-repl-isnt-lisp.html
> for a detailed answer.
> 

I see what the blog post above is saying, but (I know, "no when no if no but"), has anyone ever used editors for some of the proof assistants, like CoqIDE or ProofGeneral mode in Emacs for Coq? These support a seemingly nice compromise between the two styles. A minor annoyance I have with the DrRacket model of reloading the entire buffer is that if I have several working functions defined at the top of the file, and then a new function I'm working on below that has syntax errors or is in incomplete template form or whatever, running the file generates an error and no definitions at all are loaded into the REPL. So instead, in these proof editors, they have this feature where you can load the buffer up to a certain line/expression (assuming no syntax errors), and everything above there is then in a "locked" (uneditable) mode -- if you edit something, it rolls back the evaluated portion of the file. This way, you can have a bunch of messy/incomplete thoughts typed up at the bottom of your file, and have all good definitions up to a certain point in your file evaluated so that you can play with the evaluated definitions in the REPL, to help you fill in your unfinished thoughts. I know, this will get messy in the presence of effects (proof languages are purely functional), and probably a lot of work to implement, but something to think about...


--- nadeem