*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] yet another simplifier question*From*: noam neer <noamneer at gmail.com>*Date*: Sun, 6 Nov 2016 21:31:46 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <cd8825a1-3f2b-08c8-bec0-a23bf343257e@sketis.net>*References*: <CAGOKs0_QVcuM1gVkD3kt3wnpSONdP-vFFzO+qcaA6MjDAH4Z9g@mail.gmail.com> <a0ba4baa-8d66-ce82-9092-e992ff31ea26@in.tum.de> <CAGOKs08vyp6s4DvU8tVedaXM=7RTkL9kRzWSwKCPoc7O-hjGiQ@mail.gmail.com> <BE52C37D-839B-41E5-AFCC-62DA5563D817@cam.ac.uk> <CAGOKs08NpTbnzz-C2A-DdmFp5=P-Q++7Mye-Zj_1eCOreW5MRA@mail.gmail.com> <697aace1-0e2c-37a3-0927-a7425bbd7728@sketis.net> <CAGOKs098Ozp+cM8mALJoDww-dW=teOLEzOhJzfWqeZk+skhA2g@mail.gmail.com> <cd8825a1-3f2b-08c8-bec0-a23bf343257e@sketis.net>

I have an i3 processor and 4GB RAM. but, does sledgehammer give the external provers a time limit, a limit on the search space/number of deductions or no limit at all? in the first case, I guess one can expect different computers will differ not only in running time but in the actual results too. On Sun, Nov 6, 2016 at 8:42 PM, Makarius <makarius at sketis.net> wrote: > On 06/11/16 19:13, noam neer wrote: > > well, the computer itself is much older. > > does Isabelle 2016 require significantly more memory? > > Not much. You should try. > > A very old computer might be actually a source of these problems. The > minimal system requirements for Isabelle are 2 cores + 4 GB RAM. This is > not spelt out anywhere, because that is really minimal -- consumer > hardware from many years ago had this already. > > > Makarius > >

**Follow-Ups**:**Re: [isabelle] yet another simplifier question***From:*Makarius

**References**:**[isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Tobias Nipkow

**Re: [isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Lawrence Paulson

**Re: [isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Makarius

**Re: [isabelle] yet another simplifier question***From:*noam neer

**Re: [isabelle] yet another simplifier question***From:*Makarius

- Previous by Date: Re: [isabelle] yet another simplifier question
- Next by Date: Re: [isabelle] yet another simplifier question
- Previous by Thread: Re: [isabelle] yet another simplifier question
- Next by Thread: Re: [isabelle] yet another simplifier question
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list