src/HOL/IsaMakefile
author wenzelm
Wed Dec 18 15:56:58 1996 +0100 (1996-12-18 ago)
changeset 2448 61337170db84
child 2473 3eb12c85846c
permissions -rw-r--r--
IsaMakefile for HOL;
wenzelm@2448
     1
#
wenzelm@2448
     2
# $Id$
wenzelm@2448
     3
#
wenzelm@2448
     4
# IsaMakefile for HOL
wenzelm@2448
     5
#
wenzelm@2448
     6
wenzelm@2448
     7
#### Base system
wenzelm@2448
     8
wenzelm@2448
     9
OUT = $(ISABELLE_OUTPUT_DIR)
wenzelm@2448
    10
wenzelm@2448
    11
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
wenzelm@2448
    12
	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
wenzelm@2448
    13
	Sexp Univ List RelPow Option
wenzelm@2448
    14
wenzelm@2448
    15
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
wenzelm@2448
    16
	ind_syntax.ML cladata.ML simpdata.ML \
wenzelm@2448
    17
	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
wenzelm@2448
    18
	../Provers/hypsubst.ML ../Provers/classical.ML \
wenzelm@2448
    19
	../Provers/simplifier.ML ../Provers/splitter.ML \
wenzelm@2448
    20
	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
wenzelm@2448
    21
wenzelm@2448
    22
$(OUT)/HOL: $(OUT)/Pure $(FILES)
wenzelm@2448
    23
	@$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -qu Pure HOL
wenzelm@2448
    24
	@chmod -w $@
wenzelm@2448
    25
wenzelm@2448
    26
$(OUT)/Pure:
wenzelm@2448
    27
	@cd ../Pure; $(ISABELLE_HOME)/bin/isatool make
wenzelm@2448
    28
wenzelm@2448
    29
wenzelm@2448
    30
wenzelm@2448
    31
#### Tests and examples
wenzelm@2448
    32
wenzelm@2448
    33
ISABELLE=$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -rq
wenzelm@2448
    34
wenzelm@2448
    35
wenzelm@2448
    36
## TFL (requires integration into HOL proper)
wenzelm@2448
    37
wenzelm@2448
    38
TFL_NAMES = mask tfl thms thry usyntax utils
wenzelm@2448
    39
TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
wenzelm@2448
    40
            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
wenzelm@2448
    41
wenzelm@2448
    42
TFL:	$(OUT)/HOL $(TFL_FILES)
wenzelm@2448
    43
	$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL
wenzelm@2448
    44
wenzelm@2448
    45
wenzelm@2448
    46
## IMP-semantics example
wenzelm@2448
    47
wenzelm@2448
    48
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
wenzelm@2448
    49
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
wenzelm@2448
    50
wenzelm@2448
    51
IMP:	$(OUT)/HOL $(IMP_FILES)
wenzelm@2448
    52
	$(ISABELLE) -e 'exit_use_dir"IMP"; quit();' HOL
wenzelm@2448
    53
wenzelm@2448
    54
wenzelm@2448
    55
## Hoare logic
wenzelm@2448
    56
wenzelm@2448
    57
Hoare_NAMES = Hoare Arith2 Examples
wenzelm@2448
    58
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
wenzelm@2448
    59
	      $(Hoare_NAMES:%=Hoare/%.ML)
wenzelm@2448
    60
wenzelm@2448
    61
Hoare:	$(OUT)/HOL $(Hoare_FILES)
wenzelm@2448
    62
	$(ISABELLE) -e 'exit_use_dir"Hoare"; quit();' HOL
wenzelm@2448
    63
wenzelm@2448
    64
wenzelm@2448
    65
## The integers in HOL
wenzelm@2448
    66
wenzelm@2448
    67
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
wenzelm@2448
    68
wenzelm@2448
    69
INTEG_FILES = Integ/ROOT.ML \
wenzelm@2448
    70
	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
wenzelm@2448
    71
wenzelm@2448
    72
Integ:	$(OUT)/HOL $(INTEG_FILES)
wenzelm@2448
    73
	$(ISABELLE) -e 'exit_use_dir"Integ"; quit();' HOL
wenzelm@2448
    74
wenzelm@2448
    75
wenzelm@2448
    76
## I/O Automata
wenzelm@2448
    77
wenzelm@2448
    78
IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
wenzelm@2448
    79
		Receiver Sender
wenzelm@2448
    80
IOA_ABP_NAMES = Action Correctness Lemmas
wenzelm@2448
    81
IOA_MT_NAMES = Asig IOA Solve
wenzelm@2448
    82
