[isabelle-dev] "No such file" in build

Makarius makarius at sketis.net
Wed Apr 12 17:05:57 CEST 2017


On 12/04/17 16:14, Lars Hupel wrote:
> 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

For the moment it should work if you use an absolute path like -d
"$PWD/Lem".


	Makarius





More information about the isabelle-dev mailing list