Re: [isabelle-dev] "No such file" in build
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). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "No such file" in build
> For the moment it should work if you use an absolute path like -d > "$PWD/Lem". Yes, that works. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "No such file" in build
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] "No such file" in build
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