wenzelm@2448
    83
IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
wenzelm@2448
    84
 $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
wenzelm@2448
    85
 IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
wenzelm@2448
    86
 IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
wenzelm@2448
    87
 IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
wenzelm@2448
    88
 $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
wenzelm@2448
    89
 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
wenzelm@2448
    90
wenzelm@2448
    91
IOA:	$(OUT)/HOL $(IOA_FILES)
wenzelm@2448
    92
	$(ISABELLE) -e 'exit_use_dir"IOA/NTP"; quit();' HOL
wenzelm@2448
    93
	$(ISABELLE) -e 'exit_use_dir"IOA/ABP"; quit();' HOL
wenzelm@2448
    94
wenzelm@2448
    95
wenzelm@2448
    96
## Authentication & Security Protocols
wenzelm@2448
    97
wenzelm@2448
    98
Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
wenzelm@2448
    99
	     WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
wenzelm@2448
   100
wenzelm@2448
   101
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
wenzelm@2448
   102
wenzelm@2448
   103
Auth:	$(OUT)/HOL $(AUTH_FILES)
wenzelm@2448
   104
	$(ISABELLE) -e 'exit_use_dir"Auth"; quit();' HOL
wenzelm@2448
   105
wenzelm@2448
   106
wenzelm@2448
   107
## Properties of substitutions
wenzelm@2448
   108
wenzelm@2448
   109
SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
wenzelm@2448
   110
wenzelm@2448
   111
SUBST_FILES = Subst/ROOT.ML \
wenzelm@2448
   112
	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
wenzelm@2448
   113
wenzelm@2448
   114
Subst:	$(OUT)/HOL $(SUBST_FILES)
wenzelm@2448
   115
	$(ISABELLE) -e 'exit_use_dir"Subst"; quit();' HOL
wenzelm@2448
   116
wenzelm@2448
   117
wenzelm@2448
   118
## Confluence of Lambda-calculus
wenzelm@2448
   119
wenzelm@2448
   120
LAMBDA_NAMES = Lambda ParRed Commutation Eta
wenzelm@2448
   121
wenzelm@2448
   122
LAMBDA_FILES = Lambda/ROOT.ML \
wenzelm@2448
   123
	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
wenzelm@2448
   124
wenzelm@2448
   125
Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
wenzelm@2448
   126
	$(ISABELLE) -e 'exit_use_dir"Lambda"; quit();' HOL
wenzelm@2448
   127
wenzelm@2448
   128
wenzelm@2448
   129
## Type inference for MiniML
wenzelm@2448
   130
wenzelm@2448
   131
MINIML_NAMES = I Maybe MiniML Type W
wenzelm@2448
   132
wenzelm@2448
   133
MINIML_FILES = MiniML/ROOT.ML \
wenzelm@2448
   134
	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
wenzelm@2448
   135
wenzelm@2448
   136
MiniML: $(OUT)/HOL $(MINIML_FILES)
wenzelm@2448
   137
	$(ISABELLE) -e 'exit_use_dir"MiniML"; quit();' HOL
wenzelm@2448
   138
wenzelm@2448
   139
wenzelm@2448
   140
## Lexical analysis
wenzelm@2448
   141
wenzelm@2448
   142
LEX_FILES = Auto AutoChopper Chopper Prefix
wenzelm@2448
   143
wenzelm@2448
   144
LEX_FILES = Lex/ROOT.ML \
wenzelm@2448
   145
	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
wenzelm@2448
   146
wenzelm@2448
   147
Lex:	$(OUT)/HOL $(LEX_FILES)
wenzelm@2448
   148
	$(ISABELLE) -e 'exit_use_dir"Lex"; quit();' HOL
wenzelm@2448
   149
wenzelm@2448
   150
wenzelm@2448
   151
## Miscellaneous examples
wenzelm@2448
   152
wenzelm@2448
   153
EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
wenzelm@2448
   154
	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
wenzelm@2448
   155
wenzelm@2448
   156
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
wenzelm@2448
   157
	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
wenzelm@2448
   158
wenzelm@2448
   159
ex:	$(OUT)/HOL $(EX_FILES)
wenzelm@2448
   160
	$(ISABELLE) -e 'exit_use_dir"ex"; quit();' HOL
wenzelm@2448
   161
wenzelm@2448
   162
wenzelm@2448
   163
## Full test
wenzelm@2448
   164
wenzelm@2448
   165
test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
wenzelm@2448
   166
	echo 'Test examples ran successfully' > test
wenzelm@2448
   167
wenzelm@2448
   168
wenzelm@2448
   169
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL