Re: [isabelle] Update on I3P
> 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.
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
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and