blob: c297829c2ba24f116ce5492becd3ef3f8d286d09 (
plain)
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
|
#OTT=../../../rsem/ott/bin/ott
# this is the binary that gets rebuilt by make in ott/src:
OTT=../../../github/ott/src/ott
OTTLIB=$(dir $(shell which ott))../hol
.PHONY: all
all: l2.ml l2_parse.ml l2.lem
docs: l2.pdf l2_parse.pdf
%.pdf: %.tex
pdflatex $<
%Theory.uo: %Script.sml
Holmake --qof -I $(OTTLIB) $@
type_system.pdf: doc_in.tex type_system.tex
pdflatex type_system.tex
pdflatex type_system.tex
l2.tex: l2.ott l2_typ.ott l2_rules.ott
$(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
doc_in.tex: l2.ott primitive_doc.ott l2_typ.ott l2_rules.ott
$(OTT) -sort false -generate_aux_rules false -tex_wrap false -o $@ -picky_multiple_parses true $^
%.tex: %.ott
$(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
%.ml: %.ott
$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
%Script.sml: %.ott
$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
l2.lem: l2.ott l2_typ.ott
$(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
clean:
rm -rf *~
rm -rf *.uo *.ui *.sig *.sml .HOLMK
rm -f *.aux *.log *.dvi *.ps *.pdf *.toc
rm -rf l2.pdf l2_parse.pdf
rm -rf l2.tex doc_in.tex
realclean:
$(MAKE) clean
rm -rf l2.ml l2_parse.ml l2.lem
|
