Re: [isabelle-dev] Towards the Isabelle2014 release
On 05.06.2014 05:44, Thomas Sewell wrote: 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. A little less invasive would be enabling the compatibility mode for a whole theory using context notes [[...]] begin ... end. signature.asc Description: OpenPGP digital signature ___ 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
I certainly agree with your point of view, but I would immediately insert the local context around any proof that causes problems rather than waste time trying to fix it. Maybe we could then invite the maintainers of the entries to update their proofs if they wish. Larry On 5 Jun 2014, at 04:44, Thomas Sewell thomas.sew...@nicta.com.au wrote: 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
While fixing theories in the AFP, I arrived in a strange situation where isabelle build -D thys would no longer find and check the remaining unbuilt theories. Instead, I got a java OutOfMemory exception on the java heap. This is before anything starts building - I take it java has run out of heap just trying to parse all the theories, logs and heaps and figure out what work to do. Unfortunately I can't exactly reproduce this, since I've since got a theory to build and changed the outcome. Instead isabelle seems to get stuck - after 10 minutes at ~6 cores java still hasn't picked and started any sessions. In case anyone else gets stuck in this situation, here is my best workaround: cat thys/*/ROOT | grep session | cut -d' ' -f2 | xargs -n 10 isabelle build -d thys By focusing on (the dependencies of) 10 sessions at a time, isabelle seems to get the job done. The grepping and cutting is a bit ugly. Would it make sense to have an equivalent of 'findlogics' which found sessions? That would allow isabelle findsessions -d (DIR) | xargs -n 10 isabelle build -d (DIR) If noone else has seen this kind of thing, just ignore me. Cheers, Thomas. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
