Dear David, >>> I would guess that this is when running the X86/32 version rather than >>> X86/64. >> >> Yes, I use the 32-bit mode. I will later run some tests when using the >> 64-bit mode. >> >> Here is my current setup: >> >> ISABELLE_BUILD_OPTIONS="" >> >> ML_PLATFORM="x86-darwin" >> ML_HOME="/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin" >> ML_SYSTEM="polyml-5.5.0" >> ML_OPTIONS="--minheap 1000 --stackspace 5000" >> > > You definitely don't want a value as large as 5000. > > I think the exception may be occurring with PolyML.shareCommonData. This > needs memory outside the heap to hold some tables. If there is a lot of live > data in the heap these tables can be large and if the heap is taking up most > or all of the available virtual memory, a particular problem in 32-bit mode, > you may get the above message and exception. Is that possible in this case?
Most of the time, it indeed appears after the theories have been processed, and the heap-file is being generated. (e.g., I never get the error with "isabelle build Check-DPP", only if I build the heapfile with "isabelle build -b Check-DPP") Moreover, I now tested a bit the 64-bit version of poly, and there the error does not occur, even without specifying ML_OPTIONS. For me, this looks like the most sensible solution. > It is safe to handle the exception and continue; it's just that the sharing > process will not be complete so that the heap will be bigger than it might > otherwise be. I see. Thanks for your helpful comments, René _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
