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
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to