*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Algebraic_Numbers*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Thu, 2 Jun 2016 09:32:05 +0000*Accept-language*: de-DE, de-AT, en-US*Cc*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <574FE349.9040606@informatik.tu-muenchen.de>*References*: <34d483c8-0558-11f6-a1f3-d5932e44cfb0@in.tum.de> <574FE349.9040606@informatik.tu-muenchen.de>*Thread-index*: AQHRvKI0jgM9FbxIGU+VSiHyzvxUqp/VqbOAgAAewAA=*Thread-topic*: [isabelle] Algebraic_Numbers

Dear all, it is perfectly fine to me, to create a separate target in the ROOT file without the tests, e.g., as indicated below. However, Iâm unsure how the document preparation will work in this way. Somehow both entries contribute to the final PDF, i.e., both parts should be displayed on the AFP-website. Does anybody know an easy solution to this? Cheers, RenÃ session Algebraic_Numbers_With_Tests (AFP) = Algebraic_Numbers + description {* Testing Algebraic Number *} options [timeout = 1200] theories "Algebraic_Number_Tests" document_files "root.bib" "root.tex" session Algebraic_Numbers (AFP) = Pre_Algebraic_Numbers + description {* Algebraic Numbers *} options [timeout = 600] theories "Missing_Multiset" "Missing_List" "Compare_Complex" "Improved_Code_Equations" "Precomputation" "Is_Rat_To_Rat" "Ring_Hom_Poly" "Order_Polynomial" "Binary_Exponentiation" "Explicit_Roots" "Rational_Root_Test" "Kronecker_Factorization" "Square_Free_Factorization" "Berlekamp_Hensel_Factorization" "Rational_Factorization" "Real_Factorization" "Show_Real_Approxâ "Show_Real_Precise" document_files "root.bib" "root.tex" > Am 02.06.2016 um 09:42 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>: > >> I noticed that a huge chunk of the resource hunger of that development >> actually comes from Algebraic_Number_Tests.thy, which one does not even >> need in order to use the development. >> >> Now, I don't know if and by how much this reduces the memory >> requirements and I have no idea how to measure this reliably. In any >> case, I do not see any drawbacks of doing this. > > IMHO it is good style that things on which others are supposed to build > upon contain only libraries, not tests. So, I would suggest to go ahead. > > Cheers, > Florian Haftmann > > -- > > PGP available: > http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de >

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

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

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

- Previous by Date: Re: [isabelle] Algebraic_Numbers
- Next by Date: [isabelle] SAT solver problem
- 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