1.PHONY: build install test-compiler
2
3## Silent by default
4V =
5ifeq ($(strip $(V)),)
6        E = @echo
7        Q = @
8else
9        E = @\#
10        Q =
11endif
12export E Q
13
14PWD:=$(shell pwd)
15SCRIPTS_DIR:=$(PWD)/scripts/
16include $(PWD)/../config.mk
17
18# These file lists are for generating dummy headers for c compilation
19PASS_TEST_COGENT_FILES := $(wildcard tests/pass_*.cogent)
20FAIL_TEST_COGENT_FILES := $(wildcard tests/fail_*.cogent)
21DUMMY_HEADER_FILES := $(addprefix tests/include/,$(notdir $(PASS_TEST_COGENT_FILES:.cogent=_dummy.h)))
22
23all: .cabal-update install
24	$(E) "Cogent Compiler successfully built for $(OS)."
25	$(E)
26	$(E) "Add the installed 'cogent' executable to your path."
27	$(E)
28	$(E) "To enable bash auto-completion for 'cogent', please add the following to your .bashrc file:"
29	$(E) "source $(PWD)/misc/cogent_autocomplete.sh"
30	$(E)
31	$(E)
32
33
34stack-build:
35	$(E) "Building Cogent using stack."
36	$(Q) $(STACK) build
37
38build:
39	$(E) "Building..."
40	$(Q) $(CABAL) new-build $(BUILD_FLAGS)
41
42install:
43	$(E) "Installing.."
44	$(Q) $(CABAL) new-install $(INSTALL_FLAGS)
45
46clean:
47	$(Q) rm -rf out/
48	$(Q) rm -rf tests/include
49	$(Q) find . -name "*_flymake.hs" -delete
50
51full-clean: clean
52	$(Q) $(CABAL) new-clean
53	$(Q) rm -rf dist-newstyle/ ../isa-parser/dist-newstyle
54
55
56dev: .cabal-update .build
57	$(E) "Cogent Compiler successfully built for $(OS)."
58	$(E)
59	$(E) "Add 'cogent' compiler to your path by running (substitute the placeholders with your configuration):"
60	$(E) '  export PATH=$(PWD)/dist-newstyle/build/<ARCH>/ghc-<GHC_VERSION>/cogent-<COGENT_VERSION>/build/cogent/cogent:$$PATH'
61	$(E)
62	$(E) "_Or_ make a symlink to the executable in ~/.cabal/bin by running:"
63	$(E) '  ln -s $(PWD)/dist-newstyle/build/<ARCH>/ghc-<GHC_VERSION>/cogent-<COGENT_VERSION>/build/cogent/cogent $$HOME/.cabal/bin/cogent' 
64	$(E)
65	$(E) "To enable bash auto-completion for 'cogent', please add the following to your .bashrc file:"
66	$(E) "source $(PWD)/misc/cogent_autocomplete.sh"
67	$(E)
68	$(E)
69
70.cabal-update:
71	$(Q) $(CABAL) new-update
72
73local: .cabal-update
74	$(E) "Installing cogent locally"
75	$(Q) $(CABAL) new-install --overwrite-policy=always --installdir=$(PWD)/build/bin/
76
77# There's a sed script that does a very similar thing in scripts/cogent_validate.sh, and for some reason they're both necessary.
78tests/include/%_dummy.h: tests/%.cogent
79	$(Q) egrep "^type +([A-Z][a-zA-Z0-9_']*)( [a-z][a-zA-Z0-9_']*)* *(--.*)?$$" $^ | sed -e "s/type \([A-Z][a-zA-Z0-9_']*\).*$$/struct \1 {int dummy; }; typedef struct \1 \1;/" > $@
80
81.gen-types: .test-setup $(DUMMY_HEADER_FILES)
82	$(E) "Generated C headers."
83
84.test-setup:
85	$(Q)mkdir -p tests/include
86
87tests: test-compiler \
88       test-tc-proof test-shallow-proof test-ee test-hs test-quickcheck
89
90test-compiler: test-clean .test-cogent
91	./tests/run-test-suite.py \
92	# test-tc test-ds test-an test-mn test-cg test-gcc \
93	# test-pp test-aq \
94	# test-hs \
95	# test-quickcheck
96
97test-compiler-proofs: test-clean .test-cogent
98	./tests/run-test-suite.py --repo "$(PWD)/../" \
99		--extra-phases "$(PWD)/tests/phases/" \
100		--repo "$(PWD)/../" \
101		--ignore-phases "cogent"
102
103test-quickcheck:
104	$(Q) $(CABAL) test test-quickcheck
105
106test-clean:
107	$(E) "Cleaning up artefacts from earlier test runs."
108	$(Q) rm -rf out/
109	$(Q) rm -rf tests/include/
110
111.test-cogent:
112ifeq ($(shell which cogent 2> /dev/null; echo $$? ),1)
113	$(error Cogent not installed, or is not available in your PATH)
114endif
115
116test-pp:
117	$(E) "=== Parser & Pretty-Printer Tests ==="
118	$(SCRIPTS_DIR)/cogent_validate.sh -pp
119
120test-tc:
121	$(E) "=== Type Checking Tests ==="
122	$(SCRIPTS_DIR)/cogent_validate.sh -tc
123
124test-ds:
125	$(E) "=== Desugaring Tests ==="
126	$(SCRIPTS_DIR)/cogent_validate.sh -ds
127
128test-an:
129	$(E) "=== A-normal transform Tests ==="
130	$(SCRIPTS_DIR)/cogent_validate.sh -an
131
132test-mn:
133	$(E) "=== Monomorphization Tests ==="
134	$(SCRIPTS_DIR)/cogent_validate.sh -mn
135
136test-cg:
137	$(E) "=== Code Generation Tests ==="
138	$(SCRIPTS_DIR)/cogent_validate.sh -cg
139
140test-tc-proof:
141	$(E) "=== Proof Generation For Type Checking Tests ==="
142	$(SCRIPTS_DIR)/cogent_validate.sh -tc-proof
143
144test-ac: .gen-types
145	$(E) "=== Isabelle (AutoCorres) test ==="
146	$(SCRIPTS_DIR)/cogent_validate.sh -ac
147
148test-c-refine: .gen-types
149	$(E) "=== C-refinement proof test ==="
150	$(SCRIPTS_DIR)/cogent_validate.sh -c-refine
151
152test-flags:
153	$(E) "=== FFI-generator Tests ==="
154	$(SCRIPTS_DIR)/cogent_validate.sh -flags
155
156test-aq:
157	$(E) "=== Anti-quotation Tests ==="
158	$(SCRIPTS_DIR)/cogent_validate.sh -aq
159
160test-shallow-proof:
161	$(E) "=== Shallow-embedding Proofs Tests ==="
162	$(SCRIPTS_DIR)/cogent_validate.sh -shallow-proof
163
164test-goanna:
165	$(E) "=== Goanna test ==="
166	$(error Goanna tests are not currently supported.)
167	$(SCRIPTS_DIR)/cogent_validate.sh -goanna
168
169test-ee: .gen-types
170	$(E) "=== End-to-End Proofs Tests ==="
171	$(SCRIPTS_DIR)/cogent_validate.sh -ee
172
173test-gcc: .gen-types
174	$(E) "=== Compile generated code using GCC ==="
175	$(SCRIPTS_DIR)/cogent_validate.sh -gcc
176
177test-hs:
178	$(E) "=== Generate Haskell shallow embedding and compile using GHC ==="
179	$(SCRIPTS_DIR)/cogent_validate.sh -hs-shallow
180
181test-hsc:
182	$(E) "=== Generate C FFI in .hsc form and compile with hsc2hs ==="
183	$(SCRIPTS_DIR)/cogent_validate.sh -hsc-gen
184
185test-libgum:
186	$(E) "=== Typechecking libgum ==="
187	$(SCRIPTS_DIR)/cogent_validate.sh -libgum
188
189examples: .test-cogent
190	$(E) "=== Build Cogent examples ==="
191	$(SCRIPTS_DIR)/cogent_validate.sh -examples
192
193examples-clean:
194	$(E) "=== Build Cogent examples ==="
195	$(SCRIPTS_DIR)/build_examples.sh clean
196
197help:
198	$(E) "** Cogent Compiler **"
199	$(E) "Run 'make' to build the Cogent compiler."
200	$(E) ""
201	$(E) "* make"
202	$(E) "  Install Cogent via cabal (default to: ~/.cabal/bin)"
203	$(E) ""
204	$(E) "* make dev"
205	$(E) "  Build Cogent via cabal to a local dist-newstyle directory"
206	$(E) ""
207	$(E) "* make local"
208	$(E) "  Build Cogent and put the executable in build/bin/"
209	$(E) ""
210	$(E) "* make clean"
211	$(E) "  Cleanup"
212	$(E) ""
213	$(E) "* make full-clean"
214	$(E) "  Cleanup (removes sandbox)."
215	$(E) ""
216	$(E) "* make tests"
217	$(E) "  Run all tests."
218	$(E) ""
219	$(E) "* make test-compiler"
220	$(E) "  Run all compiler tests (excl. Isabelle proofs)."
221	$(E) ""
222	$(E) "* make test-compiler-proofs"
223	$(E) "  Only run compiler Isabelle proof tests."
224	$(E) ""
225	$(E) "* make test-clean"
226	$(E) "  Cleanup artefacts from earlier test runs."
227	$(E) ""
228	$(E) "* make test-tc"
229	$(E) "  Run Typechecking Tests."
230	$(E) ""
231	$(E) "* make test-ds"
232	$(E) "  Run Desugaring Tests."
233	$(E) ""
234	$(E) "* make test-an"
235	$(E) "  Run A-Normalisation Tests."
236	$(E) ""
237	$(E) "* make test-mn"
238	$(E) "  Run Monomorphisation Tests."
239	$(E) ""
240	$(E) "* make test-cg"
241	$(E) "  Run Code Generation Tests."
242	$(E) ""
243	$(E) "* make test-tc-proof"
244	$(E) "  Run Typechecking Proof Generation Tests."
245	$(E) ""
246	$(E) "* make test-ac"
247	$(E) "  Run AutoCorres test."
248	$(E) ""
249	$(E) "* make test-c-refine"
250	$(E) "  Run C-refinement proof test."
251	$(E) ""
252	$(E) "* make test-flags"
253	$(E) "  Run Compiler Flags Tests."
254	$(E) ""
255	$(E) "* make test-aq"
256	$(E) "  Run Anti-Quotation Tests."
257	$(E) ""
258	$(E) "* make test-shallow-proof"
259	$(E) "  Run Shallow Embedding Proofs Tests."
260	$(E) ""
261	$(E) "* make test-goanna"
262	$(E) "  Run Goanna Test [Currently Not Supported]."
263	$(E) ""
264	$(E) "* make test-ee"
265	$(E) "  Run End-to-End Proofs Tests."
266	$(E) ""
267	$(E) "* make test-gcc"
268	$(E) "  Compile generated code using GCC."
269	$(E) ""
270	$(E) "* make test-hs"
271	$(E) "  Generate Haskell shallow embedding and compile with GHC."
272	$(E) ""
273	$(E) "* make test-hsc"
274	$(E) "  Generate C FFI in .hsc form and compile with hsc2hs."
275	$(E) ""
276	$(E) "* make test-libgum"
277	$(E) "  Run libgum Typechecking Tests."
278	$(E) ""
279	$(E) "* make examples"
280	$(E) "  Compile Cogent examples."
281	$(E) ""
282	$(E) "* make examples-clean"
283	$(E) "  Clean up earlier build of examples."
284	$(E) ""
285	$(E) "* make help"
286	$(E) "  Print this help."
287
288