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.
> On 7 Jul 2016, at 16:59, Holger Ki <holger.ki at freenet.de> wrote:
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and