1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
topdir = ../..
ott_coq_lib_dir = $(topdir)/coq
ott_hol_lib_dir = $(topdir)/hol
COQC = coqc
COQDEP = coqdep
COQ_INCLUDE = -I $(ott_coq_lib_dir)
COQC_FLAGS =
DVIPS = dvips
HOLMAKE = Holmake
HOLMAKE_FLAGS = -I $(ott_hol_lib_dir)
ISABELLE = isabelle
ISABELLE_FLAGS = -q
ISABELLE_WRAPPER = use_thy "$*" handle e => (TextIO.output (TextIO.stdErr, "Isabelled failed: " ^ exnMessage e ^ "\n"); OS.Process.exit OS.Process.failure)
LATEX = latex
OTT = $(topdir)/src/ott
OTT_FLAGS = -merge true #-show_defns false -show_sort false
PDFLATEX = pdflatex
# NB THIS SHOULD BE IN SYNC WITH THE SYS_ROUGHLYFULLSIMPLE DEFINITION IN src/Makefile
# AND sys-roughlyfullsimple IN src/regression.otl
SOURCES = \
common.ott \
common_index.ott \
common_labels.ott \
common_typing.ott \
bool.ott \
bool_typing.ott \
nat.ott \
nat_typing.ott \
arrow_typing.ott \
basety.ott \
unit.ott \
seq.ott \
ascribe.ott \
let.ott \
product.ott \
sum.ott \
fix.ott \
tuple.ott \
variant.ott
#record.ott
records_sources = \
common.ott common_index.ott common_labels.ott common_typing.ott \
bool.ott bool_typing.ott \
nat.ott nat_typing.ott \
arrow_typing.ott basety.ott \
unit.ott seq.ott ascribe.ott let.ott \
product.ott sum.ott fix.ott \
tuple.ott record.ott variant.ott
isa_objects = stlc stlc_metatheory
coq_ott_libs = $(ott_coq_lib_dir)/ott_list
coq_stlc_libs = $(coq_ott_libs) stlc_tactics
coq_stlc_objects = $(coq_stlc_libs) \
stlc_auto stlc_base stlc_terms \
stlc_environments stlc_typing stlc_soundness
coq_oldlists_objects = $(coq_stlc_libs) \
records_oldlists_auto
coq_records_common = $(coq_stlc_libs) \
records_auto records_base records_terms records_environments
coq_records_objects = $(coq_records_common) \
records_hand_red records_hand_typing_fl \
records_typing records_soundness
coq_pf_objects = $(coq_records_common) \
records_hand_red records_hand_typing_pf \
records_pf_typing records_pf_soundness
coq_equiv_objects = $(coq_stlc_libs) \
records_auto records_base records_equiv_common \
records_equiv_red records_equiv_typing_fl records_equiv_typing_pf
coq_misc_objects = records_quickies records_tick
default: so
ott: stlc.tex stlc_auto.v stlcScript.sml stlc.thy \
records.tex records_auto.v recordsScript.sml records.thy
coq-stlc: $(coq_stlc_objects:=.vo)
coq-oldlists: $(coq_oldlists_objects:=.vo)
coq-records: $(coq_records_objects:=.vo)
coq-pf: $(coq_pf_objects:=.vo)
coq-equiv: $(coq_equiv_objects:=.vo)
coq-misc: $(coq_misc_objects:=.vo)
coq: coq-pf
coq-world: coq-stlc coq-records coq-pf coq-equiv coq-misc coq-oldlists
hol: metatheoryTheory.uo
isa: $(isa_objects:=.isa)
# N.B. isa currently requires a CVS version of Isabelle (Isabelle 2005 fails)
all: ott stlc.ps coq hol
world: all stlc.pdf coq-world hol isa
#### Scott's targets ####
so: stlcScript.sml metatheoryScript.sml stlc.pdf
$(HOLMAKE) $(HOLMAKE_FLAGS)
#### Tom's targets #####
tom: stlc.thy stlc.pdf
#### ott ###
records.tex records_auto.v recordsScript.sml records.thy: $(records_sources) $(OTT)
$(OTT) $(OTT_FLAGS) -merge true -coq_expand_list_types false -o records.tex -o records_auto.v -o recordsScript.sml -o records.thy $(records_sources)
records_oldlists_auto.v: $(records_sources) $(OTT)
$(OTT) $(OTT_FLAGS) -merge true -coq_expand_list_types true -o $@ $(records_sources)
stlc.tex stlc_auto.v stlcScript.sml stlc.thy: $(SOURCES) $(OTT)
$(OTT) $(OTT_FLAGS) -merge true -coq_expand_list_types true -o stlc.tex -o stlc_auto.v -o stlcScript.sml -o stlc.thy $(SOURCES)
#### TeX ####
.SUFFIXES: .tex .dvi .ps .pdf
.tex.dvi:
$(LATEX) $<
.dvi.ps:
$(DVIPS) -o $@ $<
.tex.pdf:
$(PDFLATEX) $<
#### Hol ####
hol_libs = $(ott_hol_lib_dir)/ottLib $(ott_hol_lib_dir)/ottTheory
hol_libs: $(hol_libs:=.ui) $(hol_libs:=.uo)
$(hol_libs:=.ui) $(hol_libs:=.uo): %:
cd $(@D) && $(MAKE) $(@F)
%Theory.uo: %Script.sml hol_libs
$(HOLMAKE) $(HOLMAKE_FLAGS) $@
#### Isabelle ####
.SUFFIXES: .thy .isa
.thy.isa:
$(ISABELLE) $(ISABELLE_FLAGS) -e '$(ISABELLE_WRAPPER)'
#### Coq ####
coq_libs: $(coq_ott_libs:=.vo)
$(coq_ott_libs:=.vo):
cd $(ott_coq_lib_dir) && $(MAKE) $(@F)
.SUFFIXES: .v .vo
.v.vo:
$(COQC) $(COQ_INCLUDE) $(COQC_FLAGS) $<
#### Administrative targets ####
clean:
rm -f stlc.tex stlcScript.sml auto[-_]* *[-_.]auto[-_.]*
rm -f *.aux *.log *.dvi *.ps *.pdf
rm -f *.vo
rm -f stlcTheory.sig stlcTheory.sml metatheoryTheory.sml metatheoryTheory.sig *.uo *.ui
#### Dependencies ####
dep: .depend
sed -e '/^#### AUTOMATICALLY GENERATED BY make dep, DO NOT CHANGE THIS LINE ####$$/q' <Makefile >Makefile.tmp
cat .depend >>Makefile.tmp
mv -f Makefile .Makefile.old
mv -f Makefile.tmp Makefile
.depend: force
: >.depend.tmp
$(COQDEP) -I . -I $(ott_coq_lib_dir) *.v >.depend.coq.tmp
sed -e '/^_ott_coqrc\.vo:/d' -e 's/ _ott_coqrc\.v/& $$(ott_coqrc_deps)/' <.depend.coq.tmp >>.depend.tmp
rm .depend.coq.tmp
mv .depend.tmp .depend
force:
# TeX dependencies, mentioned so as not to run afoul of the make
# feature whereby it deletes intermediate files.
records.tex:
stlc.tex:
records.dvi:
stlc.dvi:
# ott_coqrc_deps must list the dependencies of _ott_coqrc.vo, because
# coqdep would miss them (see _ott_coqrc.v).
ott_coqrc_deps = $(coq_ott_libs:=.vo)
stlc_coq_prelude = $(ott_coqrc_deps)
# stlc_coq_prelude is used by the regression tests and must depend on
# the .vo files that are required to build any ott-generated stlc .v.
stlc_coq_prelude: $(stlc_coq_prelude)
#### AUTOMATICALLY GENERATED BY make dep, DO NOT CHANGE THIS LINE ####
records_auto.vo: records_auto.v ../../coq/ott_list.vo _ott_coqrc.v $(ott_coqrc_deps) ../../coq/ott_list_flat_map.vo
records_base.vo: records_base.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo
records_environments.vo: records_environments.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo
records_equiv_common.vo: records_equiv_common.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo
records_equiv_red.vo: records_equiv_red.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_equiv_common.vo records_hand_red.vo
records_equiv_typing_fl.vo: records_equiv_typing_fl.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_equiv_common.vo records_hand_typing_fl.vo
records_equiv_typing_pf.vo: records_equiv_typing_pf.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_hand_typing_fl.vo records_hand_typing_pf.vo
records_hand_red.vo: records_hand_red.v _ott_coqrc.v $(ott_coqrc_deps) records_auto.vo records_base.vo
records_hand_typing_fl.vo: records_hand_typing_fl.v _ott_coqrc.v $(ott_coqrc_deps) records_auto.vo records_base.vo
records_hand_typing_pf.vo: records_hand_typing_pf.v _ott_coqrc.v $(ott_coqrc_deps) records_auto.vo records_base.vo
records_oldlists_auto.vo: records_oldlists_auto.v _ott_coqrc.v $(ott_coqrc_deps) ../../coq/ott_list_flat_map.vo
records_pf_soundness.vo: records_pf_soundness.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_terms.vo records_environments.vo records_hand_red.vo records_hand_typing_pf.vo records_pf_typing.vo
records_pf_typing.vo: records_pf_typing.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_terms.vo records_environments.vo records_hand_typing_pf.vo
records_quickies.vo: records_quickies.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_environments.vo records_hand_red.vo records_hand_typing_pf.vo
records_run.vo: records_run.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_terms.vo records_environments.vo records_hand_red.vo records_hand_typing_pf.vo
records_soundness.vo: records_soundness.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_terms.vo records_environments.vo records_hand_red.vo records_hand_typing_fl.vo records_typing.vo
records_terms.vo: records_terms.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo
records_tick.vo: records_tick.v _ott_coqrc.v $(ott_coqrc_deps) records_auto.vo records_base.vo records_pf_soundness.vo records_hand_red.vo records_hand_typing_pf.vo records_equiv_red.vo records_equiv_typing_pf.vo records_equiv_typing_fl.vo
records_typing.vo: records_typing.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo records_auto.vo records_base.vo records_terms.vo records_environments.vo records_hand_typing_fl.vo
stlc_auto.vo: stlc_auto.v _ott_coqrc.v $(ott_coqrc_deps) ../../coq/ott_list_flat_map.vo
stlc_base.vo: stlc_base.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo stlc_auto.vo
stlc_environments.vo: stlc_environments.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo stlc_auto.vo stlc_base.vo
stlc_soundness.vo: stlc_soundness.v _ott_coqrc.v $(ott_coqrc_deps) stlc_auto.vo stlc_tactics.vo stlc_base.vo stlc_terms.vo stlc_environments.vo stlc_typing.vo
stlc_tactics.vo: stlc_tactics.v
stlc_terms.vo: stlc_terms.v _ott_coqrc.v $(ott_coqrc_deps) stlc_tactics.vo stlc_auto.vo stlc_base.vo
stlc_typing.vo: stlc_typing.v _ott_coqrc.v $(ott_coqrc_deps) stlc_auto.vo stlc_tactics.vo stlc_base.vo stlc_terms.vo stlc_environments.vo
wet_massaged.vo: wet_massaged.v
|
