Introduce tests/dune_hello

tests/Makefile

@@ -20,6 +20,7 @@ ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
+ALL_TEST_DIRS += dune_hello
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))

tests/dune_hello/.gitignore

@@ -0,0 +1,3 @@
+*.ml
+_build
+lib

tests/dune_hello/Hello.fst

@@ -0,0 +1,5 @@
+module Hello
+
+open FStar.IO
+
+let _ = print_string "Hi!\n"

tests/dune_hello/Makefile

@@ -0,0 +1,15 @@
+FSTAR_EXE ?= ../../bin/fstar.exe
+
+.PHONY: all
+all: run
+
+Hello.ml: Hello.fst
+	$(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello
+
+bin/hello.exe: Hello.ml
+	$(FSTAR_EXE) --ocamlenv dune build @install --profile=release
+	$(FSTAR_EXE) --ocamlenv dune install --prefix=.
+
+.PHONY: run
+run: bin/hello.exe
+	./bin/hello.exe | grep "Hi!"

tests/dune_hello/dune

@@ -0,0 +1,11 @@
+(executable
+ (name hello)
+ (public_name hello.exe)
+ (libraries fstar.lib)
+ (modes native)
+)
+(env
+  (_
+    (bin_annot false)
+    (flags (:standard -w -A)))
+)

tests/dune_hello/dune-project

@@ -0,0 +1,7 @@
+(lang dune 3.8)
+(name hello)
+
+(package
+  (name hello)
+  (synopsis "An example F* application")
+)