[isabelle-dev] Mirabelle and load path

Makarius makarius at sketis.net
Tue Mar 22 22:17:46 CET 2011

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:


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:


Is this really intended, or just due to the confusing ne "" test?


More information about the isabelle-dev mailing list