src/HOL/IsaMakefile
author wenzelm
Tue May 06 15:27:35 1997 +0200 (1997-05-06)
changeset 3118 24dae6222579
parent 3079 2ea678d3523f
child 3125 3f0ab2c306f7
permissions -rw-r--r--
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
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@3118
     9
OUT = $(ISABELLE_OUTPUT)
wenzelm@2448
    10
wenzelm@2448
    11
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
nipkow@3025
    12
	mono Lfp Gfp NatDef 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 \
paulson@2889
    18
	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
wenzelm@2448
    19
	../Provers/simplifier.ML ../Provers/splitter.ML \
nipkow@2919
    20
	../Provers/nat_transitive.ML \
wenzelm@2448
    21
	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
wenzelm@2448
    22
wenzelm@2448
    23
$(OUT)/HOL: $(OUT)/Pure $(FILES)
wenzelm@2826
    24
	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
wenzelm@2448
    25
	@chmod -w $@
wenzelm@2448
    26
wenzelm@2448
    27
$(OUT)/Pure:
wenzelm@2473
    28
	@cd ../Pure; $(ISATOOL) make
wenzelm@2448
    29
wenzelm@2448
    30
wenzelm@2448
    31
## TFL (requires integration into HOL proper)
wenzelm@2448
    32
wenzelm@2448
    33
TFL_NAMES = mask tfl thms thry usyntax utils
wenzelm@2448
    34
TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
wenzelm@2448
    35
            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
wenzelm@2448
    36
wenzelm@2448
    37
TFL:	$(OUT)/HOL $(TFL_FILES)
wenzelm@2607
    38
	@$(ISABELLE) -qe 'exit_use_dir"../TFL"; quit();' HOL
wenzelm@2473
    39
wenzelm@2448
    40
wenzelm@2448
    41
wenzelm@2473
    42
#### Tests and examples
wenzelm@2473
    43
wenzelm@2448
    44
## IMP-semantics example
wenzelm@2448
    45
wenzelm@2448
    46
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
wenzelm@2448
    47
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
wenzelm@2448
    48
wenzelm@2448
    49
IMP:	$(OUT)/HOL $(IMP_FILES)
wenzelm@2826
    50
	@$(ISATOOL) usedir $(OUT)/HOL IMP
wenzelm@2448
    51
wenzelm@2448
    52
wenzelm@2448
    53
## Hoare logic
wenzelm@2448
    54
wenzelm@2448
    55
Hoare_NAMES = Hoare Arith2 Examples
wenzelm@2448
    56
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
wenzelm@2448
    57
	      $(Hoare_NAMES:%=Hoare/%.ML)
wenzelm@2448
    58
wenzelm@2448
    59
Hoare:	$(OUT)/HOL $(Hoare_FILES)
wenzelm@2826
    60
	@$(ISATOOL) usedir $(OUT)/HOL Hoare
wenzelm@2448
    61
wenzelm@2448
    62
wenzelm@2448
    63
## The integers in HOL
wenzelm@2448
    64
wenzelm@2448
    65
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
wenzelm@2448
    66
wenzelm@2448
    67
INTEG_FILES = Integ/ROOT.ML \
wenzelm@2448
    68
	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
wenzelm@2448
    69
wenzelm@2448
    70
Integ:	$(OUT)/HOL $(INTEG_FILES)
wenzelm@2826
    71
	@$(ISATOOL) usedir $(OUT)/HOL Integ
wenzelm@2448
    72
wenzelm@2448
    73
mueller@3079
    74
## I/O Automata (meta theory only)
wenzelm@2448
    75
wenzelm@2448
    76
mueller@3079
    77
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
mueller@3079
    78
  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
wenzelm@2448
    79
mueller@3079
    80
IOA: $(OUT)/HOL $(IOA_FILES)
mueller@3079
    81
	@$(ISATOOL) usedir $(OUT)/HOL IOA
wenzelm@2448
    82
wenzelm@2448
    83
wenzelm@2448
    84
## Authentication & Security Protocols
wenzelm@2448
    85
wenzelm@2448
    86
Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
wenzelm@2473
    87
	     Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
wenzelm@2448
    88
wenzelm@2448
    89
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
wenzelm@2448
    90
wenzelm@2448
    91
Auth:	$(OUT)/HOL $(AUTH_FILES)
wenzelm@2826
    92
	@$(ISATOOL) usedir $(OUT)/HOL Auth
wenzelm@2448
    93
wenzelm@2448
    94
wenzelm@2448
    95
## Properties of substitutions
wenzelm@2448
    96
wenzelm@2448
    97
SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
wenzelm@2448
    98
wenzelm@2448
    99
SUBST_FILES = Subst/ROOT.ML \
wenzelm@2448
   100
	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
wenzelm@2448
   101
wenzelm@2448
   102
Subst:	$(OUT)/HOL $(SUBST_FILES)
wenzelm@2826
   103
	@$(ISATOOL) usedir $(OUT)/HOL Subst
