[isabelle-dev] "No such file" in build
Lars Hupel
hupel at in.tum.de
Wed Apr 12 16:14:21 CEST 2017
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
More information about the isabelle-dev
mailing list