[isabelle] Fwd: replace "isabelle tty"



Dear Walther,

There is also a different approach to simulating the TTY/ProofGeneral
interaction with Isabelle.

I have written a small 20-line script that lets me imitate
minimal Isar-interaction via isabelle-console. It only allows
sending single lines to Isabelle, there is no "back" or error
handling, but this is enough for simple sending of commands to
Isabelle and analysing their outputs.

The reason why I use this script, is because I use Isabelle
on a headless server. It has enough memory to do bigger
experiments, but I cannot run graphical applications there,
in particular I cannot run PIDE. As ProofGeneral and TTY
support have been removed, I needed to implement some minimal
interaction, and the minimum, following the indispensable
help from Makarius is:

The script runs:
  "isabelle console",
Then sends it:
  "val s = Toplevel.toplevel;"
And for every line of user input sends:
  "val s = fold (Toplevel.command_exception true) (Outer_Syntax.parse
Position.start \"%s\") s;"

I suppose this could be extended to support a "go-back" or even
some more complicated protocol like the one from ProofGeneral
which I presume you are currently using.

Attached, sorry for yet another programming language, but the
above should explain it.

Regards,

Cezary

On Fri, Nov 21, 2014 at 4:22 PM, Lars Hupel <hupel at in.tum.de> wrote:
>> Isabelle/Scala is indeed the main system programming language for
>> Isabelle, so the manual should say more about it.  The reason why so
>> little Isabelle/Scala is in the manuals is that code snippets cannot be
>> formally checked, as is done for Isabelle/ML. Without formal checking,
>> it is pointless to make examples, because they will stop working in no
>> time, after the next round of refinements of the system implementation.
>
> Indeed.
>
> What could be done is writing a minimal PIDE application demonstrating
> bi-directional communication, possibly in the style of literate
> programming. This could then be executed and tested as part of a regular
> (nightly?) build against the repository version.
>
> Cheers
> Lars
>



--
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/

Attachment: isatty.ml
Description: Binary data



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