Re: [isabelle] Update on I3P



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

--
Holger


PS: While running my existing test suite on a wrapper of your software,
I have discovered a subtle bug in the Scala layer: two x-symbols are mapped
to the same Unicode character.
This bug can affect users: if they open a theory containing
the second symbol and then save it back, the symbol is silently renamed to the
first, which makes the theory file on disk useless for background reading.
I attach below a minimal test case that demonstrates this behaviour to simplify
its removal. (src/HOL uses both symbols, but \\<restriction> only occurs
in Map.thy, so perhaps it is simplest to de-activate that symbol.
The alternative would, of course, be to switch from String to some
richer structure for text management.)

public class ScalaSymbolTest {
    private Isabelle_System sys;
    private Symbol.Interpretation symbols;

    @Before
    public void setup() {
        sys = new Isabelle_System();
        symbols = sys.symbols();
    }

    @Test // this succeeds
    public void encodeDecodeRestriction() {
        check("\\<restriction>");
    }

    @Test // this fails because upharpoonright is mapped to restriction
    public void encodeDecodeRightharpoon() {
        check("\\<upharpoonright>");
    }

    private void check(String name) {
        String orig = name;
        String dec = symbols.decode(orig);
        String enc = symbols.encode(dec);
        assertEquals(1, dec.length());
        assertEquals(orig, enc);
    }

}





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