Re: [isabelle-dev] Slow builds due to excessive heap images
On 04/11/17 19:30, David Matthews wrote: > > I've had a look at this and pushed a change to IntInf.pow to Poly/ML > master (c2a2961). It now uses Word.andb rather than IntInf.andb which > avoids a call into the run-time system (RTS). > > However, this code hadn't changed since 5.6 and when I tested it using > List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly > not the massive differences you found with Par_List.map. The only thing > I can think of is that there were so many calls into the RTS that there > was some contention on a mutex and that was causing problems. > > Anyway, try the new version and let me know the results. I have briefly tested the subsequent version Poly/ML 31b5de8ee56 and it works well with Isabelle/978c584609de + ch-pow and AFP/9ad8f3af760f: ML_PLATFORM="x86_64-linux" ML_HOME="/home/wenzelm/lib/polyml/x86_64-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--minheap 4G --maxheap 32G" lxcisa0> isabelle build -d '$AFP' -o threads=8 Lorenz_C0 Building Pure ... Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95) Building HOL ... Finished HOL (0:03:21 elapsed time, 0:11:15 cpu time, factor 3.35) Building HOL-Analysis ... Finished HOL-Analysis (0:05:09 elapsed time, 0:27:51 cpu time, factor 5.40) Building Ordinary_Differential_Equations ... Finished Ordinary_Differential_Equations (0:01:55 elapsed time, 0:08:18 cpu time, factor 4.33) Building HOL-ODE ... Finished HOL-ODE (0:00:01 elapsed time) Building HOL-ODE-Refinement ... Finished HOL-ODE-Refinement (0:03:17 elapsed time, 0:20:01 cpu time, factor 6.10) Building HOL-ODE-Numerics ... Finished HOL-ODE-Numerics (0:18:23 elapsed time, 0:43:51 cpu time, factor 2.39) Building Lorenz_Approximation ... Finished Lorenz_Approximation (0:03:51 elapsed time, 0:08:15 cpu time, factor 2.14) Running Lorenz_C0 ... Finished Lorenz_C0 (0:13:14 elapsed time, 1:39:57 cpu time, factor 7.55) 0:49:55 elapsed time, 3:39:48 cpu time, factor 4.40 Here are also the earlier results with the workaround (Isabelle/17eb23e43630): On 03/11/17 20:07, Makarius wrote: > $ isabelle build -d '$AFP' -o threads=8 Lorenz_C0 > Building Pure ... > Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 0.95) > Building HOL ... > Finished HOL (0:03:19 elapsed time, 0:10:54 cpu time, factor 3.28) > Building HOL-Analysis ... > Finished HOL-Analysis (0:05:16 elapsed time, 0:28:08 cpu time, factor 5.33) > Building Ordinary_Differential_Equations ... > Finished Ordinary_Differential_Equations (0:01:59 elapsed time, 0:08:10 > cpu time, factor 4.10) > Building HOL-ODE ... > Finished HOL-ODE (0:00:01 elapsed time) > Building HOL-ODE-Refinement ... > Finished HOL-ODE-Refinement (0:03:29 elapsed time, 0:20:08 cpu time, > factor 5.76) > Building HOL-ODE-Numerics ... > Finished HOL-ODE-Numerics (0:18:06 elapsed time, 0:41:23 cpu time, > factor 2.28) > Building Lorenz_Approximation ... > Finished Lorenz_Approximation (0:03:43 elapsed time, 0:07:53 cpu time, > factor 2.12) > Running Lorenz_C0 ... > Finished Lorenz_C0 (0:14:21 elapsed time, 1:49:04 cpu time, factor 7.60) > 0:51:01 elapsed time, 3:45:59 cpu time, factor 4.43 So the uniform use of IntInf.pow might come out slightly faster. I will make a proper polyml-test component soon and then apply ch-pow permanently, but it needs a few more days: there is still NewTestRegisterSave (Isabelle/c70c47dcf63e) in the queue for official testing and timing -- my impression is that it will be only a few percent faster. Makarius # HG changeset patch # User wenzelm # Date 1509824436 -3600 # Sat Nov 04 20:40:36 2017 +0100 # Node ID 415a6bba9344b53576477a6e03d6ea5f6219ad1d # Parent 978c584609ded0d1a36246b83aeb8630d14034f9 test diff -r 978c584609de -r 415a6bba9344 src/Pure/General/integer.ML --- a/src/Pure/General/integer.ML Sat Nov 04 19:44:28 2017 +0100 +++ b/src/Pure/General/integer.ML Sat Nov 04 20:40:36 2017 +0100 @@ -40,20 +40,7 @@ fun square x = x * x; -fun pow k l = - let -fun pw 0 _ = 1 - | pw 1 l = l - | pw k l = - let -val (k', r) = div_mod k 2; -val l' = pw k' (l * l); - in if r = 0 then l' else l' * l end; - in -if k < 0 -then IntInf.pow (l, k) -else pw k l - end; +fun pow k l = IntInf.pow (l, k); fun gcd x y = PolyML.IntInf.gcd (x, y); fun lcm x y = abs (PolyML.IntInf.lcm (x, y)); @@ -65,10 +52,3 @@ | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs)); end; - -(* FIXME workaround for Poly/ML 5.7.1 testing *) -structure IntInf = -struct - open IntInf; - fun pow (i, n) = Integer.pow n i; -end ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Slow builds due to excessive heap images
On 03/11/2017 19:07, Makarius wrote: On 03/11/17 19:26, Fabian Immler wrote: I looked at it once more: profiling told me that IntInf.pow (in combination with Par_List.map) seems to be the culprit. The following snippet shows similar behavior: ML ‹ fun powers [] = [] | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs; Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31) › polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02 polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, factor 5.70 polyml-5.6-1/x86_64-darwin: 0.570s elapsed time, 1.748s cpu time, 0.000s GC time polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu time, 42.602s GC time I have discovered the same and have now pushed a workaround: http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630 Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit wasteful, maybe during the bit vector operation instead of our IntInf.divMod (_, 2) used here: see http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43 I've had a look at this and pushed a change to IntInf.pow to Poly/ML master (c2a2961). It now uses Word.andb rather than IntInf.andb which avoids a call into the run-time system (RTS). However, this code hadn't changed since 5.6 and when I tested it using List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly not the massive differences you found with Par_List.map. The only thing I can think of is that there were so many calls into the RTS that there was some contention on a mutex and that was causing problems. Anyway, try the new version and let me know the results. David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more options for "isabelle jedit"
Dear Makarius, > *** Prover IDE -- Isabelle/Scala/jEdit *** > > * The command-line tool "isabelle jedit" provides more flexible options > for session selection: > - options -P opens the parent session image of -l > - options -A and -B modify the meaning of -l to produce a base > image on the spot, based on the specified ancestor (or parent) > - option -F focuses on the specified logic session > - option -R has changed: it only opens the session ROOT entry > - option -S sets up the development environment to edit the > specified session: it abbreviates -B -F -R -l > > Examples: > isabelle jedit -d '$AFP' -S Formal_SSA -A HOL > isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis this is really great and makes my life significantly easier! There remains one gap which I am wondering how to fill it. Lets start with isabelle jedit -d '$AFP' -S … This provides a suitable base image and opens the ROOT file. What is the canonical way to proceed from there to check the whole session? Of course the ROOT file lists the respective theories and you can open them manually in jedit, but this is tiresome if the ROOT file spans many theories. Would clicakble theorie files in ROOT files be an option? Cheers, Florian -- PGP available: http://isabelle.in.tum.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] Future of Nat_Transfer
See now http://isabelle.in.tum.de/repos/isabelle/rev/0230af0f3c59. Florian Am 19.10.2017 um 13:56 schrieb Florian Haftmann: > Dear all, > > the nowadays ancient theory Nat_Transfer (essentially providing an > attribute to transfer ad-hoc between theorems on nat vs. int) is almost > obsolete: > > * »almost« since I haven't figured out how relevant it is still for > HOL-Number_Theory > > * Conversion between nat and int is rarely needed since most common > lemmas are provided by type classes anyway nowadays. > > See also > http://isabelle.in.tum.de/repos/isabelle/file/ee874941dfb8/src/HOL/Nat_Transfer.thy > for the current state of affairs. > > My suggestion would be to remove it completely. > > Any opinions on that? > > Cheers, > Florian > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.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
