[isabelle-dev] Mirabelle and load path

[Alexander Krauss]

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