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
1.1 --- a/Admin/mira.py Sun Mar 27 16:56:16 2011 +0200
1.2 +++ b/Admin/mira.py Sun Mar 27 17:32:25 2011 +0200
1.3 @@ -347,4 +347,4 @@
1.4 @configuration(repos = [Isabelle], deps = [])
1.5 def SML_makeall(*args):
1.6 """Makeall built with SML/NJ"""
1.7 - return isabelle_makeall(*args, more_settings=smlnj_settings, make_options=('-j', '3'))
1.8 + return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
2.1 --- a/src/CCL/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
2.2 +++ b/src/CCL/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
2.3 @@ -8,6 +8,7 @@
2.4 images: CCL
2.5 test: CCL-ex
2.6 all: images test
2.7 +smlnj: all
2.8
2.9
2.10 ## global settings
3.1 --- a/src/CTT/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
3.2 +++ b/src/CTT/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
3.3 @@ -8,6 +8,7 @@
3.4 images: CTT
3.5 test: CTT-ex
3.6 all: images test
3.7 +smlnj: all
3.8
3.9
3.10 ## global settings
4.1 --- a/src/Cube/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
4.2 +++ b/src/Cube/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
4.3 @@ -8,6 +8,7 @@
4.4 images:
4.5 test: Pure-Cube
4.6 all: images test
4.7 +smlnj: all
4.8
4.9
4.10 ## global settings
5.1 --- a/src/FOL/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
5.2 +++ b/src/FOL/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
5.3 @@ -8,6 +8,7 @@
5.4 images: FOL
5.5 test: FOL-ex
5.6 all: images test
5.7 +smlnj: all
5.8
5.9
5.10 ## global settings
6.1 --- a/src/FOLP/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
6.2 +++ b/src/FOLP/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
6.3 @@ -8,6 +8,7 @@
6.4 images: FOLP
6.5 test: FOLP-ex
6.6 all: images test
6.7 +smlnj: all
6.8
6.9
6.10 ## global settings
7.1 --- a/src/HOL/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
7.2 +++ b/src/HOL/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
7.3 @@ -15,7 +15,6 @@
7.4 HOL-Multivariate_Analysis \
7.5 HOL-NSA \
7.6 HOL-Nominal \
7.7 - HOL-Probability \
7.8 HOL-Proofs \
7.9 HOL-SPARK \
7.10 HOL-Word \
7.11 @@ -27,13 +26,11 @@
7.12 HOL-Main \
7.13 HOL-Plain
7.14
7.15 -#Note: keep targets sorted (except for HOL-ex)
7.16 +#Note: keep targets sorted
7.17 test: \
7.18 - HOL-ex \
7.19 HOL-Auth \
7.20 HOL-Bali \
7.21 HOL-Boogie-Examples \
7.22 - HOL-Decision_Procs \
7.23 HOL-Hahn_Banach \
7.24 HOL-Hoare \
7.25 HOL-Hoare_Parallel \
7.26 @@ -62,14 +59,12 @@
7.27 HOL-Mutabelle \
7.28 HOL-NanoJava \
7.29 HOL-Nitpick_Examples \
7.30 - HOL-Nominal-Examples \
7.31 HOL-Number_Theory \
7.32 HOL-Old_Number_Theory \
7.33 HOL-Quotient_Examples \
7.34 HOL-Predicate_Compile_Examples \
7.35 HOL-Prolog \
7.36 HOL-Proofs-ex \
7.37 - HOL-Proofs-Extraction \
7.38 HOL-Proofs-Lambda \
7.39 HOL-SET_Protocol \
7.40 HOL-SPARK-Examples \
7.41 @@ -85,8 +80,17 @@
7.42 HOL-ZF
7.43 # ^ this is the sort position
7.44
7.45 -all: test images
7.46 +images-no-smlnj: \
7.47 + HOL-Probability
7.48
7.49 +test-no-smlnj: \
7.50 + HOL-ex \
7.51 + HOL-Decision_Procs \
7.52 + HOL-Proofs-Extraction \
7.53 + HOL-Nominal-Examples
7.54 +
7.55 +all: test-no-smlnj test images-no-smlnj images
7.56 +smlnj: test images
7.57
7.58 ## global settings
7.59
8.1 --- a/src/LCF/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
8.2 +++ b/src/LCF/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
8.3 @@ -8,6 +8,7 @@
8.4 images: LCF
8.5 test: LCF-ex
8.6 all: images test
8.7 +smlnj: all
8.8
8.9
8.10 ## global settings
9.1 --- a/src/Pure/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
9.2 +++ b/src/Pure/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
9.3 @@ -8,6 +8,7 @@
9.4 images: Pure
9.5 test: RAW
9.6 all: images test
9.7 +smlnj: all
9.8
9.9
9.10 ## global settings
10.1 --- a/src/Sequents/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
10.2 +++ b/src/Sequents/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
10.3 @@ -8,6 +8,7 @@
10.4 images: Sequents
10.5 test: Sequents-LK
10.6 all: images test
10.7 +smlnj: all
10.8
10.9
10.10 ## global settings
11.1 --- a/src/ZF/IsaMakefile Sun Mar 27 16:56:16 2011 +0200
11.2 +++ b/src/ZF/IsaMakefile Sun Mar 27 17:32:25 2011 +0200
11.3 @@ -10,6 +10,7 @@
11.4 #Note: keep targets sorted
11.5 test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
11.6 all: images test
11.7 +smlnj: all
11.8
11.9
11.10 ## global settings