[isabelle-dev] JinjaThreads
JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML 5.3.0). It seems to run out of memory. I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately. Probably this is a known issue, but I don't know where to check for the automatic AFP logs. Clemens macbroy2:admin ballarin$ ./testall JinjaThreads Testing [JinjaThreads] cd /Users/ballarin/isabelle/test/src/HOL; /Users/ballarin/isabelle/test/bin/isabelle make HOL-Word make[2]: Nothing to be done for `Pure'. Building HOL-Word ... Finished HOL-Word (0:00:42 elapsed time, 0:01:13 cpu time, factor 1.73) cd ..; /Users/ballarin/isabelle/test/bin/isabelle usedir -v true -i true -g true -d pdf -V outline=/proof,/ML /Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/HOL-Word JinjaThreads Running HOL-Word-JinjaThreads ... Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Failed to recover - exiting Failed to recover - exiting HOL-Word-JinjaThreads FAILED (see also /Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads) ### (\^const== ### (\^constHOL.Trueprop ### (_applC \taured1'r ### (_cargs P ### (_cargs t ### (_cargs h ### (_cargs (_tuple a (_tuple_arg xs)) ### (_tuple a' (_tuple_arg xs' ### (\^constHOL.Trueprop ### (_applC \taured1'r ### (_cargs P ### (_cargs t ### (_cargs h ### (_cargs ### (_tuple (\^constExpr.exp.AAss a i e) (_tuple_arg xs)) ### (_tuple ### (\^constExpr.exp.LAss (\^constExpr.exp.AAcc a' i) e) ### (_tuple_arg xs') ### Fortunately, only one parse tree is type correct. ### You may still want to disambiguate your grammar or your input. make: *** [/Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads.gz] Error 1 Finished [JinjaThreads] The following tests failed: JinjaThreads Please check logs. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JinjaThreads
Clemens Ballarin wrote: JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML 5.3.0). It seems to run out of memory. I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately. Probably this is a known issue, but I don't know where to check for the automatic AFP logs. The logs are in ~isatest/afp-log. I would assume that you do not need special settings on macbroy2. On smaller machines one must turn off parallelism, I was told. I am not sure where the settings for the AFP tests come from, though... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JinjaThreads
On 19/12/2010, at 8:16 AM, Alexander Krauss wrote: Clemens Ballarin wrote: JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML 5.3.0). It seems to run out of memory. I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately. Probably this is a known issue, but I don't know where to check for the automatic AFP logs. The logs are in ~isatest/afp-log. I would assume that you do not need special settings on macbroy2. On smaller machines one must turn off parallelism, I was told. Specifically for JinjaThreads, the IsaMakefile allows you to set an environment variable JINJATHREADS_OPTIONS (to for instance -M 1). I am not sure where the settings for the AFP tests come from, though... In general, there are no special settings. If you run testall it will use whatever your environment is. The nightly regression tests uses whatever is set as $SHORT (short name for settings) in admin/regression. Currently this is mac-poly64-M4, which in turn you can look up in isabelle/Admin/isatest/settings (-M 4, mac platform, 64 bit, poly 5.3). Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
