[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