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

2019-01-23 Thread Lars Hupel
> 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

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

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

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

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

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

2019-01-23 Thread David Matthews
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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)

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

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

2019-01-23 Thread Traytel Dmitriy
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

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

2019-01-23 Thread Blanchette, J.C.
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

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

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

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

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

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

2019-01-23 Thread David Matthews
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

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

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