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

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

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

2019-01-25 Thread Fabian Immler
Great, thanks for looking into this! Fabian On 1/23/2019 4:24 PM, David Matthews wrote: 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

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

2019-01-25 Thread Makarius
On 23/01/2019 23:44, Makarius wrote: > 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. One more

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

2019-01-25 Thread Tobias Nipkow
This is really phantastic - at last I can build HOL-Analysis on my terrible new Mac without having to put it in the freezer and it does not fall over at the very end. It is also 20% faster. Great work! Tobias On 19/01/2019 21:43, Makarius wrote: Thanks to great work by David Matthews, there