Re: [isabelle] replace "isabelle tty"

On Fri, 21 Nov 2014, Lars Hupel wrote:

I hope that sheds some light onto the somewhat delicate procedure. We
could definitely do with more documentation on the system integration
aspect of Isabelle/Scala (which would presumably go into system.pdf,
whose chapter on that topic is very sparse).

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.

I reckon that with the removal of "isabelle tty", more applications of Isabelle/Scala will emerge.

Probably yes, and for two reasons:

  (1) Without the TTY baggage it becomes more feasible to introduce formal
      Isabelle/Scala checking in the documentation, in the sense above.

  (2) Removal of obsolete things makes people active, who are still using
      very old archeological layers of the system.  Actual use of new
      programming interfaces always helps to make them more smooth and
      easier to use.

The Isabelle process protocol concepts covered here are in fact already quite well-established and polished for some years. So now is the right time to convert old applications, and to forget that there was ever a TTY loop in Isabelle.


          925,281 people so far

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