-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMakefile
More file actions
153 lines (125 loc) · 4.01 KB
/
Makefile
File metadata and controls
153 lines (125 loc) · 4.01 KB
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
#
# Rules for compiling and linking the Sage typechecker/evaluator
#
# Type
# make to rebuild the executable file sage
# make windows to rebuild the executable file sage.exe
# make test to rebuild the executable and run it on tests
# make clean to remove all intermediate and temporary files
# make depend to rebuild the intermodule dependency graph that is used
# by make to determine which order to schedule
# compilations. You should not need to do this unless
# you add new modules or new dependencies between
# existing modules. (The graph is stored in the file
# .depend)
# These are the object files needed to rebuild the main executable file
#
OCAMLC=$(if $(shell which ocamlc.opt),ocamlc.opt,ocamlc)
NOCAMLC=$(if $(shell which ocamlopt.opt),ocamlopt.opt,ocamlopt)
MLFILES = \
src/support.ml \
src/options.ml \
src/syntax.ml \
src/print.ml \
src/primitives.ml \
src/parser.ml \
src/lexer.ml \
src/eval.ml \
src/gcenv.ml \
src/db.ml \
src/subtype.ml \
src/prim_defs.ml\
src/compile.ml \
src/formulaparse.ml \
src/simplify.ml \
src/sformula.ml \
src/basicalg.ml
MLIFILES = $(filter-out src/lexer.mli, $(patsubst %.ml,%.mli, $(MLFILES)))
CMIFILES = $(patsubst %.ml,%.cmi, $(MLFILES))
OBJS = $(patsubst %.ml,%.cmo, $(MLFILES))
NOBJS = $(patsubst %.ml,%.cmx, $(MLFILES))
DEPEND += src/lexer.ml src/parser.ml
# Files that need to be generated from other files
OCAMLOPTS = unix.cma str.cma -g -I src
NOCAMLOPTS = unix.cmxa str.cmxa -p -I src
DB = cow.db
# When "make" is invoked with no arguments, we build an executable
# typechecker, after building everything that it depends on
all: sage unittest pdb platex
# On a Windows machine, we do exactly the same except that the executable
# file that gets built needs to have the extension ".exe"
windows: f.exe
# Build an executable typechecker
sage: $(OBJS) src/main.cmo
@echo Linking $@
$(OCAMLC) $(OCAMLOPTS) -o $@ $^
sage.opt: $(NOBJS) src/main.cmx
@echo Linking $@
$(NOCAMLC) $(NOCAMLOPTS) -o $@ $^
unittest: $(OBJS) src/unittest.cmo
@echo Linking $@
$(OCAMLC) $(OCAMLOPTS) -o $@ $^
pdb: $(OBJS) src/pdb.cmo
@echo Linking $@
$(OCAMLC) $(OCAMLOPTS) -o $@ $^
platex: $(OBJS) src/platex.cmo
$(OCAMLC) $(OCAMLOPTS) -o $@ $^
# Build an executable typechecker for Windows
sage.exe: $(OBJS) src/main.cmo
@echo Linking $@
$(OCAMLC) $(OCAMLOPTS) -o $@ $^
# Create a dependency graph, in postscript format, for the modules
depgraph:
ocamldoc -dot *.mli *.ml -o depgraph.dot
dot -Tps depgraph.dot > depgraph.ps
tydepgraph:
ocamldoc -dot -dot-types *.mli *.ml -o tydepgraph.dot
dot -Tps tydepgraph.dot > tydepgraph.ps
# Build and test
test: all
@ ./unittest
@ rm -f $(DB)
@ cd refute && $(MAKE)
@ cd tests && $(MAKE)
docs: all
ocamldoc -v -html -d doc/ocamldoc -keep-code -sort \
-all-params -colorize-code -I src $(MLIFILES) $(MLFILES)
# Compile an ML module interface
%.cmi : %.mli
$(OCAMLC) -c $(OCAMLOPTS) $<
# Compile an ML module implementation to bytecode
%.cmo : %.ml
$(OCAMLC) -c $(OCAMLOPTS) $<
# Compile an ML module implementation to native code
%.cmx : %.ml
$(NOCAMLC) -c $(NOCAMLOPTS) $<
# Generate ML files from a parser definition file
%.ml %.mli: %.mly
# @rm -f $^
ocamlyacc -v $<
# @chmod -w $^
# Generate ML files from a lexer definition file
%.ml %.mli: %.mll
@rm -f $@
ocamllex $<
@chmod -w $@
# Clean up the directory
clean::
rm -rf $(OBJS) $(NOBJS) $(CMIFILES) \
src/lexer.ml src/parser.ml src/parser.mli src/parser.output \
sage unittest pdb TAGS src/*~ *.bak depgraph.dot depgraph.ps \
sage.opt sage.exe pdb.exe unittest.exe platex.exe \
$(DB) \
src/*.cmo src/*.cmx src/*.cmi \
platex \
doc/ocamldoc/*
cd tests && make clean
cd refute && make clean
# Rebuild intermodule dependencies
depend:: $(DEPEND)
ocamldep $(INCLUDE) $(MLIFILES) $(MLFILES) > .depend
# Word count
wc:: clean
wc $(MLFILES) $(MLIFILES) src/parser.mly src/lexer.mll
# Include an automatically generated list of dependencies between source files
include .depend