Re: [isabelle] Update on I3P



On Tue, 20 Jul 2010, Holger Gast wrote:

- It is very hard to locate the functionality that is there.
 For instance, after listening two of your talks which presented
 the Scala layer as a whole, I did not expect that there was some
 re-usable functionality just for encoding/decoding symbols.
 It always a appeared as a "whole", which could be used entirely
 or not at all.

Did you attend my recent tutorial on Isabelle System programming at Cambridge? The transscript http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/cambridge%20tutorial/file/d866d33b15d5/T06_System.thy gives you a practical overview of the main entry points.

I have also explained the importance of Isabelle_System and its many basic services like symbols more than once in private.


- Now the facade class Isabelle_System is certainly a nice idea,
 since it lists the basic entry points into the system.
 However, to use it, one has to have an Isabelle installation
 available.

Isabelle_System is really the very foundation of anything built on top of the Isabelle environment. Without that you can hardly do anything useful.

Historically, Isabelle_System used to be implicit in the process environment of Isabelle tools, later I made it an explicit object, only to figure out further on that only one instance will really work within a given JVM process. The reason for that are certain "globalities" of the JVM itself, i.e. consider low-level character encodings or input methods (both are not yet implemented). The registering of Swing fonts is another once-and-for-all thing, and it *is* implemented right now to spare users going through the pain of installing fonts manually on the system.

You cannot easily juggle various Isabelle system installations without disintegrating the Isabelle platform and reassembling it differently, loosing overall hull integrity in the process.


 And this is what makes the library useless for me:
 I simply cannot display the raw xsymbol notation until the user
 has selected the Isabelle installation. User's won't accept it.

This merely indicates that the present I3P architecture does not fit to Isabelle as of 2009 or later.


- Make re-usable functionality accessible with minimal assumptions.

 For instance, the font support from Isabelle_System is not really
 tied to a particular installation.

It is, because you cannot even read files in a robust (and platform independent manner) without Isabelle_System being around. These fundamental system integrity structures are very delicate, and I've spent a long time to make them work robustly, while minimizing assumptions routinely.


As is, incidentally, the idea of the facade pattern.

Why is a foundational concept like Isbelle_System called "facade" here? Very strange.

It is important to understand that Isabelle/Scala is our way to reach out to the JVM platform. Just because some other languages happen to live on the same JVM runtime environment does not mean that we take over their worldview -- neither that of Java, nor that of Clojure etc.

Compare this to Isabelle/ML: it is based on the Poly/ML runtime system, which is itself implemented in C++ and runs native machine code generated from ML. Nobody would start thinking in terms of C++ / assembly language in Isabelle/ML, of course.


Isabelle/Scala is about transferring established Isabelle/ML traditions as closely as possible, while honoring the intrisic virtues of the Scala/JVM platform -- e.g. using Scala actors, which do not have a counter part on the ML side. You will have a hard time understanding Isabelle/Scala with a Java mindset.


	Makarius





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