Email Gateway (Aug 18 2022 at 15:24): Email Gateway (Aug 18 2022 at 15:24):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Isabelle users,
I'm happy to announce release 1.0.2 of I3P,
the Interactive Interface for the Isabelle Prover.
The new version is available from
http://www-pu.informatik.uni-tuebingen.de/i3p/
It supports both the Isabelle2009-2 release
and Windows/Cygwin installations.
Those who are already using I3P can just employ
the Tools/Plugins dialog to download the updated modules.
I'd like to thank all users who have given me
feedback on the first version. I hope that the
changes made based on the suggestions about usability
are as expected.
Enjoy,
Holger
Email Gateway (Aug 18 2022 at 15:40):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Holger,
three quick remarks:
In Options, Fonts & Colors, Highlighting, I had to disable the
„Highlight Caret Row“ background color, otherwise I would not see how
far the code in the current row has been evaluated.
Using the IsabelleText TrueType font that comes with Isabelle-2009-2,
I can not display a few special characters, especially \<guillemotleft>,
\<guillemotright> and \<one>. These are shown as a black square. Is that
a problem with i3p, the font, or something else?
Calligraphic math (e.g. \<F>) is shown as "\<F>". A unicode codepoint
is available for that: U+2131 SCRIPT CAPITAL F. Could this be improved?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:40):From: Makarius <makarius@sketis.net>
The font should be OK. You can test it as follows:
Isabelle2009-2/bin/isabelle jedit Isabelle2009-2/etc/symbols
Assuming that this file has been loaded with the encoding
"UTF-8-Isabelle", which is the default configuration here, you will see
the decoded version of the standard symbol encoding table of the Isabelle
system. Users can add further symbols in $ISABELLE_HOME_USER/etc/symbols
There is a fairly straight-forward Isabelle/Scala interface to use this
information in JVM-based applications, but I3P still ignores that,
shipping its own (faulty) tables instead.
Makarius
Email Gateway (Aug 18 2022 at 15:41):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hi Joachim,
Thanks for pointing this out; these issues are fixed.
Also, I have taken the opportunity to add to the theory editor
an auto-completion box which pops up when you start typing a symbol
name with \<... and can also be triggered as usual by Ctrl-space.
Those who have already installed I3P, just use "check for updates".
Thanks to Makarius for pointing out that there is an official stable
mapping from symbol encodings to Unicode characters.
Email Gateway (Aug 18 2022 at 15:41):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Makarius,
For me as a possible user, the current form in which this
functionality is available is not very attractive. I hope that the
following feedback on how a user might approach the library helps
in improving the experience for others.
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.
After your remark, I therefore looked through the sources
(since there is not proper API documentation) and found the
object Symbol in General/symbol.scala. The Interpretation class
inside looked just as if I could use it, and I was quite pleased.
It turns out, however, that the constructor of Interpretation
already expects some pre-processed form of a table with
xsymbol encodings. How could I ever provide this?
After some find-grep in the Emacs, the only call to the
constructor is in Isabelle_System.
It retrieves the file from etc/symbols.
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.
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.
I suspect that the startup functions for the jedit implementation
somehow get hold of "the startup installation", and then use that.
If the library is to be re-used in different contexts, as
you imply by your remark, this may not be so easy. Re-usability
just is not for free ;(
It may be that my procedure was not the expert one, but this is
not the point; what I would like to convey is some feedback on how
users might approach the library.
Also, from a prospective library user's point of view, two
rather minimal improvements would be most helpful
(I formulate them as suggestions, for brevity):
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 could as well be offered as
a separate JAR, which would bundle the Isabelle Text font, the
symbols table, and the Symbol class.
I suspect that similar sub-functionality can be found and extracted
in other places as well. The Isabelle_System might, of course,
still offer the font support by instantiating the package.
(As is, incidentally, the idea of the facade pattern.)
Provide a minimal overview documentation of all entry points and packages.
The strategy of placing Scala and ML files side by side in the sources
is very helpful for keeping them consistent, but for the user it means
that it is very hard to find specific things they might be looking for.
An example of a good solution is the Netbeans list of modules. Each module
has a two-line description, such that the user can quickly identify
the relevant ones.
Make very clear in the documentation of classes which methods
you consider for public use and which are "public" only for
technical reasons.
For the public ones, a one or two sentence summary of their
functionality would be most helpful.
Provide simple test cases that demonstrate the usage of the re-usable
functionality.
If users have to read sources to understand what a particular method
does, this means they have to spend a lot of time on things that they
would consider as "done" and "just usable". For you, as the developer,
on the other hand, it is simple to write a few lines of example code
in the form of automatic tests that demonstrate particular use scenarios
that you have foreseen and also plan to support. The user can then proceed
by example, which simplifies development a lot.
Again: the remarks are to reflect a user's perspective.
I hope that they will help to make the emerging Scala layer
more attractive from the technical side, since certainly the
idea of _having_ a well-defined API for interacting with the
Isabelle system already is very attractive.
Holger
Email Gateway (Aug 18 2022 at 15:42):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 15:42):From: Alexander Krauss <krauss@in.tum.de>
Hi Holger,
I simply cannot display the raw xsymbol notation until the user
has selected the Isabelle installation. User's won't accept it.
I would happily accept such a minor limitation. We are used to quite
other things. Most users won't even notice, assuming that the Isabelle
installation is selected as part of some installation process.
Alex
Email Gateway (Aug 18 2022 at 15:43):From: Holger Gast <gast@informatik.uni-tuebingen.de>
- Make re-usable functionality accessible withinimal 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.
I understand from this that the Scala layer will not support my use case.
I have therefore simply developed the standalone module that I suggested.
Since others may find it useful in building xsymbol-based interfaces
(it is independent of I3P), it is available here:
http://www-pu.informatik.uni-tuebingen.de/i3p/
It only makes use of standard Java library mechanisms and should
therefore run anywhere. (Of course, I also tested it under
Linux, Windows, and MacOS.) As I proposed, demo code and test cases
showing the basic supported use scenarios are included in the files.
The development has a nice side-effect:
Users of I3P do not have to install & configure fonts anymore.
Did you attend my recent tutorial on Isabelle System programming at
Cambridge? The transscripthttp://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.
Thank you for mentioning this, because it illustrates very well what I
wanted to point out about documentation from a user's perspective:
that workshop was attended by around 25 people, most of whom were in fact
not interested in user interfaces, but in the prover. Anybody who did
not happen to be at the meeting would have to guess that the
font-related functionality is there and find the information by googling
"Scala Isabelle fonts" (The NEWS file comes up 4th, the tutorial is 7th.)
My point is that the Scala library would be used much more widely, and
that the substantial and in-depth work that it represents would be
recognized more generally, if its use was simpler. In particular,
to be effective, documentation needs to be placed where users are looking
for it. The canonical place is, of course, the standard output of
the scaladoc tool. (The raw .html files with the signatures are already there.)
Writing the basic documentation for a class takes the developer
about 10-15min (compare this to the development time for the code).
Retrieving the same information from different slides, tutorials, papers and
NEWS files takes each (!) user at least 20-30min, provided
they suspect its existance. It is clear that providing the documentation
beforehand makes the overall use of the library much more effective.
Anyway, I think we should discontinue this thread on the mailing list,
since it does not seem to lead to further results.
I am, of course, always available for offline technical discussions.
Last updated: Apr 24 2024 at 16:18 UTC