Re: [isabelle] Isabelle and the text console



What you ask has been impassable for 10 years or more. Even if it were possible, you would be taking a massive hit on productivity. The closest approximation is that you can work in a completely batch style, editing proofs in a plain text editor and then compiling them. Be a very slow and frustrating business.

Larry Paulson


> On 7 Jul 2016, at 16:59, Holger Ki <holger.ki at freenet.de> wrote:
> 
> Hi,
> 
> I'm new to isabelle/hol, and I'm currently figuring out how I might use
> the system for interactive theorem proving under Linux.
> 
> I'm not entirely new to formal proofs, I have a bit of experience
> with coq.
> 
> Now my question:
> I can't use GUIs for technical reasons, and prefer to do stuff in the
> shell anyways.
> 
> From reading isabelle documentation and grepping through this list's
> archives I understand that there is no real user interface for text
> terminals (anymore?). Is that correct?
> 
> I found isabelle process and isabelle console, but it seems, they are
> not intended for manual use. :)
> 
> What would be the best approximation to a REPL interface (e.g. like the one
> that coqtop provides), for isabelle/hol?
> 
> Or maybe I overlooked something and a interactive system can be
> easily instanciated from isabelle console?
> 
> Thank you very much,
> 
> Holger
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.