5 Isac's tests are organised parallel to sources: |
5 Isac's tests are organised parallel to sources: |
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" |
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" |
7 plus |
7 plus |
8 ~~/test/Tools/isac/ADDTESTS |
8 ~~/test/Tools/isac/ADDTESTS |
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality |
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality |
10 |
10 ------------------------------------------------------------------------------- |
|
11 |
|
12 Prepare running tests: see below |
|
13 Run tests: |
11 $ cd /usr/local/isabisac/ |
14 $ cd /usr/local/isabisac/ |
|
15 $ export ISABELLE_VERSION=2015 # for libisabelle |
12 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
16 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & |
13 *) |
17 *) |
14 |
18 |
15 section \<open>Prepare running tests\<close> |
19 section \<open>Prepare running tests\<close> |
16 text \<open> |
20 text \<open> |
17 Isac encapsulates code as much as possible in structures without open. TODO |
21 Isac encapsulates code as much as possible in structures without open. TODO ProgLang. |
18 This policy conflicts with those tests, which go into functions to details |
22 This policy conflicts with those tests, which go into functions to details |
19 not declared in the signatures. |
23 not declared in the signatures. |
20 |
24 |
21 In order to maintain these tests without changes, this has to be done before running tests: |
25 In order to maintain these tests without changes, this has to be done before running tests: |
22 (1) Query replace in src/Tools/isac: |
26 (1) Extend signatures for tests by |
|
27 ~~$ ./xcoding-to-test.sh |
|
28 ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy |
|
29 Running Test_Isac.thy opens all structures, see code after "begin" below. |
|
30 (2) Clean signatures for coding |
|
31 ~~$ ./xtest-to-coding.sh |
|
32 ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!) |
|
33 |
|
34 ********************* don't forget (2) BEFORE pushing to repository ********************* |
|
35 |
|
36 The above bash files accomplish query replace in src/Tools/isac: |
23 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit> |
37 \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit> |
24 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit> |
38 \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit> |
25 ^^^ in signature outcommented, ^^^ NOT outcommented, |
39 ^^^ in signature outcommented, ^^^ NOT outcommented, |
26 this is status for coding this is status for tests |
40 this is status for coding this is status for tests |
27 "NOT outcommented" extends the signatures with some functions required for some tests. |
|
28 |
|
29 Running Test_Isac.thy opens all structures, see code after "begin" below. |
|
30 |
|
31 * before running Test_Isac.thy ^^^ \<longrightarrow> ^^^ in src/Tools/isac |
|
32 * after running Test_Isac.thy ^^^ <-- ^^^ in src/Tools/isac |
|
33 *********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS *********************** |
|
34 \<close> |
41 \<close> |
35 |
42 |
36 section \<open>Run the tests\<close> |
43 section \<open>Run the tests\<close> |
37 text \<open> |
44 text \<open> |
38 * say "OK" to the popup asking for theories to be loaded |
45 * say "OK" to the popup asking for theories to be loaded |
216 |
223 |
217 !!! Use most recent tests or go back to the old notebook |
224 !!! Use most recent tests or go back to the old notebook |
218 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
225 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
219 *} |
226 *} |
220 |
227 |
|
228 |
|
229 subsection {* isac on Isabelle2015 *} |
|
230 subsubsection {* Summary of development *} |
|
231 text {* |
|
232 * Add signatures from top of thy-hierarchy down to Interpret, not ProgLang. |
|
233 This complicates Test_Isac, see "Prepare running tests" above. |
|
234 * Remove TTY interface. |
|
235 * Re-activate insertion sort. |
|
236 *} |
|
237 subsubsection {* State of tests: unchanged *} |
|
238 subsubsection {* Changesets of begin and end *} |
|
239 text {* |
|
240 last changeset with Test_Isac 2f1b2854927a |
|
241 first changeset with Test_Isac ??? |
|
242 *} |
|
243 |
221 subsection {* isac on Isabelle2014 *} |
244 subsection {* isac on Isabelle2014 *} |
222 subsubsection {* Summary of development *} |
245 subsubsection {* Summary of development *} |
223 text {* |
246 text {* |
224 migration from "isabelle tty" --> libisabelle |
247 migration from "isabelle tty" --> libisabelle |
225 *} |
248 *} |