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
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
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
>
> $
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")
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
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
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
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:
>
>
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
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
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
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
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
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
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
15 matches
Mail list logo
