[isabelle] question about building HOL on cygwin
I tried to install Isabelle/HOL to my cygwin.
I first installed SML/NJ which seems working well.
I then installed Isabelle and tried to build HOL.
But I got the following error message. I am afraid something is
wrong in the HOL source. I think so because
1) The build of FOL and ZF was successful and seems working well.
2) I tried the same thing with Linux and FreeBSD, and I got the
same error message at the same place.
I thought that a heap file made with SML/NJ for Linux would work,
but I could not find any. The Isabelle Home Site presents only
one build with PolyML, but I could not install PolyML to my
cygwin. It seems that the Windows binary of PolyML distributed by
the site does not work with Isabelle.
Could you give me an adequate suggestion?
(see also /usr/local/Isabelle2005/heaps/smlnj-110_x86-cygwin/log/HOL)
lemma diff_def: ?x - ?y == ?x + - ?y
lemma add_minus_cancel: ?a + (- ?a + ?b) = ?b
lemma minus_add_cancel: - ?a + (?a + ?b) = ?b
[| ?a <= ?b + ?c; ?c <= ?d |] ==> ?a <= ?b + ?d
lemma estimate_by_abs: ?a + ?b <= ?c ==> ?a <= ?c + abs ?b
*** exception Fail raised: stuck state
*** At command "use".
This archive was generated by a fusion of
Pipermail (Mailman edition) and