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