#
# $Id$
#
# IsaMakefile for HOLCF
#
#### Base system
OUT = $(ISABELLE_OUTPUT_DIR)
THYS = Porder.thy Porder0.thy Pcpo.thy \
Fun1.thy Fun2.thy Fun3.thy \
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
Cprod1.thy Cprod2.thy Cprod3.thy \
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
One.thy Tr.thy\
Discrete0.thy Discrete1.thy Discrete.thy\
Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
ONLYTHYS = Lift.thy
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
@$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF
@chmod -w $@
$(OUT)/HOL:
@cd ../HOL; $(ISATOOL) make
#### Tests and examples
## IMP
IMP_THYS = IMP/Denotational.thy
IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
IMP: $(OUT)/HOLCF $(IMP_FILES)
@$(ISATOOL) usedir $(OUT)/HOLCF IMP
## Miscellaneous examples
EX_THYS = ex/Classlib.thy ex/Witness.thy\
ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
ex/Hoare.thy ex/Loop.thy
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
EX: ex/ROOT.ML $(EX_FILES)
@$(ISATOOL) usedir $(OUT)/HOLCF ex
## Full test
test: $(OUT)/HOLCF IMP EX
echo 'Test examples ran successfully' > test
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF