search

FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.66k stars 230 forks source link

Separate data and control in REPL protocol #366

Closed s-zanella closed 7 years ago

s-zanella commented 8 years ago

See #361 to see why combining the two is a bad idea and how it's done in Dafny.

catalin-hritcu commented 8 years ago

I think the current interaction protocol was a quick fix Nik implemented, but was never supposed to be the end of the story. We could of course try to incrementally improve it, but we could also look at the standard interaction protocols for proof assistants: in particular Proof General's (both the implemented one and the proposed replacement Proof Kit / PGIP http://proofgeneral.inf.ed.ac.uk/kit) and the more modern and less emacs specific PIDE (Prover IDE) framework which Isabelle and now Coq (http://www4.in.tum.de/~wenzelm/papers/coqpide.pdf) support.

One more thing to look at: CoqPIE: A Coq IDE Aimed at Improving Proof Development Productivity http://cps-vo.org/node/19241

cpitclaudel commented 7 years ago

PGIP is mostly dead IIUC, and the current pG is just based on looking for prompts sent by a REPL. INRIA has been working on porting PG to Coq's custom XML-based async protocol. CoqPIE is just a UI on top of the regular REPL-based coqtop. The dafny protocol is REPL-like too (I wrote it during my internship two years ago), and documented at https://github.com/boogie-org/boogie-friends/blob/master/emacs/inferior-dafny.el#L54.