[isabelle-dev] Testboard problem
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
Re: [isabelle-dev] Testboard problem
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
Re: [isabelle-dev] Towards the Isabelle2014 release
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, and not immediately. Backward compatibility will be necessary for users, even if not for us. Larry On 4 Jun 2014, at 06:27, Thomas Sewell thomas.sew...@nicta.com.au wrote: I had hoped to have the change I was making to hypothesis-substitution ready for the coming release. I've got it working for all of HOL and the library, and begun looking at the AFP and at the l4.verified proofs. The HOL+library changes were easy enough, but the l4.verified changes are somewhat daunting and I haven't gotten anywhere with the AFP yet. I'll have another look at it, because I'd like this to go somewhere at some point. It might have to wait for a subsequent release though. Cheers, Thomas. On 30/05/14 21:30, Makarius wrote: The summer is getting close, and we need to start thinking about the coming release. I am myself on vacation during most of June. On return I would like to wrap up rather quickly, so that we can publish Isabelle2014-RC0 in the second week of July, for the Isabelle tutorial at VSL2014 Vienna. That will be still within the main Isabelle repository. The usual fork to the release repository and the regular sequence of Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014. I am myself attending the mega event at Vienna 13..19-Jul-2014. This will be also an opportunity to show me personally remaining snags, and to continue the elimination of remaining uses of Proof General. (It is getting harder and harder to construct counter-examples to the claim that this set is already empty.) Makarius ___ 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard problem
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 with this setup. After looking a bit closer: Mira changes ISABELLE_HOME_USER (by appending it to $ISABELLE_HOME/etc/settings). Of course, this is too late to affect ISABELLE_PATH, which still refers to $USER_HOME/.isabelle/heaps. So, we set $USER_HOME instead before starting Isabelle (see bcc6dc6c1d1c8a6). @Makarius: Does this use fit the intention of USER_HOME? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the Isabelle2014 release
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 mysterious. Of course, a lot of Isabelle proof scripts are a bit mysterious already. In particular, I want to avoid ever changing the setting globally. I've had some bad experiences in the past with theories with differing global configurations, which means that the location of a tactic and the include graphs of theories start having subtle effects on the way the tactics run. It's a mess. I've started running through the AFP, and it doesn't look too bad. I'll report on this again in the next few days. Cheers all, Thomas. On 04/06/14 23:23, Lawrence Paulson wrote: 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, and not immediately. Backward compatibility will be necessary for users, even if not for us. Larry On 4 Jun 2014, at 06:27, Thomas Sewell thomas.sew...@nicta.com.au wrote: I had hoped to have the change I was making to hypothesis-substitution ready for the coming release. I've got it working for all of HOL and the library, and begun looking at the AFP and at the l4.verified proofs. The HOL+library changes were easy enough, but the l4.verified changes are somewhat daunting and I haven't gotten anywhere with the AFP yet. I'll have another look at it, because I'd like this to go somewhere at some point. It might have to wait for a subsequent release though. Cheers, Thomas. On 30/05/14 21:30, Makarius wrote: The summer is getting close, and we need to start thinking about the coming release. I am myself on vacation during most of June. On return I would like to wrap up rather quickly, so that we can publish Isabelle2014-RC0 in the second week of July, for the Isabelle tutorial at VSL2014 Vienna. That will be still within the main Isabelle repository. The usual fork to the release repository and the regular sequence of Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014. I am myself attending the mega event at Vienna 13..19-Jul-2014. This will be also an opportunity to show me personally remaining snags, and to continue the elimination of remaining uses of Proof General. (It is getting harder and harder to construct counter-examples to the claim that this set is already empty.) Makarius ___ 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
