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 extra krmllib install
 
 ifeq ($(OS),Windows_NT)
   OCAMLPATH_SEP=;
 else
   OCAMLPATH_SEP=:
 endif
 
+all: minimal krmllib extra
+
 ifdef FSTAR_HOME
   OCAMLPATH:=$(OCAMLPATH)$(OCAMLPATH_SEP)$(FSTAR_HOME)/lib
 else
@@ -29,18 +25,16 @@ endif
 export FSTAR_HOME
 export OCAMLPATH
 
-all: minimal krmllib
-	@OCAML_ERROR_STYLE="short" \
-	 $(OCAMLBUILD) $(EXTRA_TARGETS)
+extra: pre krmllib
+	+ OCAML_ERROR_STYLE="short" \
+	OCAMLPATH="$(OCAMLPATH)$(OCAMLPATH_SEP)$(FSTAR_HOME)/bin" $(MAKE) -C krmllib extra
 
 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
+	+$(MAKE) -C krmllib
 
 src/AutoConfig.ml:
 	@if [ x"$(PREFIX)" != x ]; then \
@@ -60,9 +54,10 @@ 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
@@ -76,7 +71,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,12 @@
 
 all: verify-all compile-all
 
+extra:
+	+dune build
+
+.PHONY: all verify-all compile-all extra
+
+
 ################################################################################
 # Verification & extraction                                                    #
 ################################################################################
@@ -52,15 +58,18 @@ ROOTS = $(wildcard *.fst) $(wildcard *.fsti) $(wildcard ../runtime/*.fst) \
     FStar.HyperStack.IO.fst FStar.IO.fst FStar.Int.Cast.Full.fst \
     FStar.Bytes.fsti FStar.Dyn.fsti LowStar.Printf.fst LowStar.Endianness.fst
 
-.PHONY: clean clean-c
-clean: clean-c
+.PHONY: clean clean-c clean-ml
+clean: clean-c clean-ml
 	rm -rf *.checked *.source .depend
 
 SHELL:=$(shell which bash)
 
 clean-c:
 	rm -rf dist out extract-all */*.o
 
+clean-ml:
+	dune clean
+
 ifndef NODEPEND
 ifndef MAKE_RESTARTS
 .depend: .FORCE obj
@@ -108,7 +117,7 @@ $(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 $(KRML_ARGS) -tmpdir $(GENERIC_DIR) \
 	  -warn-error +9+11 \
 	  $(MACHINE_INTS) \
@@ -123,7 +132,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,8 +153,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
-	KRML_HOME=$(shell pwd)/.. \
+$(UINT128_DIR)/Makefile.include: $(ALL_KRML_FILES) | $(GENERIC_DIR) $(MINI_DIR) ../src/_build/default/Karamel.exe
 	../krml $(KRML_ARGS) -tmpdir $(UINT128_DIR) \
 	  $(addprefix -add-include ,'<inttypes.h>' '<stdbool.h>' '"krml/internal/types.h"' '"krml/internal/target.h"') \
 	  -bundle FStar.UInt64[rename=FStar_UInt_8_16_32_64] \

krmllib/dune

@@ -0,0 +1,6 @@
+(library
+  (name krmllib)
+  (libraries
+    fstar.lib)
+  (wrapped false)
+)

krmllib/dune-project

@@ -0,0 +1,2 @@
+(lang dune 2.0)
+(name krmllib)

src/Makefile

@@ -0,0 +1,7 @@
+all:
+	+dune build
+
+clean:
+	dune clean
+
+.PHONY: all clean

src/dune

@@ -0,0 +1,24 @@
+(include_subdirs unqualified)
+
+(executable
+  (name Karamel)
+  (libraries
+    ppx_deriving.std
+    ppx_deriving_yojson
+    zarith
+    pprint
+    unix
+    menhirLib
+    sedlex
+    process
+    fix
+    wasm
+    visitors.ppx
+    visitors.runtime
+    sedlex.ppx
+  )
+  (preprocess
+    (pps ppx_deriving.std ppx_deriving_yojson sedlex.ppx visitors.ppx)
+  )
+  (flags (:standard -warn-error -A -w @[email protected]@[email protected]@31..38-39-40-41@43@57))
+)

src/dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.0)
+(name karamel)
+(using menhir 2.0)

src/parser/dune

@@ -0,0 +1,5 @@
+  (menhir
+    (modules KParser)
+    (flags --explain --dump)
+    (infer true)
+  )

test/Makefile

@@ -26,7 +26,7 @@ ifneq ($(CRYPTO),)
   CRYPTO_OPTS	= -I $(CRYPTO) -I $(CRYPTO)/real
 endif
 TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
-KRML_BIN	= ../_build/src/Karamel.native
+KRML_BIN	= ../src/_build/default/Karamel.exe
 KRML		= $(KRML_BIN) $(KOPTS) $(TEST_OPTS)
 
 # TODO: disambiguate between broken tests that arguably should work (maybe
@@ -242,19 +242,18 @@ $(LOWLEVEL_DIR)/%: ctypes/%
 	cp $< $@
 
 ctypes-test: $(LOWLEVEL_DIR)/Client.native
-	cd $(LOWLEVEL_DIR)/_build && export LD_LIBRARY_PATH=. && \
-	  ./Client.native && ./Client.byte
+	cd $(LOWLEVEL_DIR)/_build/default && export LD_LIBRARY_PATH=. && \
+	  ./Client.exe && ./Client.bc
 
 sepcomp-test:
 	+$(MAKE) -C sepcomp
 .PHONY: sepcomp-test
 
-CTYPES_HAND_WRITTEN_FILES=myocamlbuild.ml Client.ml _tags
+CTYPES_HAND_WRITTEN_FILES=Client.ml dune dune-workspace lib/dune lib_gen/dune
 
 .PHONY: $(LOWLEVEL_DIR)/Client.native
 $(LOWLEVEL_DIR)/Client.native: $(OUTPUT_DIR)/Ctypes2.exe $(addprefix $(LOWLEVEL_DIR)/,$(CTYPES_HAND_WRITTEN_FILES))
-	cd $(dir $@) && \
-	  CTYPES_LIB_DIR=$(shell ocamlfind query ctypes) ocamlbuild -use-ocamlfind $(notdir $@) Client.byte
+	cd $(dir $@) && env CTYPES_LIB_DIR=$(shell ocamlfind query ctypes) LOWLEVEL_DIR=$(realpath $(LOWLEVEL_DIR)) dune build
 
 
 # A pseudo-target for WASM compilation that does not match any specific file.

test/ctypes/dune

@@ -0,0 +1,39 @@
+(executable
+  (name Client)
+  (libraries
+    Ctypes1_stubs
+    Lowlevel_bindings
+    Lowlevel_stubs
+    Ctypes2_bindings
+    Ctypes2_stubs
+    Client_foreign
+  )
+  (link_flags "-linkall")
+  (modes (byte exe) (native exe))
+  (flags (:standard -w -32-33))
+)
+
+(library
+  (name Client_foreign)
+  (modules)
+  (wrapped false)
+  (foreign_stubs (language c) (names Lowlevel Ctypes1 Ctypes2 Lowlevel_c_stubs Ctypes1_c_stubs Ctypes2_c_stubs) (include_dirs %{env:KRML_HOME=../../..}/include %{env:KRML_HOME=../../..}/krmllib/dist/generic internal %{env:CTYPES_LIB_DIR=.}))
+)
+
+(rule
+  (target Ctypes1_c_stubs.c)
+  (deps lib/Ctypes1_c_stubs.c)
+  (action (copy %{deps} %{target}))
+)
+
+(rule
+  (target Lowlevel_c_stubs.c)
+  (deps lib/Lowlevel_c_stubs.c)
+  (action (copy %{deps} %{target}))
+)
+
+(rule
+  (target Ctypes2_c_stubs.c)
+  (deps lib/Ctypes2_c_stubs.c)
+  (action (copy %{deps} %{target}))
+)

test/ctypes/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.2)

test/ctypes/lib/dune

@@ -0,0 +1,77 @@
+(library
+  (name Ctypes1_bindings)
+  (wrapped false)
+  (libraries
+    ctypes
+  )
+  (modules Ctypes1_bindings)
+  (flags (:standard -w -A))
+)
+
+(library
+  (name Lowlevel_bindings)
+  (wrapped false)
+  (libraries
+    ctypes
+    Ctypes1_bindings
+    Ctypes1_stubs
+  )
+  (modules Lowlevel_bindings)
+  (flags (:standard -w -A))
+)
+
+(library
+  (name Ctypes2_bindings)
+  (wrapped false)
+  (modules Ctypes2_bindings)
+  (libraries
+    Ctypes1_bindings
+    Ctypes1_stubs
+  )
+  (flags (:standard -w -A))
+)
+
+(library
+  (name Lowlevel_stubs)
+  (wrapped false)
+  (modules Lowlevel_stubs)
+  (libraries
+    ctypes.stubs
+  )
+)
+
+(library
+  (name Ctypes1_stubs)
+  (wrapped false)
+  (modules Ctypes1_stubs)
+  (libraries
+    ctypes.stubs
+  )
+)
+
+(library
+  (name Ctypes2_stubs)
+  (wrapped false)
+  (modules Ctypes2_stubs)
+  (libraries
+    ctypes.stubs
+  )
+)
+
+(rule
+  (targets Ctypes1_stubs.ml Ctypes1_c_stubs.c)
+  (deps ../lib_gen/Ctypes1_gen.exe)
+  (action (chdir .. (run %{dep:../lib_gen/Ctypes1_gen.exe})))
+)
+
+(rule
+  (targets Lowlevel_stubs.ml Lowlevel_c_stubs.c)
+  (deps ../lib_gen/Lowlevel_gen.exe)
+  (action (chdir .. (run %{dep:../lib_gen/Lowlevel_gen.exe})))
+)
+
+(rule
+  (targets Ctypes2_stubs.ml Ctypes2_c_stubs.c)
+  (deps ../lib_gen/Ctypes2_gen.exe)
+  (action (chdir .. (run %{dep:../lib_gen/Ctypes2_gen.exe})))
+)

test/ctypes/lib_gen/dune

@@ -0,0 +1,29 @@
+(executable
+  (name Ctypes1_gen)
+  (modules Ctypes1_gen)
+  (libraries
+    ctypes.stubs
+    Ctypes1_bindings
+  )
+  (link_flags "-linkall")
+)
+
+(executable
+  (name Lowlevel_gen)
+  (modules Lowlevel_gen)
+  (libraries
+    ctypes.stubs
+    Lowlevel_bindings
+  )
+  (link_flags "-linkall")
+)
+
+(executable
+  (name Ctypes2_gen)
+  (modules Ctypes2_gen)
+  (libraries
+    ctypes.stubs
+    Ctypes2_bindings
+  )
+  (link_flags "-linkall")
+)