Email Gateway (Aug 22 2022 at 13:44): Email Gateway (Aug 22 2022 at 13:44):From: Holger Ki <holger.ki@freenet.de>
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
Email Gateway (Aug 22 2022 at 13:44):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 26 2024 at 16:20 UTC