Re: [isabelle-dev] Question about testing isabelle with Poly/ML x86_64_32

2019-01-29 Thread Makarius
On 29/01/2019 16:14, João Rafael Nicola wrote:
> 
> I've been using Isabelle/2018 in x86 (32) mode on a Xeon E3-1505M
> (2.80GHz, 3.6Ghz turbo) 4-core, 64GB machine. Since I run frequently
> into timeouts while running sledgehammer, proof methods
> (metis,meson,etc.) or processing notation-heavy locales, I would like to
> know how can I determine whether or not a shift to x86_64_32 would help.
> How can I determine if the limited heap size of x86_32 Poly/ML might be
> hindering Isabelle?

Isabelle/jEdit has a "Monitor" panel, its "Heap" tab might provide some
clues.

The current test version of Poly/ML is polyml-test-1b2dcf8f5202. If you
keep an eye on changing versions of
https://isabelle.in.tum.de/repos/isabelle/file/tip/Admin/components/main
you will see what is the latest and greatest one.

Note that we still have 1 or 2 hard crash situations that need to be
sorted out.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


[isabelle-dev] Question about testing isabelle with Poly/ML x86_64_32

2019-01-29 Thread João Rafael Nicola
Dear Isabelle developers,

I've been using Isabelle/2018 in x86 (32) mode on a Xeon E3-1505M (2.80GHz,
3.6Ghz turbo) 4-core, 64GB machine. Since I run frequently into timeouts
while running sledgehammer, proof methods (metis,meson,etc.) or processing
notation-heavy locales, I would like to know how can I determine whether or
not a shift to x86_64_32 would help. How can I determine if the limited
heap size of x86_32 Poly/ML might be hindering Isabelle?

Thank you in advance,

Joao Rafael Nicola
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev