Merge pull request #212 from FStarLang/taramana_dune

Build with dune

Makefile

@@ -1,20 +1,16 @@
 # make src/Ast.processed.ml
 include $(shell ocamlfind query visitors)/Makefile.preprocess
 
-.PHONY: all minimal clean test
-
-OCAMLBUILD=ocamlbuild -I src -I lib -I parser -I krmllib -use-menhir -use-ocamlfind \
- -menhir "menhir --infer --explain" -quiet
-FLAVOR?=native
-TARGETS=Karamel.$(FLAVOR)
-EXTRA_TARGETS=Ast.inferred.mli krmllib/C.cmx krmllib/TestLib.cmx krmllib/C.cmo krmllib/TestLib.cmo
+.PHONY: all minimal clean test pre krmllib install
 
 ifeq ($(OS),Windows_NT)
   OCAMLPATH_SEP=;
 else
   OCAMLPATH_SEP=:
 endif
 
+all: minimal krmllib
+
 ifdef FSTAR_HOME
   OCAMLPATH:=$(OCAMLPATH)$(OCAMLPATH_SEP)$(FSTAR_HOME)/lib
 else
@@ -29,15 +25,9 @@ endif
 export FSTAR_HOME
 export OCAMLPATH
 
-all: minimal krmllib
-	@OCAML_ERROR_STYLE="short" \
-	 $(OCAMLBUILD) $(EXTRA_TARGETS)
-
 minimal: src/AutoConfig.ml src/Version.ml
-	@# Workaround Windows bug in OCamlbuild
-	$(shell [ -f Karamel.$(FLAVOR) ] && rm Karamel.$(FLAVOR))
-	@OCAML_ERROR_STYLE="short" $(OCAMLBUILD) $(TARGETS)
-	ln -sf Karamel.$(FLAVOR) krml
+	+ OCAML_ERROR_STYLE="short" $(MAKE) -C src
+	ln -sf src/_build/default/Karamel.exe krml
 
 krmllib: minimal
 	$(MAKE) -C krmllib
@@ -60,12 +50,13 @@ src/Version.ml:
 	@echo "let version = \"$(shell git rev-parse HEAD)\"" > $@ \
 
 clean:
-	rm -rf krml _build Karamel.$(FLAVOR)
-	$(MAKE) -C test clean
+	rm -rf krml
+	$(MAKE) -C src clean
 	$(MAKE) -C krmllib clean
+	$(MAKE) -C test clean
 
 test: all
-	+$(MAKE) -C test
+	$(MAKE) -C test
 
 # Auto-detection
 pre:
@@ -76,7 +67,7 @@ pre:
 install: all
 	@if [ x"$(PREFIX)" = x ]; then echo "please define PREFIX"; exit 1; fi
 	mkdir -p $(PREFIX)/bin
-	cp _build/src/Karamel.native $(PREFIX)/bin/krml
+	cp src/_build/default/Karamel.exe $(PREFIX)/bin/krml
 	mkdir -p $(PREFIX)/include
 	cp -r include/* $(PREFIX)/include
 	mkdir -p $(PREFIX)/lib/krml

krmllib/Makefile

@@ -6,6 +6,9 @@
 
 all: verify-all compile-all
 
+.PHONY: all verify-all compile-all
+
+
 ################################################################################
 # Verification & extraction                                                    #
 ################################################################################
@@ -108,7 +111,8 @@ $(GENERIC_DIR):
 	mkdir -p $@
 
 # Everything in the universe
-$(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c/*.c) $(wildcard c/*.h) ../_build/src/Karamel.native
+$(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c/*.c) $(wildcard c/*.h) ../src/_build/default/Karamel.exe
+	KRML_HOME=$(shell pwd)/.. \
 	../krml $(KRML_ARGS) -tmpdir $(GENERIC_DIR) \
 	  -warn-error +9+11 \
 	  $(MACHINE_INTS) \
@@ -123,7 +127,7 @@ $(GENERIC_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(wildcard c
 	cp c/*.c c/*.h $(dir $@)
 
 # Minimalistic build (just machine integers and endianness)
-$(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar_uint128*.h) ../_build/src/Karamel.native
+$(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar_uint128*.h) ../src/_build/default/Karamel.exe
 	mkdir -p $(dir $@)
 	KRML_HOME=$(shell pwd)/.. \
 	../krml $(KRML_ARGS) -tmpdir $(MINI_DIR) \
@@ -144,7 +148,7 @@ $(MINI_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(MINI_DIR) $(wildcard c/fstar
 # Extracted (and verified) uint128s; copied into generic and minimal. Note that
 # FStar.UInt64 shares the same bundle name, meaning that
 # FStar_UInt128_Verified.h can be dropped in any of the two krmllibs above.
-$(UINT128_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(MINI_DIR) ../_build/src/Karamel.native
+$(UINT128_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(MINI_DIR) ../src/_build/default/Karamel.exe
 	KRML_HOME=$(shell pwd)/.. \
 	../krml $(KRML_ARGS) -tmpdir $(UINT128_DIR) \
 	  $(addprefix -add-include ,'<inttypes.h>' '<stdbool.h>' '"krml/internal/types.h"' '"krml/internal/target.h"') \