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 43002e54a985daa61
parent 43001 6803f2fd15c1
child 43010 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
     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