On Tue, 28 Apr 2015, Larry Paulson wrote:
Today I added some material about complex transcendental functions, and
then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and
HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the
latter.
I am presently not on the isabelle-dev repository, but here are some
hints nonetheless.
### theory "XML_Data"
### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
*** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
***
*** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")
Unfinished session(s): HOL-Proofs-ex
The Size exception above refers to this example:
text {* Some fairly large proof: *}
ML_val {*
val xml = export_proof @{thm Int.times_int.abs_eq};
val thm = import_proof thy1 xml;
@{assert} (size (YXML.string_of_body xml) > 50000000);
*}
It means that the text representation of the proof term is bigger than
64MB, which is the limit of heap objects for Poly/ML on x86. This may be
seen as a reminder of invisible concrete walls that surround the whole
game of ever growing proof libraries, walls that David Matthews has
continuously moved further to enlarge the playground. One day we will
have to give up x86, though, and the entry to the game will be 16 GB
memory.
For now it should be possible to find a different example with a smaller
proof object instead of Int.times_int.abs_eq above, or to tune the proof
of Int.times_int.abs_eq to reduce its recorded term size -- there might be
something bad elsewhere that causes the sudden increase of size.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
