Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)
Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec (active by default). It performs slightly better than the previous test version -- I have also removed old workarounds for integer arithmetic in Isabelle/4591221824f6. It is important to check that obsolete entries in $ISASELLE_HOME_USER/etc/settings are cleaned up, such that this greatest and latest version gets used. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 23/01/2019 21:08, Makarius wrote: On 23/01/2019 12:05, David Matthews wrote: I've had a look at this under Windows and the problem seems to be with calls to IntInf.divMod from generated code, not from IntInf.pow. The underlying RTS call used by IntInf.quotRem has changed in the 32-in-64 version. It previously returned the pair of values by passing in a stack location and having the RTS update this. That isn't possible in the 32-in-64 version so now it allocates a pair on the heap. For simplicity this is now used for the native code versions as well. From what I can tell nearly all the threads are waiting for mutexes and I suspect that the extra heap allocation in IntInf.quotRem is causing some of the problem. Waiting for a contended mutex can cost a significant amount of processor time both in busy-waiting and in kernel calls. I'm not sure what to suggest except not to use concurrency here. There doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem. In the meantime David has produced Poly/ML a444f281ccec and I can confirm that it works very well: I had another look and it was a mutex contention problem, just not exactly where I'd thought. Most calls to the run-time system involved taking a lock for a very short period in order to get the thread's C++ data structure. This wasn't a problem in the vast majority of cases but this example involves very many calls to the long-format arbitrary precision package. That resulted in contention on the lock. I've changed this so the lock is no longer needed and it seems to have solved the problem. David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 23/01/2019 12:05, David Matthews wrote: > > I've had a look at this under Windows and the problem seems to be with > calls to IntInf.divMod from generated code, not from IntInf.pow. The > underlying RTS call used by IntInf.quotRem has changed in the 32-in-64 > version. It previously returned the pair of values by passing in a > stack location and having the RTS update this. That isn't possible in > the 32-in-64 version so now it allocates a pair on the heap. For > simplicity this is now used for the native code versions as well. From > what I can tell nearly all the threads are waiting for mutexes and I > suspect that the extra heap allocation in IntInf.quotRem is causing some > of the problem. Waiting for a contended mutex can cost a significant > amount of processor time both in busy-waiting and in kernel calls. > > I'm not sure what to suggest except not to use concurrency here. There > doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem. In the meantime David has produced Poly/ML a444f281ccec and I can confirm that it works very well: Isabelle/2444c8b85aac AFP/2eacf2ed7d5d x86_64_32-linux --minheap 1500 threads=8 Finished HOL-ODE-Numerics (0:17:18 elapsed time, 0:45:28 cpu time, factor 2.63) Finished Lorenz_C0 (0:12:06 elapsed time, 1:29:19 cpu time, factor 7.37) x86_64-linux --minheap 1500 threads=8 Finished HOL-ODE-Numerics (0:19:19 elapsed time, 0:49:46 cpu time, factor 2.58) Finished Lorenz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 23/01/2019 14:14, Bertram Felgenhauer wrote: > Makarius wrote: >> On 22/01/2019 12:31, Bertram Felgenhauer wrote: >>> Makarius wrote: So this is the right time for further testing of applications: Isabelle2018 should work as well, but I have not done any testing beyond "isabelle build -g main" -- Isabelle development only moves forward in one direction on a single branch. >>> >>> I have tried this with Isabelle2018 and IsaFoR; I've encountered no >>> problems and there's a nice speedup (estimated 1.25 times faster). >>> Heap images are 40% smaller, which is a welcome change as well. >> >> Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)? > > This is compared to x86_64. Sorry, I should have mentioned this, > but to my mind it was implied because IsaFoR is notorious for running > out of memory with the x86 version of PolyML. OK, this is the kind of applications that x86_64_32 has been made for: less memory requirements (< 16 GB) and much faster within it. >> I am asking this, because I have noted a speedup of building heap >> images: x86_64_32 compared to x86, and was wondering about the reasons >> for it. (For x86_64 everything is just more bulky, of course, including >> heaps.) > > As far as I can see, one difference between x86 and x86_64_32 is that > PolyML keeps heap objects aligned to 8 byte boundaries for the latter. > This may impact performance. I misinterpreted my earlier measurements: the test version is actually a bit slower in dumping heap images, but x86 is worse than x86_64_32 in this respect. Something to be investigated further ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Spam] cardinality primitives in Isabelle/HOL?
This makes perfect sense to me. I suggest moving at least the definition of Fpow into Main (it’s small, and fundamental) while creating a new Library entry for my own new material. Larry > On 23 Jan 2019, at 12:48, Blanchette, J.C. wrote: > > Hi Larry, > > You wrote: > >> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so >> clearly a lot of facts about cardinals are available already in Main. > > FYI: As you might already know or deduced from the name convention, the > (co)datatype (a.k.a. "BNF") package is based on some cardinality material. > When we moved the BNF package into Main, I surgically split the HOL-Cardinals > theories into two, moving the exact dependencies into Main and leaving the > rest outside. As a result, it's pretty random what's in Main and what's > outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed > undesirable because it would slow down building Main quite a bit. > > Jasmin > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
Makarius wrote: > On 22/01/2019 12:31, Bertram Felgenhauer wrote: > > Makarius wrote: > >> So this is the right time for further testing of applications: > >> Isabelle2018 should work as well, but I have not done any testing beyond > >> "isabelle build -g main" -- Isabelle development only moves forward in > >> one direction on a single branch. > > > > I have tried this with Isabelle2018 and IsaFoR; I've encountered no > > problems and there's a nice speedup (estimated 1.25 times faster). > > Heap images are 40% smaller, which is a welcome change as well. > > Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)? This is compared to x86_64. Sorry, I should have mentioned this, but to my mind it was implied because IsaFoR is notorious for running out of memory with the x86 version of PolyML. > I am asking this, because I have noted a speedup of building heap > images: x86_64_32 compared to x86, and was wondering about the reasons > for it. (For x86_64 everything is just more bulky, of course, including > heaps.) As far as I can see, one difference between x86 and x86_64_32 is that PolyML keeps heap objects aligned to 8 byte boundaries for the latter. This may impact performance. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Spam] cardinality primitives in Isabelle/HOL?
Hi Larry, You wrote: > The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so > clearly a lot of facts about cardinals are available already in Main. FYI: As you might already know or deduced from the name convention, the (co)datatype (a.k.a. "BNF") package is based on some cardinality material. When we moved the BNF package into Main, I surgically split the HOL-Cardinals theories into two, moving the exact dependencies into Main and leaving the rest outside. As a result, it's pretty random what's in Main and what's outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed undesirable because it would slow down building Main quite a bit. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
The question of dependency is tricky. I tried deleting the reference to
HOL-Cardinals.Cardinals and found that most of the elementary results were
easily provable using other library facts. But then there was this:
lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans
ordIso_iff_ordLeq)
The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so
clearly a lot of facts about cardinals are available already in Main.
But I do prove a couple of things involving the operator Fpow:
lemma lepoll_restricted_funspace:
"{f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A ∧ finite {x. f x ≠ k x}} ≲ Fpow (A × B)"
proof -
have *: "∃U ∈ Fpow (A × B). f = (λx. if ∃y. (x, y) ∈ U then SOME y. (x,y) ∈ U
else k x)"
if "f ` A ⊆ B" "{x. f x ≠ k x} ⊆ A" "finite {x. f x ≠ k x}" for f
apply (rule_tac x="(λx. (x, f x)) ` {x. f x ≠ k x}" in bexI)
using that by (auto simp: image_def Fpow_def)
show ?thesis
apply (rule subset_image_lepoll [where f = "λU x. if ∃y. (x,y) ∈ U then @y.
(x,y) ∈ U else k x"])
using * by (auto simp: image_def)
qed
lemma eqpoll_Fpow:
assumes "infinite A" shows "Fpow A ≈ A”
The thing is though, Fpow (which is nothing but the finite powerset operator)
probably belongs in Main as well.
An alternative proposal is to create a new theory, Library/Equipollence. I
agree about hiding the syntax.
Larry
> On 23 Jan 2019, at 10:11, Traytel Dmitriy wrote:
>
> Hi Larry,
>
> if you want to put the definitions and the basic properties in Main, then
> Fun.thy would probably be the place. But then I would argue that the syntax
> should be hidden, as users might want to use these symbols for something else.
>
> For the advanced material, do you need some theorems from HOL-Cardinals or
> just the syntax from HOL-Library.Cardinal_Notations in addition to what is
> already there in Main about cardinals? If it is only the syntax, then a
> separate theory in HOL-Library is probably a good fit. Otherwise, a separate
> theory in HOL-Cardinals would make sense.
>
> Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 22/01/2019 23:01, Makarius wrote: On 22/01/2019 23:08, Fabian Immler wrote: On 1/22/2019 4:00 PM, Fabian Immler wrote: On 1/22/2019 2:28 PM, Makarius wrote: On 22/01/2019 20:05, Fabian Immler wrote: These numbers look quite extreme: The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as it seems to be the case with polyml-test-0a6ebca445fc). The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0: ML_PLATFORM="x86-linux" ML_OPTIONS="--minheap 2000 --maxheap 4000" Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time, factor 2.66) Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time, factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take some time...) HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that this was the case with your computations, too. Unlike Lorenz_C0: x86_64_32-linux -minheap 1500 Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44) x86_64-linux --minheap 3000 Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52) Lorenz_C0 had the most significant slowdown, it has the biggest number of parallel computations, so I thought this might be related. And indeed, if you try the theory at the end: Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32 whereas the sequential evaluation is only 2 times slower. All of this reminds me of the discussion we had in November 2017: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643 Back in Nov-2017, I made the following workaround that is still active: http://isabelle.in.tum.de/repos/isabelle/rev/5da20135f560 Looking at the profiles of the included Float_Test.thy I now see a lot of IntInf.divMod, but it is qualitatively similar to former IntInf.pow. Maybe David can revisit both of these operations, so that we can get rid of the workarounds. I've had a look at this under Windows and the problem seems to be with calls to IntInf.divMod from generated code, not from IntInf.pow. The underlying RTS call used by IntInf.quotRem has changed in the 32-in-64 version. It previously returned the pair of values by passing in a stack location and having the RTS update this. That isn't possible in the 32-in-64 version so now it allocates a pair on the heap. For simplicity this is now used for the native code versions as well. From what I can tell nearly all the threads are waiting for mutexes and I suspect that the extra heap allocation in IntInf.quotRem is causing some of the problem. Waiting for a contended mutex can cost a significant amount of processor time both in busy-waiting and in kernel calls. I'm not sure what to suggest except not to use concurrency here. There doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem. By the way I updated IntInf.pow with https://github.com/polyml/polyml/commit/c2a296122426f5a6205cf121218e3f38415d2b06 David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Hi Larry, if you want to put the definitions and the basic properties in Main, then Fun.thy would probably be the place. But then I would argue that the syntax should be hidden, as users might want to use these symbols for something else. For the advanced material, do you need some theorems from HOL-Cardinals or just the syntax from HOL-Library.Cardinal_Notations in addition to what is already there in Main about cardinals? If it is only the syntax, then a separate theory in HOL-Library is probably a good fit. Otherwise, a separate theory in HOL-Cardinals would make sense. Dmitriy > On 22 Jan 2019, at 15:58, Lawrence Paulson wrote: > > I’m trying to install some of my new material and I’m wondering what to do > with equipollence and related concepts: > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) > where "eqpoll A B ≡ ∃f. bij_betw f A B" > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) > where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) > where "A ≺ B == A ≲ B ∧ ~(A ≈ B)" > > The raw definitions are extremely simple and could even be installed in the > main Isabelle/HOL distribution. The basic properties of these concepts > require few requisites. However, more advanced material requires the > Cardinals development. > > Where do people think these definitions and proofs should be installed? > > Larry > >> On 27 Dec 2018, at 20:29, Makarius wrote: >> >> On 27/12/2018 17:45, Traytel Dmitriy wrote: >>> Hi Larry, >>> >>> the HOL-Cardinals library might be just right for the purpose: >>> >>> theory Scratch >>> imports "HOL-Cardinals.Cardinals" >>> begin >>> >>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" >>> by (rule card_of_ordLeq[symmetric]) >>> >>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" >>> by (rule card_of_ordIso[symmetric]) >>> >>> lemma >>> assumes "|A| ≤o |B|" "|B| ≤o |A|" >>> shows "|A| =o |B|" >>> by (simp only: assms ordIso_iff_ordLeq) >>> >>> end >>> >>> The canonical entry point for the library is the above >>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already >>> in Main, because the (co)datatype package is based on them. The syntax is >>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations >>> (which HOL-Cardinals.Cardinals does transitively). >> >> It would be great to see this all consolidated and somehow unified, i.e. >> some standard notation in Main as proposed by Larry (potentially as >> bundles as proposed by Florian), and avoidance of too much no_syntax >> remove non-standard notation from Main. >> >> >> Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith
> But ocamlfind semms not to provide a subcommand to invoke the > interactive OCaml toplevel. What am I missing? The other way round. "ocamlfind" hooks into the toplevel. $ isabelle ocaml_opam config exec ocaml OCaml version 4.05.0 # #use "topfind";; - : unit = () Findlib has been successfully loaded. Additional directives: #require "package";; to load a package #list;; to list the available packages #camlp4o;;to load camlp4 (standard syntax) #camlp4r;;to load camlp4 (revised syntax) #predicates "p,q,...";; to set these predicates Topfind.reset();; to force that packages will be reloaded #thread;; to enable threads - : unit = () # #require "zarith";; /home/lars/.isabelle/opam/4.05.0/lib/zarith: added to search path /home/lars/.isabelle/opam/4.05.0/lib/zarith/zarith.cma: loaded # Z.one;; - : Z.t = Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
