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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev