| author | bulwahn |
| Wed, 20 Jul 2011 08:16:42 +0200 | |
| changeset 43916 | eabe4d6fbd13 |
| parent 43850 | 7f2cbc713344 |
| child 43938 | 78a0a2ad91a3 |
| permissions | -rw-r--r-- |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39544
diff
changeset
|
1 |
use_thys [ |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39616
diff
changeset
|
2 |
"Examples", |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39616
diff
changeset
|
3 |
"Predicate_Compile_Tests", |
|
40055
1f7cc5357d96
temporary removed Predicate_Compile_Quickcheck_Examples from tests
bulwahn
parents:
39655
diff
changeset
|
4 |
(* "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *) |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39544
diff
changeset
|
5 |
"Specialisation_Examples", |
|
43916
eabe4d6fbd13
deactivating quickcheck invocation in this example until the Interrupt issue is understood
bulwahn
parents:
43850
diff
changeset
|
6 |
(* "Hotel_Example_Small_Generator",*) |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39544
diff
changeset
|
7 |
"IMP_1", |
|
40137
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
8 |
"IMP_2" |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
9 |
(* "IMP_3", |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
10 |
"IMP_4"*)]; |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39544
diff
changeset
|
11 |
|
|
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
40243
diff
changeset
|
12 |
if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39544
diff
changeset
|
13 |
(warning "No prolog system found - skipping some example theories"; ()) |
|
39544
3a07bbc264b2
replacing temporary hack by checking for environment settings of the component
bulwahn
parents:
39225
diff
changeset
|
14 |
else |
|
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
40243
diff
changeset
|
15 |
if not (getenv "ISABELLE_SWIPL" = "") orelse |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
41952
diff
changeset
|
16 |
#1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
41952
diff
changeset
|
17 |
"5.10.1" |
|
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
40243
diff
changeset
|
18 |
then |
|
40243
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
19 |
(use_thys [ |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
20 |
"Code_Prolog_Examples", |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
21 |
"Context_Free_Grammar_Example", |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
22 |
"Hotel_Example_Prolog", |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
23 |
"Lambda_Example", |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
24 |
"List_Examples"]; |
|
3102b27ca03a
adding a simple check to only run with a SWI-Prolog version known to work
bulwahn
parents:
40137
diff
changeset
|
25 |
Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]) |
|
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
40243
diff
changeset
|
26 |
else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ()); |