Discussion:
[isabelle] Isabelle and the text console
(too old to reply)
Holger Ki
2016-07-08 09:59:32 UTC
Permalink
Raw Message
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
Lawrence Paulson
2016-07-08 10:19:06 UTC
Permalink
Raw Message
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
Post by Holger Ki
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.
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
Loading...