[isabelle-dev] Testboard problem

Johannes Hölzl hoelzl at in.tum.de
Wed Jun 4 13:37:19 CEST 2014


We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it
works...

I don't know why mira is accessing this file, it actually sets up the
settings file to _not_ look into the users heaps-directory. But it looks
like there is a problem with this setup.

 - Johannes



Am Mittwoch, den 04.06.2014, 10:18 +0200 schrieb Johannes Hölzl:
> Hi,
> 
> a change of mine leads to a failure of the testboard,
> HOL-Proofs-Extraction can not be build anymore.
> 
> For example see:
> 
> http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28
> 
> But when I run on this very changeset the commands
> 
>   isabelle build -b HOL-Proofs-Extraction
> 
> or
> 
>   isabelle build -a
> 
> on my machine, everything runs fine.
> 
> Is there a special setup for the testboard when it runs Isabelle
> makeall?
> 
>  - Johannes
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





More information about the isabelle-dev mailing list