Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
Hi Johannes, I tried to reduce the runtime requirement of HOL-Probability by removing some of the sublocale instantiations. As a lot of time is spend in locale interpretation inside proofs. Is the same interpretation repeated over and over? In that case the corresponding proposition can be factored out into a lemma which is then reused over and over. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 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] NEWS: Isabelle/jEdit (19e1c6e922b6)
On Tue, 20 Sep 2011, Makarius wrote: In the meantime I have investigated this a little bit. It seems that HOL-Probability requires quite some memory even in minimalistic batch mode -- approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB for the editor process and the same (and more) for the fully persistent document state within ML. So it adds up to something 4 GB such that it becomes infeasible to edit the full session live on a small laptop with only 4 GB. I tried to reduce the runtime requirement of HOL-Probability by removing some of the sublocale instantiations. As a lot of time is spend in locale interpretation inside proofs. For example currently I had: locale A = ... locale B = A + ... (0) locale C = A + th sublocale C B I assume replacing (0) by: locale C = B + th lemma [Pure.intros!]: C - A /\ th should fasten up locale interpretation? But how is it in the following case: locale prodA = A M1 + A M2 (1) locale prodB = B M1 + B M2 sublocale prodB prodA locale prodC = C M1 + C M2 sublocale prodC prodB locale prodD = D M1 + D M2 sublocale prodD prodA Or should this be: (2) locale prodB = prodA + B M1 + B M2 locale prodC = prodB + C M1 + C M2 locale prodD = prodC + D M1 + D M2 as a user the difference should not be visible, and I thought (1) would be slower than (2) but after updating Probability it seams like (2) is slower than (1). - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On 18.09.2011 17:05, Makarius wrote: On Tue, 13 Sep 2011, Lars Noschinski wrote: I was irritated when Isabelle/jEdit complained about missing theory files, when the files where obviously there (and loaded). Later I found out, that this error is also displayed if there are any errors (transitively) in these theory files. Did you see the panel Prover Session / Theory Status? It provides some overview over the whole session. Yes, it's pretty useful. But at the I had above problem, it did not yet display the status in a way readable for the uninitiated ;) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On Tue, 13 Sep 2011, Lars Noschinski wrote: I was irritated when Isabelle/jEdit complained about missing theory files, when the files where obviously there (and loaded). Later I found out, that this error is also displayed if there are any errors (transitively) in these theory files. Did you see the panel Prover Session / Theory Status? It provides some overview over the whole session. In Isabelle/a04f3eb3943c it works more smoothly, although I need to defer even more refinements until after the release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On 06.09.2011 21:58, Makarius wrote: * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as isabelle jedit on the command line. . Management of multiple theory files directly from the editor buffer store -- bypassing the file-system (no requirement to save files for checking). Nice! Together with the improved scheduling, I was able to use Isabelle/jEdit for some serious work (tuning the simpset for Complete_Lattices). In the beginning I was irritated when Isabelle/jEdit complained about missing theory files, when the files where obviously there (and loaded). Later I found out, that this error is also displayed if there are any errors (transitively) in these theory files. . Markup of formal entities within the text buffer, with semantic highlighting, tooltips and hyperlinks to jump to defining source positions. . Refined scheduling of proof checking and printing of results, based on interactive editor view. (Note: jEdit folding and narrowing allows to restrict buffer perspectives explicitly.) When looking at simplifier traces, if found the output display not really smooth yet, sometimes I had to move the cursor a bit around, till the output view displayed what I expected; but I have not analyzed yet, what exactly goes wrong. . Reduced CPU performance requirements, usable on machines with few cores. . Reduced memory requirements due to pruning of unused document versions (garbage collection). As some data point: I was able to load HOL/Probability/Probability.thy (using HOL-Image), but needed my whole memory for this (6GiB). Pruning unused document versions sometimes interferes with the option to _not_ update the output window automatically: To compare the effect of different simpsets, I added a new output window and unchecked the auto update option. Then I changed the simp call and the not-updating output window went blank. See also ~~/src/Tools/jEdit/README.html for further information, including some remaining limitations. Some further comments: - The command line help shows some option -l to use a different logic image, but this does not seem to work. - Is Isabelle/jEdit supposed to work with Pure as a logic image? On one occasion, it misparsed a document because it did not consider datatype as a keyword. I can try to reproduce it, if you are interested. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On 09/13/2011 11:38 AM, Lars Noschinski wrote: - The command line help shows some option -l to use a different logic image, but this does not seem to work. -l works perfectly for us: for instance, /usr/local/isabelle/bin/isabelle jedit -l Isac Test_Isac.thy runs all tests on the behaviour of Isac used in Test_Isac.thy. Walther ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On 13.09.2011 12:01, Walther Neuper wrote: On 09/13/2011 11:38 AM, Lars Noschinski wrote: - The command line help shows some option -l to use a different logic image, but this does not seem to work. -l works perfectly for us: for instance, /usr/local/isabelle/bin/isabelle jedit -l Isac Test_Isac.thy Ah; the -l option only works if Default is chosen as logic image in the theory selector in Isabelle/jEdit. If a specific theory is selected, then the command line switch is overridden. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as isabelle jedit on the command line. . Management of multiple theory files directly from the editor buffer store -- bypassing the file-system (no requirement to save files for checking). . Markup of formal entities within the text buffer, with semantic highlighting, tooltips and hyperlinks to jump to defining source positions. . Refined scheduling of proof checking and printing of results, based on interactive editor view. (Note: jEdit folding and narrowing allows to restrict buffer perspectives explicitly.) . Reduced CPU performance requirements, usable on machines with few cores. . Reduced memory requirements due to pruning of unused document versions (garbage collection). See also ~~/src/Tools/jEdit/README.html for further information, including some remaining limitations. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On Tue, 6 Sep 2011, Makarius wrote: * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as isabelle jedit on the command line. The required build component is still the same: http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
