Re: [isabelle] Proof by analogy and proof stability in Isabelle

On Sat, 29 May 2010, Lucas Dixon wrote:

On 30/04/2010 16:09, Makarius wrote:
Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25
months between the releases and the result being rather unstable. At
that time it was not completely clear if we would ever recover from a
continously "intermediate" state, and join the fate of notorious
projects such as SML/NJ or the STIX fonts.

I just noticed that STIX have released version 1 of their fonts (May 24th 2010); does anyone have experience with using them for Isabelle?

I've tried it just a few hours after it came out. My impression is that the quality as a screen font is not ideal, but this might be due to my homegrown conversion from OpenType to TrueType via fontforge. The latter does not treat all details of the hinting according to its author. Does anybody have a high quality font converter?

I would be particularly interested to know if it was possible to get a fixed-width version of the font. I don't anything about font-design, is this a very hard thing to do?

The STIX people spent the first half of all these years counting only glyph coverage. Then they noticed that the spacing between glyhps is just as hard, and spent five more years on it.

Anyway, the last time when Isabelle symbol fonts were discussed on the list I promised not to get involved in it again. But after projecting the expected quality of STIX on the JVM -- which is particularly bad -- I've had another go at it some months ago. The resulting IsabelleText font is actually quite nice as a pseudo-fixed width screen font and will be shipped with the next Isabelle release, i.e. within the next few weeks.


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