added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
authorkrauss
Sun, 27 Mar 2011 17:32:25 +0200
changeset 42138 e54a985daa61
parent 42137 6803f2fd15c1
child 42139 f667e64a5b4d
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall
Admin/mira.py
src/CCL/IsaMakefile
src/CTT/IsaMakefile
src/Cube/IsaMakefile
src/FOL/IsaMakefile
src/FOLP/IsaMakefile
src/HOL/IsaMakefile
src/LCF/IsaMakefile
src/Pure/IsaMakefile
src/Sequents/IsaMakefile
src/ZF/IsaMakefile
--- a/Admin/mira.py	Sun Mar 27 16:56:16 2011 +0200
+++ b/Admin/mira.py	Sun Mar 27 17:32:25 2011 +0200
@@ -347,4 +347,4 @@
 @configuration(repos = [Isabelle], deps = [])
 def SML_makeall(*args):
     """Makeall built with SML/NJ"""
-    return isabelle_makeall(*args, more_settings=smlnj_settings, make_options=('-j', '3'))
+    return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
--- a/src/CCL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/CCL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: CCL
 test: CCL-ex
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/CTT/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/CTT/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: CTT
 test: CTT-ex
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/Cube/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Cube/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images:
 test: Pure-Cube
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/FOL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/FOL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: FOL
 test: FOL-ex
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/FOLP/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/FOLP/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: FOLP
 test: FOLP-ex
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/HOL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/HOL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -15,7 +15,6 @@
   HOL-Multivariate_Analysis \
   HOL-NSA \
   HOL-Nominal \
-  HOL-Probability \
   HOL-Proofs \
   HOL-SPARK \
   HOL-Word \
@@ -27,13 +26,11 @@
   HOL-Main \
   HOL-Plain
 
-#Note: keep targets sorted (except for HOL-ex)
+#Note: keep targets sorted
 test: \
-  HOL-ex \
   HOL-Auth \
   HOL-Bali \
   HOL-Boogie-Examples \
-  HOL-Decision_Procs \
   HOL-Hahn_Banach \
   HOL-Hoare \
   HOL-Hoare_Parallel \
@@ -62,14 +59,12 @@
   HOL-Mutabelle \
   HOL-NanoJava \
   HOL-Nitpick_Examples \
-  HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Quotient_Examples \
   HOL-Predicate_Compile_Examples \
   HOL-Prolog \
   HOL-Proofs-ex \
-  HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
   HOL-SET_Protocol \
   HOL-SPARK-Examples \
@@ -85,8 +80,17 @@
   HOL-ZF
     # ^ this is the sort position
 
-all: test images
+images-no-smlnj: \
+  HOL-Probability
 
+test-no-smlnj: \
+  HOL-ex \
+  HOL-Decision_Procs \
+  HOL-Proofs-Extraction \
+  HOL-Nominal-Examples
+
+all: test-no-smlnj test images-no-smlnj images
+smlnj: test images
 
 ## global settings
 
--- a/src/LCF/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/LCF/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: LCF
 test: LCF-ex
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/Pure/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Pure/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: Pure
 test: RAW
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/Sequents/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Sequents/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: Sequents
 test: Sequents-LK
 all: images test
+smlnj: all
 
 
 ## global settings
--- a/src/ZF/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/ZF/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -10,6 +10,7 @@
 #Note: keep targets sorted
 test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
 all: images test
+smlnj: all
 
 
 ## global settings