*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Algebraic_Numbers*From*: Lars Hupel <hupel at in.tum.de>*Date*: Fri, 3 Jun 2016 23:17:15 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5750A3B8.4070208@sketis.net>*References*: <34d483c8-0558-11f6-a1f3-d5932e44cfb0@in.tum.de> <574FE349.9040606@informatik.tu-muenchen.de> <E1491251-20E2-4993-A058-5167D9C88F77@uibk.ac.at> <251ba710-5d97-3eee-7a24-ca07fbbc7f3b@in.tum.de> <696C6BAF-9C2F-40BE-AEEE-0F0B336FF7A2@nicta.com.au> <1667CB23-B68C-42A9-BF7D-2FACD8C6CE24@uibk.ac.at> <bc6ee781-85b8-2f94-13d8-5bca02064470@in.tum.de> <57504FA9.3010008@sketis.net> <E3369AA1-D02B-4D31-94A6-A40F3A212315@nicta.com.au> <5750A3B8.4070208@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.0

> I think the worries of Lars Hupel are based on the rather weak > Isabelle/Jenkins testing hardware. My own worries are based on general > observations that Algebraic_Numbers could be close to the infamous > "invisible concrete wall" (without detailed measurements yet). Better hardware is on its way. > There are already AFP entries with more than one session, and also > add-on documents. Maybe that is already sufficient to publish the tests > separately, or maybe not. Lars Hupel might be able to say that. Presently, all documents for the development version are built, but not published. The reason for that is that it turns out the disk space requirements to retain all HTML and PDF files is excessive (dozens of GB amassed during two or three weeks). I have a changeset to the build server in my pipeline which will retain the latest set of documents. (NB, build logs are retained and will be retained forever; they are relatively small due to compression.) The remaining question is how these documents will be presented in AFP. Currently only the documents of the main sessions are linked from the entry pages. > Stepping back further, the question is why Algebraic_Number_Tests > requires so much persistent heap memory that sessions built on it might > get into problems. Maybe there is a deeper resource problem behind it. That is an excellent question. I still can't quite put my finger on it as to why that single theory forces us to run AFP tests in bulky 64 bit mode. Cheers Lars

**Follow-Ups**:**Re: [isabelle] Algebraic_Numbers***From:*Makarius

**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

**References**:**[isabelle] Algebraic_Numbers***From:*Manuel Eberl

**Re: [isabelle] Algebraic_Numbers***From:*Florian Haftmann

**Re: [isabelle] Algebraic_Numbers***From:*Thiemann, Rene

**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

**Re: [isabelle] Algebraic_Numbers***From:*Makarius

**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

**Re: [isabelle] Algebraic_Numbers***From:*Makarius

- Previous by Date: Re: [isabelle] Algebraic_Numbers
- Next by Date: Re: [isabelle] Algebraic_Numbers
- Previous by Thread: Re: [isabelle] Algebraic_Numbers
- Next by Thread: Re: [isabelle] Algebraic_Numbers
- Cl-isabelle-users June 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