[isabelle-dev] mkdir failures

Makarius makarius at sketis.net
Fri Oct 1 17:03:59 CEST 2010


On Fri, 1 Oct 2010, Jasmin Blanchette wrote:

> Last week I experienced strange errors on my machine regarding "mkdir" 
> on my Mac (with Nitpick and Sledgehammer), but these eventually went 
> away after I pulled a newer version of Isabelle.
>
> Now I'm testing on macbroy2 and getting similar errors, but this time in 
> Imperative HOL:
>
> *** Theory loader: failed to load "Imperative_HOL_ex" (unresolved "Linked_Lists", "Imperative_Reverse", "Imperative_Quicksort")
> *** System command failed: mkdir -p '/tmp/isabelle-blanchet45778/Code_Test1375420'
> *** At command "export_code" (line 1018 of "/Users/blanchet/rsync_isabelle/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
>
> Has anybody run into similar issues before?

Yes, it merely means there is an inconsistency between the sources 
(notably lib/scripts/process) and the compiled image.  You merely need to 
make sure everything is compiled afresh.


 	Makarius



More information about the isabelle-dev mailing list