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

2017-04-12 Thread Lars Hupel 
> 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

2017-04-12 Thread Makarius 
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

2017-04-12 Thread Lars Hupel 
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

[isabelle-dev] NEWS: main theory entry points

2017-04-12 Thread Makarius 
*** General ***

* The main theory entry points for some non-HOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:

  CTT/Main.thy~>  CTT/CTT.thy
  ZF/Main.thy ~>  ZF/ZF.thy
  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
  ZF/ZF.thy   ~>  ZF/ZF_Base.thy

INCOMPATIBILITY.


This refers to Isabelle/5febea96902f. It belongs to cleanup and
clarification towards session-qualified theory names, with the exception
of a few important global entry points like "Pure", "Main", "Complex_Main".


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Access problems to repositories and NFS

2017-04-12 Thread Tobias Nipkow 



On 12/04/2017 14:29, Makarius wrote:

On 11/04/17 09:34, Lars Hupel wrote:


In order to keep going with development, I've created a temporary clone
on Bitbucket: 

I'm in the process of inviting people to that clone so they can keep
working. I'll also update the URLs in Jenkins shortly.

If you need to push but I forgot to add you, please mail me your
Bitbucket user name and I'll add you ASAP.

I hope that this is just a temporary workaround (famous last words, I
know ...).


lxbroy10 is back to normal, see the proof
http://isabelle.in.tum.de/repos/isabelle/rev/f3cd78ba687c



Indeed it is, thanks to the invaluable help of Franz Huber. However, he spoke of 
a workaround when he notified us and wasn't 100% certain it works reliably. I 
felt we should wait a few more days before we move the repo back, but I am easy 
either way.


Tobias


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Access problems to repositories and NFS

2017-04-12 Thread Makarius 
On 11/04/17 09:34, Lars Hupel wrote:
> 
> In order to keep going with development, I've created a temporary clone
> on Bitbucket: 
> 
> I'm in the process of inviting people to that clone so they can keep
> working. I'll also update the URLs in Jenkins shortly.
> 
> If you need to push but I forgot to add you, please mail me your
> Bitbucket user name and I'll add you ASAP.
> 
> I hope that this is just a temporary workaround (famous last words, I
> know ...).

lxbroy10 is back to normal, see the proof
http://isabelle.in.tum.de/repos/isabelle/rev/f3cd78ba687c


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev