1.1 --- a/README_WN Fri Nov 17 05:49:54 2017 +0100
1.2 +++ b/README_WN Thu Jan 18 15:25:39 2018 +0100
1.3 @@ -1,3 +1,7 @@
1.4
1.5 -
1.6 - see ../isabisac13-2/README_WN
1.7 +# test-setup according to ~~/test/Tools/isac/Test_Isac.thy
1.8 + xcoding-to-test.sh # extend signatures for tests
1.9 + zcoding-to-test.sh # -"- + go back to Test_Isac.thy
1.10 +
1.11 + xtest-to-coding.sh # clean signatures for coding
1.12 + ztest-to-coding.sh # -"- + go back to coding (!update thy!)
2.1 --- a/src/Tools/isac/ROOT Fri Nov 17 05:49:54 2017 +0100
2.2 +++ b/src/Tools/isac/ROOT Thu Jan 18 15:25:39 2018 +0100
2.3 @@ -2,6 +2,7 @@
2.4 Author: Walther Neuper, TU Graz, 130715
2.5 (c) due to copyright terms
2.6
2.7 +$ export ISABELLE_VERSION=2015 # for libisabelle
2.8 $ cd /usr/local/isabisac/
2.9 $ ./bin/isabelle build -v -b Isac
2.10
3.1 --- a/test/Tools/isac/Test_Isac.thy Fri Nov 17 05:49:54 2017 +0100
3.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jan 18 15:25:39 2018 +0100
3.3 @@ -7,30 +7,37 @@
3.4 plus
3.5 ~~/test/Tools/isac/ADDTESTS
3.6 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
3.7 +-------------------------------------------------------------------------------
3.8
3.9 +Prepare running tests: see below
3.10 +Run tests:
3.11 $ cd /usr/local/isabisac/
3.12 +$ export ISABELLE_VERSION=2015 # for libisabelle
3.13 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
3.14 *)
3.15
3.16 section \<open>Prepare running tests\<close>
3.17 text \<open>
3.18 -Isac encapsulates code as much as possible in structures without open. TODO
3.19 +Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
3.20 This policy conflicts with those tests, which go into functions to details
3.21 not declared in the signatures.
3.22
3.23 In order to maintain these tests without changes, this has to be done before running tests:
3.24 -(1) Query replace in src/Tools/isac:
3.25 +(1) Extend signatures for tests by
3.26 + ~~$ ./xcoding-to-test.sh
3.27 + ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
3.28 + Running Test_Isac.thy opens all structures, see code after "begin" below.
3.29 +(2) Clean signatures for coding
3.30 + ~~$ ./xtest-to-coding.sh
3.31 + ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
3.32 +
3.33 +********************* don't forget (2) BEFORE pushing to repository *********************
3.34 +
3.35 +The above bash files accomplish query replace in src/Tools/isac:
3.36 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
3.37 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
3.38 ^^^ in signature outcommented, ^^^ NOT outcommented,
3.39 this is status for coding this is status for tests
3.40 - "NOT outcommented" extends the signatures with some functions required for some tests.
3.41 -
3.42 -Running Test_Isac.thy opens all structures, see code after "begin" below.
3.43 -
3.44 -* before running Test_Isac.thy ^^^ \<longrightarrow> ^^^ in src/Tools/isac
3.45 -* after running Test_Isac.thy ^^^ <-- ^^^ in src/Tools/isac
3.46 -*********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS ***********************
3.47 \<close>
3.48
3.49 section \<open>Run the tests\<close>
3.50 @@ -218,6 +225,22 @@
3.51 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.52 *}
3.53
3.54 +
3.55 +subsection {* isac on Isabelle2015 *}
3.56 +subsubsection {* Summary of development *}
3.57 +text {*
3.58 + * Add signatures from top of thy-hierarchy down to Interpret, not ProgLang.
3.59 + This complicates Test_Isac, see "Prepare running tests" above.
3.60 + * Remove TTY interface.
3.61 + * Re-activate insertion sort.
3.62 +*}
3.63 +subsubsection {* State of tests: unchanged *}
3.64 +subsubsection {* Changesets of begin and end *}
3.65 +text {*
3.66 + last changeset with Test_Isac 2f1b2854927a
3.67 + first changeset with Test_Isac ???
3.68 +*}
3.69 +
3.70 subsection {* isac on Isabelle2014 *}
3.71 subsubsection {* Summary of development *}
3.72 text {*
4.1 --- a/xcoding-to-test.sh Fri Nov 17 05:49:54 2017 +0100
4.2 +++ b/xcoding-to-test.sh Thu Jan 18 15:25:39 2018 +0100
4.3 @@ -4,4 +4,4 @@
4.4 cd src/Tools/isac
4.5 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/g {} \;
4.6 find . -type f -exec sed -i s/'( \*\\--- ! aktivate for Test_Isac END ---'/'(\*\\--- ! aktivate for Test_Isac END ---'/g {} \;
4.7 -cd ../../../
4.8 +cd ../../../ # go back to ~~/.
5.1 --- a/xtest-to-coding.sh Fri Nov 17 05:49:54 2017 +0100
5.2 +++ b/xtest-to-coding.sh Thu Jan 18 15:25:39 2018 +0100
5.3 @@ -4,4 +4,4 @@
5.4 cd src/Tools/isac
5.5 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
5.6 find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
5.7 -cd ../../../
5.8 \ No newline at end of file
5.9 +cd ../../../ # go back to ~~/.
6.1 --- a/zcoding-to-test.sh Fri Nov 17 05:49:54 2017 +0100
6.2 +++ b/zcoding-to-test.sh Thu Jan 18 15:25:39 2018 +0100
6.3 @@ -4,5 +4,7 @@
6.4 cd src/Tools/isac
6.5 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/g {} \;
6.6 find . -type f -exec sed -i s/'( \*\\--- ! aktivate for Test_Isac END ---'/'(\*\\--- ! aktivate for Test_Isac END ---'/g {} \;
6.7 -cd ../../../
6.8 +cd ../../../ # go back to ~~/.
6.9 +
6.10 +# immediately go to testing
6.11 ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
7.1 --- a/ztest-to-coding.sh Fri Nov 17 05:49:54 2017 +0100
7.2 +++ b/ztest-to-coding.sh Thu Jan 18 15:25:39 2018 +0100
7.3 @@ -1,8 +1,10 @@
7.4 # switches isac from test-mode to coding-mode:
7.5 -# this closes signatures as much as possible for coding;
7.6 +# this closes signatures as much as possible for coding.
7.7
7.8 cd src/Tools/isac
7.9 find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
7.10 find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
7.11 -cd ../../../
7.12 -./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &
7.13 \ No newline at end of file
7.14 +cd ../../../ # go back to ~~/.
7.15 +
7.16 +# immediately go to correcting code in Interpret/
7.17 +./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &