src/HOLCF/IsaMakefile
author wenzelm
Wed Jan 08 15:12:44 1997 +0100 (1997-01-08)
changeset 2494 5d45c2094ff6
child 2571 b9f641195b48
permissions -rw-r--r--
IsaMakefile for HOLCF;
wenzelm@2494
     1
#
wenzelm@2494
     2
# $Id$
wenzelm@2494
     3
#
wenzelm@2494
     4
# IsaMakefile for HOLCF
wenzelm@2494
     5
#
wenzelm@2494
     6
wenzelm@2494
     7
#### Base system
wenzelm@2494
     8
wenzelm@2494
     9
OUT = $(ISABELLE_OUTPUT_DIR)
wenzelm@2494
    10
wenzelm@2494
    11
THYS = Void.thy Porder.thy Pcpo.thy \
wenzelm@2494
    12
       Fun1.thy Fun2.thy Fun3.thy \
wenzelm@2494
    13
       Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
wenzelm@2494
    14
       Cprod1.thy Cprod2.thy Cprod3.thy \
wenzelm@2494
    15
       Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
wenzelm@2494
    16
       Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
wenzelm@2494
    17
       Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
wenzelm@2494
    18
       Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy
wenzelm@2494
    19
wenzelm@2494
    20
FILES = ROOT.ML Porder0.thy  $(THYS) $(THYS:.thy=.ML)
wenzelm@2494
    21
wenzelm@2494
    22
$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
wenzelm@2494
    23
	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
wenzelm@2494
    24
	@chmod -w $@
wenzelm@2494
    25
wenzelm@2494
    26
$(OUT)/HOL:
wenzelm@2494
    27
	@cd ../HOL; $(ISATOOL) make
wenzelm@2494
    28
wenzelm@2494
    29
wenzelm@2494
    30
wenzelm@2494
    31
#### Tests and examples
wenzelm@2494
    32
wenzelm@2494
    33
## Miscellaneous examples
wenzelm@2494
    34
wenzelm@2494
    35
EX_THYS = ex/Fix2.thy ex/Hoare.thy \
wenzelm@2494
    36
	  ex/Loop.thy
wenzelm@2494
    37
wenzelm@2494
    38
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
wenzelm@2494
    39
wenzelm@2494
    40
test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
wenzelm@2494
    41
	@$(ISATOOL) testdir $(OUT)/HOLCF ex
wenzelm@2494
    42
wenzelm@2494
    43
wenzelm@2494
    44
## Explicit domains
wenzelm@2494
    45
wenzelm@2494
    46
EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
wenzelm@2494
    47
			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
wenzelm@2494
    48
			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \
wenzelm@2494
    49
			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
wenzelm@2494
    50
wenzelm@2494
    51
EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
wenzelm@2494
    52
			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
wenzelm@2494
    53
wenzelm@2494
    54
test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
wenzelm@2494
    55
	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
wenzelm@2494
    56
wenzelm@2494
    57
wenzelm@2494
    58
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF