|
From: Jens B. <br...@in...> - 2004-01-12 13:44:08
|
Due to a bug in Moscow ML 2.00, it seems that new types cannot be created i=
n=20
HOL any more. All definitions throw an overflow exception:
=2D new_type("s",0);
! Uncaught exception:
! Overflow
After a closer look, the error is caused by the function dest_time in
"hol/src/portableML/Portable.sml", which uses toSeconds of the MosML librar=
y.
This function does not work any more, because the value returned by it is=20
greater than the maximum possible integer 2^30-1=3D1073741823.
Moscow ML version 2.00 (June 2000)
Enter `quit();' to quit.
=2D load "Time"; open Time;
> val it =3D () : unit
=2D > type time =3D time
val fromSeconds =3D fn : int -> time
[...]
val fromMilliseconds =3D fn : int -> time
=2D toSeconds(now());
! Uncaught exception:
! Overflow
=2D toReal(now());
> val it =3D 1073912178.66 : real
I reported the bug to Peter Sestoft.
Regards,
Jens Brandt
=2D-=20
Jens Brandt
AG Reaktive Systeme, Fachbereich Informatik
Technische Universit=E4t Kaiserslautern
http://rsg.informatik.uni-kl.de
|