I've just updated Isabelle (f3cd78ba687c) and am getting an odd error
message for "isabelle build":
*** No such file:
"/home/lars/work/reify/verified-codegen/Lem/Lem/Lem_pervasives.thy"
*** The error(s) above occurred for theory "Lem_pervasives"
This is the invocation:
isabelle build -bv -d Lem/ LEM
This is the ROOT file (Lem/ROOT):
session LEM = HOL +
description {*
HOL + LEM specific theories
*}
theories Lem_pervasives Lem_pervasives_extra
I'm unsure why Isabelle is trying to load "Lem/Lem/Lem_pervasives.thy"
instead of "Lem/Lem_pervasives.thy" (the latter of which exists).
If I move the ROOT file to . and rewrite it as
session LEM in Lem = HOL + ...
the behaviour is unchanged. Calling "isabelle build -l" correctly shows
that it should be looking for Lem/Lem_pervasives.thy".
Cheers
Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
