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
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
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
As is, incidentally, the idea of the facade pattern.
Why is a foundational concept like Isbelle_System called "facade" here?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and