diff --git a/tests/dune_hello/Makefile b/tests/dune_hello/Makefile index 84107aea18d..99e2277ff37 100644 --- a/tests/dune_hello/Makefile +++ b/tests/dune_hello/Makefile @@ -13,6 +13,8 @@ bin/hello.exe: Hello.ml .PHONY: run run: bin/hello.exe ./bin/hello.exe | grep "Hi!" + # Find a way to install this? dune install skips the bytecode + $(FSTAR_EXE) --ocamlenv dune exec ./hello.bc | grep "Hi!" clean: dune clean diff --git a/tests/dune_hello/dune b/tests/dune_hello/dune index 86f94bf3049..e1bb73c8a6b 100644 --- a/tests/dune_hello/dune +++ b/tests/dune_hello/dune @@ -2,5 +2,8 @@ (name hello) (public_name hello.exe) (libraries fstar.lib) - (modes native) + (modes native byte) ) +(env + (_ + (flags (:standard -w -A)))) diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile index 14bfea61f9b..728af2a84e2 100644 --- a/tests/simple_hello/Makefile +++ b/tests/simple_hello/Makefile @@ -6,14 +6,18 @@ FSTAR ?= ../../bin/fstar.exe all: Hello.test -Hello.test: Hello.exe - ./Hello.exe | grep "Hello F\*!" +Hello.test: Hello.exe Hello.byte + ./Hello.exe | grep "Hello F\*!" + ./Hello.byte | grep "Hello F\*!" %.ml: %.fst $(FSTAR) --codegen OCaml $< --extract $* %.exe: %.ml + $(FSTAR) --ocamlopt $< -o $@ + +%.byte: %.ml $(FSTAR) --ocamlc $< -o $@ clean: - rm -f *.ml *.exe + rm -f *.ml *.exe *.byte