--- a/Admin/mira.py Sun Mar 27 21:19:23 2011 +0200
+++ b/Admin/mira.py Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/CCL/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/CTT/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/Cube/IsaMakefile Sun Mar 27 21:44:10 2011 +0200
@@ -8,6 +8,7 @@
images:
test: Pure-Cube
all: images test
+smlnj: all
## global settings
--- a/src/FOL/IsaMakefile Sun Mar 27 21:19:23 2011 +0200
+++ b/src/FOL/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/FOLP/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/HOL/IsaMakefile Sun Mar 27 21:44:10 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/HOL/Tools/refute.ML Sun Mar 27 21:19:23 2011 +0200
+++ b/src/HOL/Tools/refute.ML Sun Mar 27 21:44:10 2011 +0200
@@ -1136,7 +1136,7 @@
Output.urgent_message "Invoking SAT solver...";
(case solver fm of
SatSolver.SATISFIABLE assignment =>
- (Output.urgent_message ("*** Model found: ***\n" ^ print_model ctxt model
+ (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
(fn i => case assignment i of SOME b => b | NONE => true));
if maybe_spurious then "potential" else "genuine")
| SatSolver.UNSATISFIABLE _ =>
--- a/src/LCF/IsaMakefile Sun Mar 27 21:19:23 2011 +0200
+++ b/src/LCF/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/Pure/IsaMakefile Sun Mar 27 21:44:10 2011 +0200
@@ -8,6 +8,7 @@
images: Pure
test: RAW
all: images test
+smlnj: all
## global settings
--- a/src/Sequents/IsaMakefile Sun Mar 27 21:19:23 2011 +0200
+++ b/src/Sequents/IsaMakefile Sun Mar 27 21:44:10 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 21:19:23 2011 +0200
+++ b/src/ZF/IsaMakefile Sun Mar 27 21:44:10 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