On 03/22/2011 10:17 PM, Makarius wrote:
It seems to have recovered, e.g. in 626fcf4a803e. Are you now the Mirabelle maintainer?
I wouldn't go that far, as I know nothing about most Mirabelle internals. I just needed to use it, so I fixed it with Sascha's help. This is part of another attempt to make the Judgement Day benchmarks continuous.
MIRABELLE_OUTPUT_PATH=/tmp/mirabelle MUTABELLE_OUTPUT_PATH=/tmp/mutabelle Such strong assumptions about exclusive access to global resources --- hardwired into the default settings --- are apt to cause more surprises.
I tried to fix this in 6a147393c62a for Mirabelle. If it doesn't produce new crashes, we can do the same for Mutabelle.
I also wonder about mirabelle -q, which produces strange messages in the regular makeall setup: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l134 http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l139 Is this really intended, or just due to the confusing ne "" test?
Maybe Sascha can comment on this (cf. f20cc66b2c74). If in doubt, we might just kill the two lines.
Alex _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
