Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 20:35, Christian Sternagel wrote: > > While what you say is true and in addition such "build sessions" (we > have for example "IsaFoR_1", ..., "IsaFoR_4" in the IsaFoR project) can > be tedious to maintain I find them necessary from time to time. > > For example in IsaFoR I (depending on the machine I am working on) and > some students are in a situation where thy-files that are very close to > the final code generation session are really hard to work with in > Isabelle/jEdit since RAM is close to or already swapping and every > single edit takes quite some time before taking effect. In such > situations (especially when you have to restart Isabelle/jEdit) I find > it convenient to have a heap image that contains everything up to the > single file I am currently working on. > > Maybe there is a better way to achieve the same goal without creating > superfluous ad-hoc sessions? One could try to make this systematic via Isabelle/Scala, similar to option "isabelle jedit -R" -- but it requires to look very closely what is really required. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 20:32, Makarius wrote: > > Whenever I pass by this JNF-AFP-Lib session, I wonder if there is any > remaining use of it. It quotes a lot of theories without a check if they > are actually needed. Loading the material takes only 30s in my 8core > machine. Here are some concrete measurements on my 8 core machine with very fast memory + SSD: ML_PLATFORM="x86_64_32-linux" ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8/x86_64_32-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="--minheap 1500" $ isabelle build -d '$AFP' Jordan_Normal_Form Polynomial_Factorization Jordan_Normal_Form Polynomial_Factorization Building JNF-AFP-Lib ... Finished JNF-AFP-Lib (0:00:57 elapsed time, 0:03:46 cpu time, factor 3.92) Running Polynomial_Factorization ... Finished Polynomial_Factorization (0:00:26 elapsed time, 0:01:30 cpu time, factor 3.44) Running Jordan_Normal_Form ... Finished Jordan_Normal_Form (0:02:43 elapsed time, 0:09:19 cpu time, factor 3.42) 0:04:15 elapsed time, 0:14:36 cpu time, factor 3.42 $ isabelle build -d '$AFP' Jordan_Normal_Form Polynomial_Factorization Running Jordan_Normal_Form ... Finished Jordan_Normal_Form (0:02:58 elapsed time, 0:11:54 cpu time, factor 4.01) Running Polynomial_Factorization ... Finished Polynomial_Factorization (0:00:39 elapsed time, 0:02:32 cpu time, factor 3.86) 0:03:45 elapsed time, 0:14:26 cpu time, factor 3.85 The canonical changeset to "build faster without intermediate sessions" is included (not pushed yet). Makarius # HG changeset patch # User wenzelm # Date 1568314131 -7200 # Thu Sep 12 20:48:51 2019 +0200 # Node ID 229812cc587410c279aece30432a26bd52fec64a # Parent 98320942654aaf57ea6e91c1863b1ce192bc59cd build faster without intermediate sessions; diff -r 98320942654a -r 229812cc5874 thys/Jordan_Normal_Form/ROOT --- a/thys/Jordan_Normal_Form/ROOT Wed Sep 11 21:50:31 2019 +0200 +++ b/thys/Jordan_Normal_Form/ROOT Thu Sep 12 20:48:51 2019 +0200 @@ -1,9 +1,16 @@ chapter AFP -session "Jordan_Normal_Form" (AFP) = "JNF-AFP-Lib" + +session "Jordan_Normal_Form" (AFP) = "HOL-Algebra" + options [timeout = 1200] sessions +"Abstract-Rewriting" +"HOL-Cardinals" +Containers +Gauss_Jordan Matrix Polynomial_Factorization +Polynomial_Interpolation +Show +VectorSpace theories Missing_Ring Missing_Permutations diff -r 98320942654a -r 229812cc5874 thys/Polynomial_Factorization/ROOT --- a/thys/Polynomial_Factorization/ROOTWed Sep 11 21:50:31 2019 +0200 +++ b/thys/Polynomial_Factorization/ROOTThu Sep 12 20:48:51 2019 +0200 @@ -1,63 +1,18 @@ chapter AFP -session "JNF-AFP-Lib" (AFP) in "Lib" = "HOL-Algebra" + - description "Theories from HOL-Library and the Archive of Formal Proofs that are used by this entry" - options [timeout = 600] - sessions -Containers -"Abstract-Rewriting" -Gauss_Jordan Matrix -Polynomial_Interpolation -Show -VectorSpace -"HOL-Cardinals" - theories -Containers.Set_Impl -Matrix.Utility -Matrix.Ordered_Semiring -"Abstract-Rewriting.SN_Order_Carrier" -"Abstract-Rewriting.Relative_Rewriting" -Show.Show_Instances -VectorSpace.VectorSpace -Polynomial_Interpolation.Missing_Polynomial -Polynomial_Interpolation.Ring_Hom_Poly -"HOL-Library.AList" -"HOL-Library.Cardinality" -"HOL-Library.Char_ord" -"HOL-Library.Code_Binary_Nat" -"HOL-Library.Code_Target_Numeral" -"HOL-Library.DAList" -"HOL-Library.DAList_Multiset" -"HOL-Library.Infinite_Set" -"HOL-Library.Lattice_Syntax" -"HOL-Library.Mapping" -"HOL-Library.Monad_Syntax" -"HOL-Library.More_List" -"HOL-Library.Multiset" -"HOL-Library.Permutation" -"HOL-Library.Permutations" -"HOL-Library.IArray" -"HOL-Library.Phantom_Type" -"HOL-Library.Ramsey" -"HOL-Library.RBT_Impl" -"HOL-Library.Simps_Case_Conv" -"HOL-Library.While_Combinator" -"HOL-Computational_Algebra.Fundamental_Theorem_Algebra" -"HOL-Computational_Algebra.Fraction_Field" -"HOL-Computational_Algebra.Polynomial" -"HOL-Computational_Algebra.Primes" -"HOL-Cardinals.Order_Union" -"HOL-Cardinals.Wellorder_Extension" - - -session Polynomial_Factorization (AFP) = "JNF-AFP-Lib" + +session Polynomial_Factorization (AFP) = "HOL-Algebra" + description "Algebraic Numbers" options [timeout = 600] sessions +"Abstract-Rewriting" +"HOL-Cardinals" +Containers +Gauss_Jordan Matrix Partial_Function_MR Polynomial_Interpolation Show Sqrt_Babylonian +VectorSpace theories Missing_Multiset Missing_List ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 9/12/19 4:33 PM, Makarius wrote: > On 12/09/2019 16:04, Christian Sternagel wrote: >> >> On 9/12/19 3:04 PM, Makarius wrote: >>> *** General *** >>> >>> * Session ROOT files need to specify explicit 'directories' for import >>> of theory files. Directories cannot be shared by different sessions. >>> (Recall that import of theories from other sessions works via >>> session-qualified theory names, together with suitable 'sessions' >>> declarations in the ROOT.) >>> >> >> (at least for document preparation) I often use a single ROOT file along >> the following lines >> >> session S_base = HOL + ... >> session S = S_base + ... >> >> where S_base typically collects a lot of stuff (from the AFP say) into a >> single heap image to make processing faster for my actual work that is >> done in S. >> >> I wonder what a suitable replacement for the above setup would be, now >> that directories cannot be shared by different sessions anymore? > > You merely need to invent a dummy directory that no other session is > using. The theory imports refer to "collected" theories from other > sessions via session-qualified names, so that directory is irrelavant. Thanks. In hindsight that was obvious and quite easy too. You made the start-up time great again. > > If you do have additional local theories for the "base" session, you put > them into this separate session directory. > > I have already cleaned up AFP in this respect: unexpectedly it was > rather easy. > > >> While logically such "collecting sessions" might be irrelevant, they are >> very convenient in terms of saving build time. > > Even worse, they often waste more time than they save. While what you say is true and in addition such "build sessions" (we have for example "IsaFoR_1", ..., "IsaFoR_4" in the IsaFoR project) can be tedious to maintain I find them necessary from time to time. For example in IsaFoR I (depending on the machine I am working on) and some students are in a situation where thy-files that are very close to the final code generation session are really hard to work with in Isabelle/jEdit since RAM is close to or already swapping and every single edit takes quite some time before taking effect. In such situations (especially when you have to restart Isabelle/jEdit) I find it convenient to have a heap image that contains everything up to the single file I am currently working on. Maybe there is a better way to achieve the same goal without creating superfluous ad-hoc sessions? cheers chris > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 16:04, Christian Sternagel wrote: > > On 9/12/19 3:04 PM, Makarius wrote: >> *** General *** >> >> * Session ROOT files need to specify explicit 'directories' for import >> of theory files. Directories cannot be shared by different sessions. >> (Recall that import of theories from other sessions works via >> session-qualified theory names, together with suitable 'sessions' >> declarations in the ROOT.) >> > > I often use a single ROOT file along > the following lines > > session S_base = HOL + ... > session S = S_base + ... > > where S_base typically collects a lot of stuff (from the AFP say) into a > single heap image to make processing faster for my actual work that is > done in S. > > I wonder what a suitable replacement for the above setup would be, now > that directories cannot be shared by different sessions anymore? Has everything become clear already? There might be a remaining confusion about the meaning of "session directory": it is a place where .thy files may reside in order to be incorporated into the session-qualified theory name space. Each directory stands for itself, without inclusion of subdirectories. Here is also a concrete example from AFP: https://isabelle.sketis.net/repos/afp-devel/file/98320942654a/thys/Polynomial_Factorization/ROOT It uses the subdirectory "Lib" for the auxiliary session, but that does not contribute any theories on its own. Whenever I pass by this JNF-AFP-Lib session, I wonder if there is any remaining use of it. It quotes a lot of theories without a check if they are actually needed. Loading the material takes only 30s in my 8core machine. For interactive development there is "isabelle jedit -R" (option "-S" with its session focus restriction is obsolete). Is that sufficient, or is something else required? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 15:04, Makarius wrote: > *** General *** > > * Session ROOT files need to specify explicit 'directories' for import > of theory files. Directories cannot be shared by different sessions. > (Recall that import of theories from other sessions works via > session-qualified theory names, together with suitable 'sessions' > declarations in the ROOT.) An important consequence is that a theory file gets a unique session-qualified name, without accidental multiplication of theories that is occasionally seen in applications. Thus by forcing users to clean up their session/theory arrangement, some applications might become faster without further ado. (In the past 2 years, I've cleaned up such situations several times in AFP, and it is all fine in AFP/98320942654a). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 16:59, Tobias Nipkow wrote: > >>> While logically such "collecting sessions" might be irrelevant, they are >>> very convenient in terms of saving build time. >> >> Even worse, they often waste more time than they save. > > For paper writing (which Christian referred to) they are indispensible. > It would kill you if you had to load all the theories once more when you > modify the paper based on them. I was talking implicitly about AFP: people sometimes publish "private" session setups there that cause lots of problems. This unclear situation in AFP was the main reason why we had to suffered 2 years with increasingly slow PIDE startup times. I am glad that it has turned out so well in current AFP/98320942654a. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 16:33, Makarius wrote: On 12/09/2019 16:04, Christian Sternagel wrote: On 9/12/19 3:04 PM, Makarius wrote: *** General *** * Session ROOT files need to specify explicit 'directories' for import of theory files. Directories cannot be shared by different sessions. (Recall that import of theories from other sessions works via session-qualified theory names, together with suitable 'sessions' declarations in the ROOT.) (at least for document preparation) I often use a single ROOT file along the following lines session S_base = HOL + ... session S = S_base + ... where S_base typically collects a lot of stuff (from the AFP say) into a single heap image to make processing faster for my actual work that is done in S. I wonder what a suitable replacement for the above setup would be, now that directories cannot be shared by different sessions anymore? You merely need to invent a dummy directory that no other session is using. The theory imports refer to "collected" theories from other sessions via session-qualified names, so that directory is irrelavant. If you do have additional local theories for the "base" session, you put them into this separate session directory. I have already cleaned up AFP in this respect: unexpectedly it was rather easy. While logically such "collecting sessions" might be irrelevant, they are very convenient in terms of saving build time. Even worse, they often waste more time than they save. For paper writing (which Christian referred to) they are indispensible. It would kill you if you had to load all the theories once more when you modify the paper based on them. Tobias Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
On 12/09/2019 16:04, Christian Sternagel wrote: > > On 9/12/19 3:04 PM, Makarius wrote: >> *** General *** >> >> * Session ROOT files need to specify explicit 'directories' for import >> of theory files. Directories cannot be shared by different sessions. >> (Recall that import of theories from other sessions works via >> session-qualified theory names, together with suitable 'sessions' >> declarations in the ROOT.) >> > > (at least for document preparation) I often use a single ROOT file along > the following lines > > session S_base = HOL + ... > session S = S_base + ... > > where S_base typically collects a lot of stuff (from the AFP say) into a > single heap image to make processing faster for my actual work that is > done in S. > > I wonder what a suitable replacement for the above setup would be, now > that directories cannot be shared by different sessions anymore? You merely need to invent a dummy directory that no other session is using. The theory imports refer to "collected" theories from other sessions via session-qualified names, so that directory is irrelavant. If you do have additional local theories for the "base" session, you put them into this separate session directory. I have already cleaned up AFP in this respect: unexpectedly it was rather easy. > While logically such "collecting sessions" might be irrelevant, they are > very convenient in terms of saving build time. Even worse, they often waste more time than they save. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: proper session directories and faster PIDE startup
Dear Makarius, On 9/12/19 3:04 PM, Makarius wrote: > *** General *** > > * Session ROOT files need to specify explicit 'directories' for import > of theory files. Directories cannot be shared by different sessions. > (Recall that import of theories from other sessions works via > session-qualified theory names, together with suitable 'sessions' > declarations in the ROOT.) > (at least for document preparation) I often use a single ROOT file along the following lines session S_base = HOL + ... session S = S_base + ... where S_base typically collects a lot of stuff (from the AFP say) into a single heap image to make processing faster for my actual work that is done in S. I wonder what a suitable replacement for the above setup would be, now that directories cannot be shared by different sessions anymore? While logically such "collecting sessions" might be irrelevant, they are very convenient in terms of saving build time. But maybe there is a better way to achieve the same goal? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
