Re-organised to perform the tests independently. Now test
is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to
refer to the right command for running the object-logic. Uses "suffix
substitution" to shorten macro definitions.
--- a/Makefile Tue Feb 28 02:02:34 1995 +0100
+++ b/Makefile Tue Feb 28 10:48:46 1995 +0100
@@ -18,50 +18,16 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML HOL.thy HOL.ML simpdata.ML Ord.thy Ord.ML \
- Set.thy Set.ML Fun.thy Fun.ML subset.thy subset.ML \
- equalities.thy equalities.ML thy_syntax.ML \
- Prod.thy Prod.ML Trancl.ML Trancl.thy Sum.thy Sum.ML WF.thy WF.ML \
- mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
- add_ind_def.ML ind_syntax.ML indrule.ML Inductive.ML Inductive.thy \
- intr_elim.ML datatype.ML ../Pure/section_utils.ML\
- Finite.ML Finite.thy\
- Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
- List.thy List.ML \
- ../Provers/classical.ML ../Provers/simplifier.ML \
- ../Provers/splitter.ML ../Provers/ind.ML
-
-IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
- IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy\
- IMP/Properties.thy IMP/Properties.ML
+THYS = HOL.thy Ord.thy Set.thy Fun.thy subset.thy \
+ equalities.thy Prod.thy Trancl.thy Sum.thy WF.thy \
+ mono.thy Lfp.thy Gfp.thy Nat.thy Inductive.thy \
+ Finite.thy Arith.thy Sexp.thy Univ.thy List.thy
-IOA_FILES = IOA/ROOT.ML IOA/example/Action.ML IOA/example/Action.thy\
- IOA/example/Channels.ML IOA/example/Channels.thy\
- IOA/example/Correctness.ML IOA/example/Correctness.thy\
- IOA/example/Impl.ML IOA/example/Impl.thy IOA/example/Lemmas.ML\
- IOA/example/Lemmas.thy IOA/example/Multiset.ML\
- IOA/example/Multiset.thy IOA/example/Packet.thy\
- IOA/example/Receiver.ML IOA/example/Receiver.thy\
- IOA/example/Sender.ML IOA/example/Sender.thy IOA/example/Spec.thy\
- IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.ML\
- IOA/meta_theory/IOA.thy IOA/meta_theory/Option.ML\
- IOA/meta_theory/Option.thy IOA/meta_theory/Solve.ML\
- IOA/meta_theory/Solve.thy
-
-EX_FILES = ex/ROOT.ML ex/cla.ML \
- ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
- ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
- ex/PropLog.ML ex/PropLog.thy ex/Puzzle.ML ex/Puzzle.thy\
- ex/Qsort.thy ex/Qsort.ML ex/LList.thy ex/LList.ML \
- ex/Rec.ML ex/Rec.thy ex/rel.ML ex/set.ML ex/Simult.ML ex/Simult.thy\
- ex/Term.ML ex/Term.thy ex/String.thy ex/String.ML
-
-SUBST_FILES = Subst/ROOT.ML Subst/AList.ML Subst/AList.thy\
- Subst/Setplus.ML Subst/Setplus.thy\
- Subst/Subst.ML Subst/Subst.thy\
- Subst/Unifier.ML Subst/Unifier.thy\
- Subst/UTerm.ML Subst/UTerm.thy\
- Subst/UTLemmas.ML Subst/UTLemmas.thy
+FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
+ ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
+ subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
+ ../Provers/classical.ML ../Provers/simplifier.ML \
+ ../Provers/splitter.ML ../Provers/ind.ML $(THYS) $(THYS:.thy=.ML)
$(BIN)/HOL: $(BIN)/Pure $(FILES)
if [ -d $${ISABELLEBIN:?}/Pure ];\
@@ -75,21 +41,74 @@
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml; exit 1;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-#Directories IMP and Subst also test the system
-#Load ex/ROOT.ML last since it creates the file "test"
-test: $(BIN)/HOL $(IMP_FILES) $(IOA_FILES) $(SUBST_FILES) $(EX_FILES)
- case "$(COMP)" in \
- poly*) echo '(use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"); quit();' \
- | $(COMP) $(BIN)/HOL ;;\
- sml*) echo '(use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/HOL;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+#### Testing of HOL
+
+#A macro referring to the object-logic (depends on ML compiler)
+LOGIC:sh=case $ISABELLECOMP in \
+ poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
+ sml*) echo "$ISABELLEBIN/HOL" ;;\
+ *) echo "echo Bad value for ISABELLECOMP: \
+ $ISABELLEBIN is not poly or sml; exit 1" ;;\
esac
-.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
+##IMP-semantics example
+IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy IMP/Properties.thy
+IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
+
+IMP: $(BIN)/HOL $(IMP_FILES)
+ echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
+
+##The integers in HOL
+INTEG_THYS = Integ/Relation.thy Integ/Equiv.thy Integ/Integ.thy
+
+INTEG_FILES = Integ/ROOT.ML $(INTEG_THYS) $(INTEG_THYS:.thy=.ML)
+
+Integ: $(BIN)/HOL $(INTEG_FILES)
+ echo 'use"Integ/ROOT.ML";quit();' | $(LOGIC)
+
+##I/O Automata
+IOA_THYS = IOA/example/Action.thy IOA/example/Channels.thy\
+ IOA/example/Correctness.thy IOA/example/Impl.thy \
+ IOA/example/Lemmas.thy IOA/example/Multiset.thy \
+ IOA/example/Receiver.thy IOA/example/Sender.thy \
+ IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.thy \
+ IOA/meta_theory/Option.thy IOA/meta_theory/Solve.thy
+
+IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\
+ $(IOA_THYS) $(IOA_THYS:.thy=.ML)
+
+IOA: $(BIN)/HOL $(IOA_FILES)
+ echo 'use"IOA/ROOT.ML";quit();' | $(LOGIC)
+
+##Properties of substitutions
+SUBST_THYS = Subst/AList.thy Subst/Setplus.thy\
+ Subst/Subst.thy Subst/Unifier.thy\
+ Subst/UTerm.thy Subst/UTLemmas.thy
+
+SUBST_FILES = Subst/ROOT.ML $(SUBST_THYS) $(SUBST_THYS:.thy=.ML)
+
+Subst: $(BIN)/HOL $(SUBST_FILES)
+ echo 'use"Subst/ROOT.ML";quit();' | $(LOGIC)
+
+##Miscellaneous examples
+EX_THYS = ex/LexProd.thy ex/MT.thy ex/Acc.thy \
+ ex/PropLog.thy ex/Puzzle.thy ex/Qsort.thy ex/LList.thy \
+ ex/Rec.thy ex/Simult.thy ex/Term.thy ex/String.thy
+
+EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
+ ex/set.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
+
+ex: $(BIN)/HOL $(EX_FILES)
+ echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
+
+#Full test.
+test: $(BIN)/HOL IMP Integ IOA Subst ex
+ echo 'Test examples ran successfully' > test
+
+.PRECIOUS: $(BIN)/Pure $(BIN)/HOL