wenzelm@2448
   104
wenzelm@2448
   105
wenzelm@2448
   106
## Confluence of Lambda-calculus
wenzelm@2448
   107
wenzelm@2448
   108
LAMBDA_NAMES = Lambda ParRed Commutation Eta
wenzelm@2448
   109
wenzelm@2448
   110
LAMBDA_FILES = Lambda/ROOT.ML \
wenzelm@2448
   111
	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
wenzelm@2448
   112
wenzelm@2448
   113
Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
wenzelm@2826
   114
	@$(ISATOOL) usedir $(OUT)/HOL Lambda
wenzelm@2448
   115
wenzelm@2448
   116
nipkow@2527
   117
## Type inference without let
nipkow@2527
   118
nipkow@2527
   119
W0_NAMES = I Maybe MiniML Type W
nipkow@2527
   120
nipkow@2527
   121
W0_FILES = W0/ROOT.ML \
nipkow@2527
   122
	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
wenzelm@2448
   123
nipkow@2527
   124
W0: $(OUT)/HOL $(W0_FILES)
wenzelm@2826
   125
	@$(ISATOOL) usedir $(OUT)/HOL W0
nipkow@2527
   126
nipkow@2527
   127
nipkow@2527
   128
## Type inference with let
nipkow@2527
   129
nipkow@2527
   130
MINIML_NAMES = Generalize Instance Maybe MiniML Type W
wenzelm@2448
   131
wenzelm@2448
   132
MINIML_FILES = MiniML/ROOT.ML \
wenzelm@2448
   133
	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
wenzelm@2448
   134
wenzelm@2448
   135
MiniML: $(OUT)/HOL $(MINIML_FILES)
wenzelm@2826
   136
	@$(ISATOOL) usedir $(OUT)/HOL MiniML
wenzelm@2448
   137
wenzelm@2448
   138
wenzelm@2448
   139
## Lexical analysis
wenzelm@2448
   140
wenzelm@2448
   141
LEX_FILES = Auto AutoChopper Chopper Prefix
wenzelm@2448
   142
wenzelm@2448
   143
LEX_FILES = Lex/ROOT.ML \
wenzelm@2448
   144
	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
wenzelm@2448
   145
wenzelm@2448
   146
Lex:	$(OUT)/HOL $(LEX_FILES)
wenzelm@2826
   147
	@$(ISATOOL) usedir $(OUT)/HOL Lex
wenzelm@2448
   148
wenzelm@2448
   149
wenzelm@2545
   150
## Axiomatic type classes examples
wenzelm@2545
   151
wenzelm@2545
   152
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
wenzelm@2545
   153
	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
wenzelm@2545
   154
wenzelm@2545
   155
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
wenzelm@2545
   156
	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
wenzelm@2545
   157
	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
wenzelm@2545
   158
	Order.ML Order.thy ROOT.ML tools.ML
wenzelm@2545
   159
wenzelm@2545
   160
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
wenzelm@2545
   161
	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
wenzelm@2545
   162
	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
wenzelm@2545
   163
	Xor.ML Xor.thy
wenzelm@2545
   164
wenzelm@2545
   165
AXCLASSES_FILES = AxClasses/ROOT.ML \
wenzelm@2545
   166
	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
wenzelm@2545
   167
	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
wenzelm@2545
   168
	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
wenzelm@2545
   169
wenzelm@2545
   170
AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
wenzelm@2826
   171
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
wenzelm@2827
   172
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
wenzelm@2827
   173
	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
wenzelm@2827
   174
	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
wenzelm@2545
   175
wenzelm@2545
   176
slotosch@2909
   177
## Higher-order quotients and example fractionals
wenzelm@2900
   178
slotosch@2909
   179
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
slotosch@2909
   180
	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
slotosch@2909
   181
	Quot/FRACT.thy Quot/FRACT.ML
wenzelm@2900
   182
Quot:	$(OUT)/HOL $(QUOT_FILES)
wenzelm@2900
   183
	@$(ISATOOL) usedir $(OUT)/HOL Quot
wenzelm@2900
   184
wenzelm@2900
   185
wenzelm@2448
   186
## Miscellaneous examples
wenzelm@2448
   187
paulson@2982
   188
EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
paulson@2982
   189
	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
wenzelm@2448
   190
wenzelm@2448
   191
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
wenzelm@2448
   192
	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
wenzelm@2448
   193
wenzelm@2448
   194
ex:	$(OUT)/HOL $(EX_FILES)
wenzelm@2826
   195
	@$(ISATOOL) usedir $(OUT)/HOL ex
wenzelm@2448
   196
wenzelm@2448
   197
wenzelm@2448
   198
## Full test
wenzelm@2448
   199
oheimb@2635
   200
test:	$(OUT)/HOL \
wenzelm@2900
   201
	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
wenzelm@2448
   202
	echo 'Test examples ran successfully' > test
wenzelm@2448
   203
wenzelm@2448
   204
wenzelm@2448
   205
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL