Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
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.
Note that I have produced the profiles as follows:
isabelle build -o profiling=time ...
with a suitable test session that includes the above test theory, e.g.
see the included ROOT.
Then with "isabelle profiling_report" on the resulting log files, e.g.
isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Float_Test.gz
Makarius
theory Float_Test
imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin
definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down
p 1 (-x)))"
primrec iter where
"iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"
definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1))
(nat_of_integer i)"
ML \val logistic_chaos = @{code logistic_chaos}\
ML \Par_List.map logistic_chaos (replicate 10 10)\
\ \x86_64_32: 24s
x86_64: 2s\
(*
ML \map logistic_chaos (replicate 10 10)\
\ \x86_64_32: 16s
x86_64: 8s\
*)
endsession Float_Test = "HOL-Library" +
theories
Float_Test
Float_Test:
1 eq-xsymb
1 Term_Ord.typ_ord
1 Raw_Simplifier.extract_rews
1 Output_Primitives.ignore_outputs
1 Code_Symbol.symbol_ord
1 Proofterm.thm_ord
1 Multithreading.sync_wait
1 Graph().merge_trans_acyclic
1 Scan.many
1 Basics.fold_map
1 Basics.fold
1 Pretty.string
1 Type_Infer_Context.prepare_term
1 eq-xprod
1 Term.add_tvarsT
1 Print_Mode.print_mode_value
1 X86ICodeToX86Code().icodeToX86Code
1 ProofRewriteRules.rew
1 String.fields
1 List.foldr
1 Library.insert
1 Type_Infer_Context.unify
1 Term.fold_aterms
1 Term.fastype_of1
1 Raw_Simplifier.bottomc
1 Term_Ord.fast_indexname_ord
1 Term_Subst.map_aterms_same
1 Type_Infer.add_parms
1 Axclass.unoverload
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 X86ICodeIdentifyReferences().getInstructionState
1 IntSet.minusLists
1 Term_Subst.map_types_same
1 Symbol.explode
1 Graph().add_edge
1 TYPE_TREE().eventual
1 Raw_Simplifier.rewrite_rule_extra_vars
1 Path.check_elem
1 Lazy.force_result
1 Raw_Simplifier.insert_rrule
1 Term.map_types
1 Induct().concl_var
2 Generic_Data().get
2 Logic.list_implies
2
2 Table().join
2 IntSet.partition
2 Thm.deriv_rule2
2 X86CodetreeToICode().codeFunctionToX86
2 Thm.transfer
2 Term.fold_term_types
2 IntSet.mergeLists
2
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
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
Fabian
==
theory Scratch
imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin
definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) *
(float_plus_down p 1 (-x)))"
primrec iter where
"iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"
definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1))
(nat_of_integer i)"
ML ‹val logistic_chaos = @{code logistic_chaos}›
ML ‹Par_List.map logistic_chaos (replicate 10 10)›
― ‹x86_64_32: 24s
x86_64: 2s›
ML ‹map logistic_chaos (replicate 10 10)›
― ‹x86_64_32: 16s
x86_64: 8s›
end
smime.p7s
Description: S/MIME Cryptographic Signature
___
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
Hi Lars,
Am 22.01.19 um 22:34 schrieb Lars Hupel:
> It is admittedly a complicated incantation, but here you go:
>
> $ cat test.ml
> let x = Z.one;;
> let _ = print_endline (Z.to_string x);;
>
> $ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
> -linkpkg test.ml
>
> $ ./a.out
> 1
>
> You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
> look for packages.
thanks for that hint.
But ocamlfind semms not to provide a subcommand to invoke the
interactive OCaml toplevel. What am I missing?
Cheers,
Florian
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] State of the art in Isabelle with OCaml, opam and zarith
It is admittedly a complicated incantation, but here you go:
$ cat test.ml
let x = Z.one;;
let _ = print_endline (Z.to_string x);;
$ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
-linkpkg test.ml
$ ./a.out
1
You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
look for packages.
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result
Hi all, as of 82f57315cade (followed-up by AFP bf62184), the still occasionally seen Local_Theory.reset invocations are gone, conveniently replaced by Local_Theory.subtarget_result. I'm considering pushing that even further: specification tools should by contract provide a »clean« definitional extension without any artefacts of the internal construction leaking out, i. e. val specification: spec -> local_theory -> result * local_theory where »spec« is the input specification and »result« a characterization of the definitional extension with enough information to build on it in derived tools; the resulting local_theory can be continued on directly -- all internal construction steps are hid in a local subtarget. The corresponding package is supposed to provide a morphism lifter for results val transform: morphism -> result -> result hence exporting up through nested context is trivial. This would also open up the possibility to get rid of the still seen *_global variants for specification tools: using a combinator Named_Target.theory_map_result: (morphism -> 'a -> 'a) -> (local_theory -> 'a * local_theory) -> theory -> 'a * theory any Package.spec_global can be trivially inlined as Named_Target.theory_map_result Package.transform (Package.spec …) So much my current understanding of affairs. Cheers, Florian 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] State of the art in Isabelle with OCaml, opam and zarith
On 22/01/2019 22:02, Florian Haftmann wrote: > > Then I have no clue how to include the installed zarith properly. > https://opam.ocaml.org/doc/FAQ.html mentions subcommands »exec« and > »env« for opam, which the installed version available through »isabelle > ocaml_opam« does not provide. That documentation is for Opam 2.0, but we are still on 1.2.2 because that is the latest version I've found for Windows (based on MinGW); the same 1.2.2 is part of Cygwin. I can update Isabelle/Opam when there is a proper Windows version for 2.0 -- maybe it has already arrived in the meantime, somewhere in some dark corner. Apart from that, I've recently seen Coq experts worry about the status-quo of Opam: it is not as well-developed as Stack for Haskell, and Coq already critically depends on it. 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 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)
Can you point to some smaller parts of these sessions, where the effect
is visible? We can then use profiling to get an idea what actually
happens in x86_64_32.
It should be the by (tactic ...) invocations, which ultimately run
generated code as an oracle (the one defined via @{computation_check}
here:
https://bitbucket.org/isa-afp/afp-devel/src/5d11846ac6abdad9c9dfee108d2772ac71c6179c/thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy#lines-2449)
The term that is being evaluated should be printed when declaring
[[ode_numerics_trace]].
(But it takes a lot of time to get there...)
I would have assumed that it is the heavy use of int computations that
makes the difference, and it should be precisely the kind that is tested
in the attached Float_Test.thy.
On my Windows-Laptop and on lxcisa0, however, I see the expected
slowdown of about a factor of 2, but not more...
Could the issue be related to specific machines?
(I am testing HOL-ODE-ARCH-COMP with
polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take
some time...)
Fabian
theory Float_Test
imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin
definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down
p 1 (-x)))"
primrec iter where
"iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"
definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1))
(nat_of_integer i)"
ML \val logistic_chaos = @{code logistic_chaos}\
ML \logistic_chaos 100\
end
smime.p7s
Description: S/MIME Cryptographic Signature
___
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 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) Can you point to some smaller parts of these sessions, where the effect is visible? We can then use profiling to get an idea what actually happens in x86_64_32. 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
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) ML_PLATFORM="x86_64-linux" ML_OPTIONS="--minheap 2000 --maxheap 4000" Finished HOL-ODE-Numerics (0:29:34 elapsed time, 1:21:08 cpu time, factor 2.74) Finished HOL-ODE-ARCH-COMP (0:06:49 elapsed time, 0:12:41 cpu time, factor 1.86) Fabian On 1/22/2019 11:36 AM, Makarius wrote: On 19/01/2019 21:43, Makarius wrote: Thanks to great work by David Matthews, there is now an Isabelle component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" It requires the usual "isabelle components -a" incantation afterwards. polyml-test-0a6ebca445fc is the default in 81ca77cb7c8c, it means the scope of further testing has widened. Almost everything has become faster by default, but an exception are heavy-duty int computations that rely on a certain word size, notably the HOL-ODE family of sessions. AFP/a04825886e71 marks various sessions explicitly as "large", which means that they prefer x86_64. Here are concrete numbers: x86_64_32-linux -minheap 1500 Finished Pure (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00) Finished HOL (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45) Finished HOL-Analysis (0:03:48 elapsed time, 0:21:27 cpu time, factor 5.64) Finished Ordinary_Differential_Equations (0:01:14 elapsed time, 0:05:31 cpu time, factor 4.43) Finished Differential_Dynamic_Logic (0:01:29 elapsed time, 0:05:03 cpu time, factor 3.39) Finished HOL-ODE-Numerics (0:17:51 elapsed time, 0:46:30 cpu time, factor 2.60) Finished Lorenz_Approximation (0:04:02 elapsed time, 0:07:46 cpu time, factor 1.92) Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10) Finished HOL-ODE-ARCH-COMP (0:12:56 elapsed time, 0:28:35 cpu time, factor 2.21) Finished HOL-ODE-Examples (0:37:13 elapsed time, 2:51:00 cpu time, factor 4.59) Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44) x86_64-linux --minheap 3000 Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00) Finished HOL (0:02:44 elapsed time, 0:09:28 cpu time, factor 3.47) Finished HOL-Analysis (0:04:05 elapsed time, 0:22:47 cpu time, factor 5.58) Finished Ordinary_Differential_Equations (0:01:19 elapsed time, 0:05:49 cpu time, factor 4.40) Finished Differential_Dynamic_Logic (0:01:33 elapsed time, 0:05:22 cpu time, factor 3.44) Finished HOL-ODE-Numerics (0:18:59 elapsed time, 0:49:00 cpu time, factor 2.58) Finished Lorenz_Approximation (0:04:01 elapsed time, 0:07:39 cpu time, factor 1.90) Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.20) Finished HOL-ODE-ARCH-COMP (0:04:06 elapsed time, 0:08:37 cpu time, factor 2.10) Finished HOL-ODE-Examples (0:05:18 elapsed time, 0:17:04 cpu time, factor 3.22) Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ 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 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" > > It requires the usual "isabelle components -a" incantation afterwards. polyml-test-0a6ebca445fc is the default in 81ca77cb7c8c, it means the scope of further testing has widened. Almost everything has become faster by default, but an exception are heavy-duty int computations that rely on a certain word size, notably the HOL-ODE family of sessions. AFP/a04825886e71 marks various sessions explicitly as "large", which means that they prefer x86_64. Here are concrete numbers: x86_64_32-linux -minheap 1500 Finished Pure (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00) Finished HOL (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45) Finished HOL-Analysis (0:03:48 elapsed time, 0:21:27 cpu time, factor 5.64) Finished Ordinary_Differential_Equations (0:01:14 elapsed time, 0:05:31 cpu time, factor 4.43) Finished Differential_Dynamic_Logic (0:01:29 elapsed time, 0:05:03 cpu time, factor 3.39) Finished HOL-ODE-Numerics (0:17:51 elapsed time, 0:46:30 cpu time, factor 2.60) Finished Lorenz_Approximation (0:04:02 elapsed time, 0:07:46 cpu time, factor 1.92) Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10) Finished HOL-ODE-ARCH-COMP (0:12:56 elapsed time, 0:28:35 cpu time, factor 2.21) Finished HOL-ODE-Examples (0:37:13 elapsed time, 2:51:00 cpu time, factor 4.59) Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44) x86_64-linux --minheap 3000 Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00) Finished HOL (0:02:44 elapsed time, 0:09:28 cpu time, factor 3.47) Finished HOL-Analysis (0:04:05 elapsed time, 0:22:47 cpu time, factor 5.58) Finished Ordinary_Differential_Equations (0:01:19 elapsed time, 0:05:49 cpu time, factor 4.40) Finished Differential_Dynamic_Logic (0:01:33 elapsed time, 0:05:22 cpu time, factor 3.44) Finished HOL-ODE-Numerics (0:18:59 elapsed time, 0:49:00 cpu time, factor 2.58) Finished Lorenz_Approximation (0:04:01 elapsed time, 0:07:39 cpu time, factor 1.90) Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.20) Finished HOL-ODE-ARCH-COMP (0:04:06 elapsed time, 0:08:37 cpu time, factor 2.10) Finished HOL-ODE-Examples (0:05:18 elapsed time, 0:17:04 cpu time, factor 3.22) Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52) 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 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)? 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.) Makarius ___ 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?
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] Poly/ML x86_64_32 available for testing
Looks impressive. Thanks! Larry > On 22 Jan 2019, at 11:27, Makarius wrote: > > Here are some performance measurements on the best hardware that I have > presently access to (not at TUM): ___ 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: > 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. Thanks a lot, David and Makarius! Bertram ___ 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 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" > > It requires the usual "isabelle components -a" incantation afterwards. Here are some performance measurements on the best hardware that I have presently access to (not at TUM): Intel Xeon Gold 6148 CPU @ 2.40GHz 20 CPU cores * 2 hyperthreads * 2 nodes 64 GB memory SSD Isabelle/2633e166136a + AFP/ba82c831e5c2 isabelle build -N -j2 -o threads=8 x86-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL-Analysis (0:03:49 elapsed time, 0:21:11 cpu time, factor 5.55) Finished HOL-Analysis (0:03:50 elapsed time, 0:21:19 cpu time, factor 5.55) Finished HOL-Data_Structures (0:01:39 elapsed time, 0:11:30 cpu time, factor 6.91) Finished HOL-Data_Structures (0:01:43 elapsed time, 0:11:52 cpu time, factor 6.87) Finished HOL-Nominal (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.34) Finished HOL-Nominal (0:00:29 elapsed time, 0:01:08 cpu time, factor 2.33) Finished HOL-Nominal-Examples (0:02:57 elapsed time, 0:14:11 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:03:09 elapsed time, 0:14:55 cpu time, factor 4.73) Finished HOL-Proofs (0:09:52 elapsed time, 0:23:45 cpu time, factor 2.41) Finished HOL-Proofs (0:09:52 elapsed time, 0:24:04 cpu time, factor 2.44) x86_64_32-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.49) Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.48) Finished HOL-Analysis (0:03:41 elapsed time, 0:20:56 cpu time, factor 5.67) Finished HOL-Analysis (0:03:39 elapsed time, 0:20:50 cpu time, factor 5.70) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:33 cpu time, factor 7.16) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:35 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:24 cpu time, factor 2.07) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.06) Finished HOL-Nominal-Examples (0:02:53 elapsed time, 0:13:54 cpu time, factor 4.82) Finished HOL-Nominal-Examples (0:02:51 elapsed time, 0:13:51 cpu time, factor 4.83) Finished HOL-Proofs (0:09:55 elapsed time, 0:23:48 cpu time, factor 2.40) Finished HOL-Proofs (0:09:48 elapsed time, 0:23:35 cpu time, factor 2.40) x86_64_32-linux --minheap 3000 --maxheap 7000 Finished HOL (0:02:32 elapsed time, 0:08:53 cpu time, factor 3.50) Finished HOL (0:02:32 elapsed time, 0:08:51 cpu time, factor 3.49) Finished HOL-Analysis (0:03:26 elapsed time, 0:20:06 cpu time, factor 5.84) Finished HOL-Analysis (0:03:45 elapsed time, 0:21:20 cpu time, factor 5.67) Finished HOL-Data_Structures (0:01:35 elapsed time, 0:11:32 cpu time, factor 7.26) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:36 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.08) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.10) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.88) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.87) Finished HOL-Proofs (0:08:10 elapsed time, 0:19:17 cpu time, factor 2.36) Finished HOL-Proofs (0:08:23 elapsed time, 0:19:13 cpu time, factor 2.29) x86_64-linux --minheap 1500 --maxheap 7000 Finished HOL (0:02:48 elapsed time, 0:09:46 cpu time, factor 3.48) Finished HOL (0:02:46 elapsed time, 0:09:34 cpu time, factor 3.45) Finished HOL-Analysis (0:04:01 elapsed time, 0:22:39 cpu time, factor 5.64) Finished HOL-Analysis (0:04:00 elapsed time, 0:22:27 cpu time, factor 5.60) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:49 cpu time, factor 6.47) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:42 cpu time, factor 6.46) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.05) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04) Finished HOL-Nominal-Examples (0:03:03 elapsed time, 0:14:39 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:02:58 elapsed time, 0:14:29 cpu time, factor 4.88) Finished HOL-Proofs (0:10:16 elapsed time, 0:25:24 cpu time, factor 2.47) Finished HOL-Proofs (0:10:21 elapsed time, 0:25:35 cpu time, factor 2.47) x86_64-linux --minheap 3000 --maxheap 14000 Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.46) Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.47) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:40 cpu time, factor 5.51) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:54 cpu time, factor 5.57) Finished HOL-Data_Structures (0:01:44 elapsed time, 0:12:28 cpu time, factor 7.14) Finished HOL-Data_Structures (0:01:43 elapsed
