[isabelle-dev] JinjaThreads

[Clemens Ballarin]

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>==>"
###   ("\<^const>HOL.Trueprop"
###     ("_applC" \<tau>red1'r
###       ("_cargs" P
###         ("_cargs" t
###           ("_cargs" h
###             ("_cargs" ("_tuple" a ("_tuple_arg" xs))
###               ("_tuple" a' ("_tuple_arg" xs'))))))))
###   ("\<^const>HOL.Trueprop"
###     ("_applC" \<tau>red1'r
###       ("_cargs" P
###         ("_cargs" t
###           ("_cargs" h
###             ("_cargs"
###               ("_tuple" ("\<^const>Expr.exp.AAss" a i e)  
("_tuple_arg" xs))
###               ("_tuple"
###                 ("\<^const>Expr.exp.LAss"  
("\<^const>Expr.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.