Re: [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
Description: Message signed with OpenPGP using GPGMail



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.