diff options
| -rw-r--r-- | Makefile | 21 | ||||
| -rw-r--r-- | README.md | 8 |
2 files changed, 13 insertions, 16 deletions
@@ -1,18 +1,23 @@ +UNAME_S := $(shell uname -s) +ifeq ($(UNAME_S),Linux) + ARCH := x86_64-linux +endif +ifeq ($(UNAME_S),Darwin) + ARCH := x86_64-macosx +endif + COMPCERTRECDIRS := lib common x86_64 x86 backend cfrontend driver flocq exportclight \ MenhirLib cparser -COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) - COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \ -R src/extraction coqup.extraction -R src/translation coqup.translation \ - -R src coqup $(COMPCERTCOQINCLUDES) + -R src coqup \ + $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source -COQMAKE := "$(COQBIN)coq_makefile" +COQMAKE := $(COQBIN)coq_makefile -COQUPDIRS := translation common verilog -VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) -VS := src/Compiler.v src/Simulator.v $(VSSUBDIR) +VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v) PREFIX ?= . @@ -23,7 +28,7 @@ all: lib/COMPCERTSTAMP $(MAKE) compile lib/COMPCERTSTAMP: - (cd lib/CompCert && ./configure x86_64-linux) + (cd lib/CompCert && ./configure $(ARCH)) $(MAKE) -C lib/CompCert touch $@ @@ -18,14 +18,6 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so These dependencies can be installed manually, or automatically through Nix. -### Building on OSX - -To build the project on OSX, currently the makefile has to be manually edited so that CompCert builds for the correct architecture. To do this, simply execute the following `sed` command to change the instance of `x86_64-linux` into `x86_64-macosx`. - -``` shell -sed -i'' 's/x86_64-linux/x86_64-macosx/' Makefile -``` - ### Downloading CompCert CompCert is added as a submodule in the `lib/CompCert` directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run: |