Now target "test" builds and tests TFL
authorpaulson
Tue Dec 10 15:08:57 1996 +0100 (1996-12-10)
changeset 2371c5dc6f8b385b
parent 2370 5f9607d293f5
child 2372 a2999e19703b
Now target "test" builds and tests TFL
src/HOL/Makefile
     1.1 --- a/src/HOL/Makefile	Tue Dec 10 15:07:43 1996 +0100
     1.2 +++ b/src/HOL/Makefile	Tue Dec 10 15:08:57 1996 +0100
     1.3 @@ -76,6 +76,17 @@
     1.4  			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
     1.5  	esac`
     1.6  
     1.7 +##TFL (requires integration into HOL proper)
     1.8 +TFL_NAMES = mask tfl thms thry usyntax utils
     1.9 +TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
    1.10 +            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
    1.11 +
    1.12 +TFL:	$(BIN)/HOL  $(TFL_FILES)
    1.13 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.14 +	then echo 'make_html:= true; exit_use_dir"../TFL";quit();' | $(LOGIC);\
    1.15 +	else echo 'exit_use_dir"../TFL";quit();' | $(LOGIC); \
    1.16 +	fi
    1.17 +
    1.18  ##IMP-semantics example
    1.19  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.20  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.21 @@ -211,7 +222,7 @@
    1.22  	fi
    1.23  
    1.24  #Full test.
    1.25 -test:	$(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
    1.26 +test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
    1.27  	echo 'Test examples ran successfully' > test
    1.28  
    1.29  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL