[isabelle-dev] Testboard problem

2014-06-04 Thread 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

Re: [isabelle-dev] Testboard problem

2014-06-04 Thread Johannes Hölzl
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,

Re: [isabelle-dev] Towards the Isabelle2014 release

2014-06-04 Thread Lawrence Paulson
Didn’t we agree that a “backward compatibility mode” declaration (restoring the former behaviour) would have to be available? That should make repairing legacy proofs trivial. Naturally we would like to gradually port some of these developments to do things the new way, but only some of them,

Re: [isabelle-dev] Testboard problem

2014-06-04 Thread Lars Noschinski
On 04.06.2014 13:37, Johannes Hölzl wrote: 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

Re: [isabelle-dev] Towards the Isabelle2014 release

2014-06-04 Thread Thomas Sewell
Indeed, there is a backward compatibility mode declaration. In fixing things, I've been trying to use it as little as possible and as locally as possible. Perhaps I should be bolder. I'm aesthetically against using the compatibility mode all over the place, since I feel that it's just