On Mon, 4 Mar 2013, Peter Vincent Homeier wrote: > There was a bug in the previous version of the HOL-Omega system which > prevented it from building with Poly/ML 5.5, the current version of Poly/ML. > > This has been fixed and posted to the public repository for HOL-Omega, > and the current version should build correctly. If anyone has tried > building HOL-Omega and been frustrated, please try again with this new > version of HOL-Omega.
In your changeset https://github.com/mn200/HOL/commit/9b92ae9 you say ... caused a type error with Poly/ML version 5.5. This is a difference from Poly/ML version 5.3. Does it mean you were still using old Poly/ML 5.3 until recently? For Isabelle, the advances from 5.3 to 5.4 to 5.5 made a big difference in performance. 5.5 is particularly nice, since it allows to run even big sessions in plain-old 32bit address space -- due to the online sharing of immutable data that David Matthews is doing now for all of us. How is the situation for HOL4 concerning Poly/ML performance? Makarius ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
