Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

> That suggests that you're running the 32-bit version of Poly/ML in which
> case the heap is limited to around 3-3.5G by the system and the problem
> you're having is the total 4G memory limit.  Switch to the 64-bit
> version as a starting point.  I was assuming that with 32G of memory you
> were running the 64-bit version already.

No, I initially planned to, but Makarius usually advises against it. I'm
not sure how to proceed here.

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

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

On 22/02/2016 07:58, Lars Hupel wrote:

Another possibility is to set the maximum heap size with --maxheap e.g.
ML_OPTIONS="--maxheap 28G"
If the application needs it Poly/ML will try to grow the heap to avoid
doing a lot of garbage collection.  That can result in it crowding out
other parts of the system that also need memory.  The "Unable to
increase stack" probably results from it being unable to grow an ML
stack if the application recurses very deeply.  I'm guessing that you
don't have any swap space configured so there's no leeway there.  You
may have to experiment with the setting.  You don't need --stackspace if
you set the maximum heap size.


Thanks for the hint. Indeed, there's no swap space configured, because
all the build boxes have 32 GB of RAM.

I've tried setting the --maxheap to 4 GB, but here's the error I'm getting:

   Value of --maxheap option is too large

(Relevant build log:
)


That suggests that you're running the 32-bit version of Poly/ML in which 
case the heap is limited to around 3-3.5G by the system and the problem 
you're having is the total 4G memory limit.  Switch to the 64-bit 
version as a starting point.  I was assuming that with 32G of memory you 
were running the 64-bit version already.


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

Re: [isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]

[Thiemann, Rene]

Dear Florian,

thanks for the info.

Concerning the factorial semiring, we also made some development in that 
direction which we required
for the algebraic numbers. To be more precise, we have an instance of

poly :: (ufd) ufd

where ufd is a unique factorization domain, cf.

http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Domain.html
and
http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Poly.html

Perhaps we should share efforts on this topic (but please after the ITP 
deadline).

Cheers,
René

> Am 18.02.2016 um 17:00 schrieb Florian Haftmann 
> :
> 
> Hi Rene,
> 
> see now fd049b54ad68 for an abstract semiring_gcd with a corresponding
> poly :: (field) semiring_gcd instance.
> 
> Btw. in my pipeline there is an abstract factorial ring with
> 
>   subclass (in factorial_semiring) semiring_gcd
> 
> and hence the possibility to formulate also the other prominent instance
> 
>   poly :: (factorial_semiring) factorial_semiring
> 
> This will still take some time however.
> 
> Cheers,
>   Florian
> 
> Am 15.01.2016 um 12:12 schrieb Thiemann, Rene:
>> 
>>> Am 14.01.2016 um 15:36 schrieb Makarius :
>>> 
>>> On Thu, 14 Jan 2016, Florian Haftmann wrote:
>>> 
>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>> thus very hardly different from syntactic classes, so there is no loss
>> of generality here.
> 
> I disagree with this second item: the classes (semi)ring_gcd in 
> Isabelle2015 have
> the three essential lemmas:
> 
> gcd_dvd1, gcd_dvd2, and gcd_greatest.
 
 indeed, but these are exactly the assumptions of the type class.
 
> And since you want to include the patch anyway, why not include at least 
> the instance now?
 
 It sits on top of a couple of other patches definitely not suitable for
 inclusion by now.
>>> 
>>> Does it mean this thread is closed concerning Isabelle2016?
>> 
>> If Florian has a post-release patch available and wants to insert exactly 
>> that patch,
>> then that’s fine for me.
>> 
>> Then Isabelle users (including myself) can just load the proposed instance 
>> declaration from the AFP to
>> uniformly access the gcd-properties via the semiring-class(-axioms) in 
>> Isabelle 2016.
>> 
>> Cheers,
>> René
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> --
> 
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev