1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Jan 17 17:25:26 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Jan 18 15:17:59 2018 +0100
     1.3 @@ -7,34 +7,37 @@
     1.4     plus
     1.5       ~~/test/Tools/isac/ADDTESTS
     1.6       ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
     1.7 +-------------------------------------------------------------------------------
     1.8  
     1.9 +Prepare running tests: see below
    1.10 +Run tests:
    1.11  $ cd /usr/local/isabisac/
    1.12 +$ export ISABELLE_VERSION=2015 # for libisabelle
    1.13  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
    1.14  *)
    1.15  
    1.16  section \<open>Prepare running tests\<close>
    1.17  text \<open>
    1.18 -Isac encapsulates code as much as possible in structures without open. TODO
    1.19 +Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
    1.20  This policy conflicts with those tests, which go into functions to details
    1.21  not declared in the signatures.
    1.22  
    1.23  In order to maintain these tests without changes, this has to be done before running tests:
    1.24 -(1) Query replace in src/Tools/isac:
    1.25 +(1) Extend signatures for tests by
    1.26 +    ~~$ ./xcoding-to-test.sh
    1.27 +    ~~$ ./zcoding-to-test.sh  # -"- + go back to Test_Isac.thy
    1.28 +    Running Test_Isac.thy opens all structures, see code after "begin" below.
    1.29 +(2) Clean signatures for coding
    1.30 +    ~~$ ./xtest-to-coding.sh
    1.31 +    ~~$ ./xtest-to-coding.sh  # -"- + go back to coding (!update thy!)
    1.32 +
    1.33 +********************* don't forget (2) BEFORE pushing to repository *********************
    1.34 +
    1.35 +The above bash files accomplish query replace in src/Tools/isac:
    1.36      \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
    1.37      \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit>   \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
    1.38       ^^^ in signature outcommented,                     ^^^ NOT outcommented,
    1.39           this is status for coding                          this is status for tests
    1.40 -  "NOT outcommented" extends the signatures with some functions required for some tests.
    1.41 -
    1.42 -Running Test_Isac.thy opens all structures, see code after "begin" below.
    1.43 -
    1.44 -*   before running Test_Isac.thy  ^^^            \<longrightarrow>  ^^^  in src/Tools/isac
    1.45 -*   after running Test_Isac.thy   ^^^            <--  ^^^  in src/Tools/isac
    1.46 -*********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS ***********************
    1.47 -
    1.48 -rebuild Isac (with ^^^updated files) by
    1.49 -$ export ISABELLE_VERSION=2015 # for libisabelle
    1.50 -$ ./bin/isabelle build -v -b Isac
    1.51  \<close>
    1.52  
    1.53  section \<open>Run the tests\<close>
    1.54 @@ -222,6 +225,22 @@
    1.55        with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
    1.56  *}
    1.57  
    1.58 +
    1.59 +subsection {* isac on Isabelle2015 *}
    1.60 +subsubsection {* Summary of development *}
    1.61 +text {*
    1.62 +  * Add signatures from top of thy-hierarchy down to Interpret, not ProgLang.
    1.63 +    This complicates Test_Isac, see "Prepare running tests" above.
    1.64 +  * Remove TTY interface.
    1.65 +  * Re-activate insertion sort.
    1.66 +*}
    1.67 +subsubsection {* State of tests: unchanged *}
    1.68 +subsubsection {* Changesets of begin and end *}
    1.69 +text {*
    1.70 +  last changeset with Test_Isac 2f1b2854927a
    1.71 +  first changeset with Test_Isac ???
    1.72 +*}
    1.73 +
    1.74  subsection {* isac on Isabelle2014 *}
    1.75  subsubsection {* Summary of development *}
    1.76  text {*