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
