Re: [isabelle] Unicode (Was: Update on I3P)


Am Montag, den 20.09.2010, 13:43 +0200 schrieb Holger Gast:
> >>> I should add that this sequence of four characters is the utf8
> >>> representation of 𝒵 (\<Z>), re-encoded as utf8:
> >>> $ echo -n ð??µ|iconv -futf8 -tlatin1
> >>> 𝒵
> >>> $ echo -n 𝒵 | iconv -flatin1 -tutf8
> >>> ð??µ
> >>>
> >>> Maybe i3p has problems with unicode character code points that do not
> >>> fit in one 16-bit number?
> Not in general; when adding the support for true code points in August,
> I already wrote a number of tests to ensure that theories do not get broken
> by editing them. Unfortunately, this did not catch a remaining bug
> in the on-the-fly encoding in the driver ;(
> This is fixed now (check for updates) and a corresponding test is added
> to make sure it will work more smoothly in the future.

thanks. Unfortunately, the auto-updater does not work for me (no idea
why, "strace -e network" does not show anything obvious and I have no
proxy...). Anyways, I prefer installing updating software manually :-)

I have another issue with i3p to report that is more severe. In my
current project, I sometimes get quite large goals. When that happens,
i3p becomes very slow when I move backwards and forwards in my theory.
My ProofGeneral using colleges do not have this problem.

You can check yourself if you clone git://,
checkout revision b625bc51b6a4372f73d807dcd4e79ccedcf2a530 and run
CFGraph/HOLCFExSV.thy (the final lemma fails in this revision, don’t
worry about that). This took >15 minutes on my machine. I then reduced
the size of the goals by replacing
	proof (cases "(d,ds,ve,b)" rule:fstate_case)
	proof (cases "(d,ds,ve,b)" rule:fstate_case,
	       auto split:d.split prim.split simp del:Un_insert_left Un_insert_right)

which is probably bad style but helped me reduce the time to run the
theory to a bearable 1min15s. This is of course a rather big issue, as I
might not always be able (or willing) to find a work-around like this. 

Is there anything that can be done about this, or is this an inherent
consequence of the i3p design?

Nevertheless I’m a happy i3p user,

Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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