Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Fabian Immler
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

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

2019-01-22 Thread Florian Haftmann
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 > > $

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

2019-01-22 Thread 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")

[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

2019-01-22 Thread Florian Haftmann
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

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

2019-01-22 Thread Makarius
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

[isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

2019-01-22 Thread Florian Haftmann
Hi all, I plan to go some steps to use zarith for integer arithmetic for code generated in OCaml, and at the moment I am surrounded by tapestry. As of, 331ef175a112, I issue the following steps: $ isabelle ocaml_setup --> fine $ isabelle ocaml_opam install zarith --> fine $

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Fabian Immler
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
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: > >

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Fabian Immler
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
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

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

2019-01-22 Thread Lawrence Paulson
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Lawrence Paulson
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Bertram Felgenhauer
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
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