On 03/11/17 16:36, Fabian Immler wrote: > > > I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap > 1600 --maxheap 4000" if that is relevant). > Invoked with "isabelle build -d . -othreads=8" for the theory below. > > polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu > time, factor 6.94) > polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor > 4.70) > > Both are in isabelle/123670d1cff3 > > theory Check > imports Pure > begin > > ML_file \<open>check.sml\<close> > ML \<open>timeap Check.check (0 upto 7)\<close> > > end
Just for the record, here are my test results for this setup: lxcisa0, x86_64-linux, threads=6. log1.gz: polyml-5.6-1 Finished Check (0:00:56 elapsed time, 0:03:01 cpu time, factor 3.21) log2.gz: polyml-test-e8d82343b692 Finished Check (0:02:50 elapsed time, 0:13:25 cpu time, factor 4.72) log3.gz: polyml-NewTestRegisterSave Finished Check (0:02:53 elapsed time, 0:13:36 cpu time, factor 4.72) log4.gz: polyml-test-e8d82343b692 ML \<open> structure IntInf = struct open IntInf fun pow (i, n) = Integer.pow n i; end \<close> Finished Check (0:00:39 elapsed time, 0:02:01 cpu time, factor 3.06) The logs contain profiling information at the bottom. Here is are the relevant bits of log2.gz vs. log4.gz (produced with "isabelle profiling_report): 229 IntInf.divMod 256 Check.approx_floatarith 261 IntSet.mergeLists 281 Check.map 306 GARBAGE COLLECTION (total) 352 Check.divide_inta 468 Check.float_plus_down 3155 Check.log2 33415 IntInf.pow 234 Check.approx_floatarith 245 IntSet.mergeLists 276 Check.divide_inta 307 GARBAGE COLLECTION (total) 321 Integer.pow 323 Check.float_plus_down 1514 IntInf.divMod 2946 Check.log2 The problem is de-facto solved by the workaround in Isabelle/17eb23e43630. Makarius
log1.gz
Description: application/gzip
log2.gz
Description: application/gzip
log3.gz
Description: application/gzip
log4.gz
Description: application/gzip
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev