[isabelle-dev] Mirabelle and load path

[Makarius]

On Fri, 4 Mar 2011, Alexander Krauss wrote:

> Unfortunately, Mirabelle is broken since aa8dce9ab8a9

It seems to have recovered, e.g. in 626fcf4a803e.  Are you now the 
Mirabelle maintainer?


Since it is now also run as part of the standard test, some further things
are needed to make it work for > 1 users running > 1 processes;
isatest has already crashed on these global settings:

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 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?


 	Makarius