test/Tools/isac/Test_Isac_Short.thy
changeset 59626 7b53f514b5e9
parent 59624 eb29ccf2da34
child 59628 3ba64c992e64
equal deleted inserted replaced
59625:1ebbd31aab7b 59626:7b53f514b5e9
    29 \<close>
    29 \<close>
    30 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
    30 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
    31 text \<open>
    31 text \<open>
    32   Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
    32   Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
    33   if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
    33   if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
    34   This exception can be avoided by ML_system_64 = "true" in ~~/etc/preferences.
    34   This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
       
    35   A model is in the repository at ~~/etc/preferences.
    35   These preferences have drawbacks, however:
    36   These preferences have drawbacks, however:
    36   * they claim more memory such that Isabelle instances canNOT run in parallel.
    37   * they claim more memory such that Isabelle instances canNOT run in parallel.
    37   * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
    38   * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
    38 
    39 
    39   So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
    40   So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
    40   From time to time full testing in Test_Isac.thy is recommended. For that purpose
    41   From time to time full testing in Test_Isac.thy is recommended. For that purpose
    41   * set ML_system_64 = "true"
    42   * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
    42 
    43 
    43 ********************* don't forget to re-set defaults BEFORE updating code *********************
    44 ********************* don't forget to re-set defaults BEFORE updating code *********************
    44 
    45 
    45     Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always
    46     Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
    46     ******* edit etc/preferences by use of gedit ******* 
    47     ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
    47 \<close>
    48 \<close>
    48 
    49 
    49 section \<open>code for copy & paste\<close>
    50 section \<open>code for copy & paste\<close>
    50 text \<open>
    51 text \<open>
    51 "~~~~~ fun , args:"; val () = ();
    52 "~~~~~ fun , args:"; val () = ();