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

Makarius makarius at sketis.net
Thu Apr 13 15:27:11 CEST 2017

On 12/04/17 17:05, Makarius wrote:
> 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".

A more substantial change is now Isabelle/c41791ad75c3.

There might be more boundary cases still open, and the reform of theory
imports is only half through yet (presently at Isabelle/7c40477e0a87).


More information about the isabelle-dev mailing list