Re: [isabelle] Update on I3P

Dear Makarius,

> 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
  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

  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 MHonArc.