Re: [isabelle] question about building HOL on cygwin

This error is caused by a bug in recent versions of SML/NJ. Its lexer dies when it encounters bad ASCII characters. The file you mention has some, in comments of course. I think they are a present from XEmacs :-)

You have several options:

1. Download a recent development snapshot from http:// (Beware, it is not guaranteed to work, and there will be differences from the last official version)

2. Delete the bad characters yourself. They aren't hard to find. Nearly all are in author's names at the beginning of the file. Or a local Perl whiz could set up something to delete all characters that aren't 7-bit ASCII.

3. Download an earlier version of SML/NJ. I think 110.55 and earlier are OK.

Larry Paulson

On 25 Apr 2006, at 06:34, Akira KANEKO wrote:

[opening /usr/local/Isabelle2005/src/HOL/OrderedGroup.ML]
*** exception Fail raised: stuck state

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