-
Notifications
You must be signed in to change notification settings - Fork 131
/
Holmakefile
65 lines (48 loc) · 1.99 KB
/
Holmakefile
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
INCLUDES = ../Tools ../../examples/probability $(HOLDIR)/src/integer
TEX_CORES = description title preface system conv drules tactics \
theories math definitions libraries misc HolSat PatternMatchesLib \
enumfset simplifier latex-munger
TEX_SOURCES = ../LaTeX/ack.tex ../LaTeX/commands.tex $(patsubst %,%.tex,$(TEX_CORES))
PS_STUFF = ../Tools/polyscripter ../Tools/umap
PS_COMMAND = $(PS_STUFF) < $< > $@
description.pdf: $(TEX_SOURCES)
latexmk -pdf description
definitions.tex: definitions.stex $(PS_STUFF)
$(PS_COMMAND)
conv.tex: conv.stex $(PS_STUFF)
$(PS_COMMAND)
drules.tex: drules.stex $(PS_STUFF)
$(PS_COMMAND)
tactics.tex: tactics.stex $(PS_STUFF)
$(PS_COMMAND)
theories.tex: theories.stex $(PS_STUFF) $(dprot $(SIGOBJ)/realTheory.uo) \
$(dprot $(HOLDIR)/src/integer/integerTheory.uo) \
$(dprot $(SIGOBJ)/real_sigmaTheory.uo) \
$(dprot $(SIGOBJ)/iterateTheory.uo)
$(PS_COMMAND)
math.tex: math.stex $(PS_STUFF) $(dprot $(SIGOBJ)/probabilityTheory.uo) \
$(HOLDIR)/examples/probability/large_numberTheory.uo \
$(HOLDIR)/examples/probability/lebesgue_measureTheory.uo
$(PS_COMMAND)
simplifier.tex: simplifier.stex $(PS_STUFF)
$(PS_COMMAND)
PatternMatchesLib.tex: PatternMatchesLib.stex $(PS_STUFF)
$(PS_COMMAND)
libraries.tex: libraries.stex $(PS_STUFF) $(dprot $(SIGOBJ)/integerTheory.uo)
$(PS_COMMAND)
system.tex: system.stex $(PS_STUFF)
$(PS_COMMAND)
HolSat.tex: HolSat.stex $(PS_STUFF) zchaff.cnf
$(PS_COMMAND)
# This builds figs/0.mps, figs/1.mps, ...
figures:
mpost -mem=metafun -tex=latex figure.mp
EXTRA_CLEANS = drules.tex tactics.tex theories.tex libraries.tex \
PatternMatchesLib.tex HolSat.tex definitions.tex \
system.tex conv.tex math.tex \
description.pdf \
$(patsubst %,%.aux,$(TEX_CORES)) \
description.log description.out \
description.toc description.fls description.idx description.ilg \
description.ind description.blg description.bbl \
description.fdb_latexmk