author  bulwahn 
Thu, 21 Jul 2011 08:33:57 +0200  
changeset 43938  78a0a2ad91a3 
parent 43916  eabe4d6fbd13 
permissions  rwrr 
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 *) 
43938
78a0a2ad91a3
deactivating all quickcheck invocations until parallel invocation works safely
bulwahn
parents:
43916
diff
changeset

5 
"Specialisation_Examples" 
78a0a2ad91a3
deactivating all quickcheck invocations until parallel invocation works safely
bulwahn
parents:
43916
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" 
43938
78a0a2ad91a3
deactivating all quickcheck invocations until parallel invocation works safely
bulwahn
parents:
43916
diff
changeset

9 
"IMP_3", 
40137
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 SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

19 
(use_thys [ 
3102b27ca03a
adding a simple check to only run with a SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

20 
"Code_Prolog_Examples", 
3102b27ca03a
adding a simple check to only run with a SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

21 
"Context_Free_Grammar_Example", 
3102b27ca03a
adding a simple check to only run with a SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

22 
"Hotel_Example_Prolog", 
3102b27ca03a
adding a simple check to only run with a SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

23 
"Lambda_Example", 
3102b27ca03a
adding a simple check to only run with a SWIProlog version known to work
bulwahn
parents:
40137
diff
changeset

24 
"List_Examples"]; 
3102b27ca03a
adding a simple check to only run with a SWIProlog 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 SWIProlog version  skipping some example theories"; ()); 