Skip to content

Commit

Permalink
simple_hello/dune_hello: test bytecode too
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Oct 18, 2024
1 parent c52f271 commit 443289c
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 4 deletions.
2 changes: 2 additions & 0 deletions tests/dune_hello/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 4 additions & 1 deletion tests/dune_hello/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,8 @@
(name hello)
(public_name hello.exe)
(libraries fstar.lib)
(modes native)
(modes native byte)
)
(env
(_
(flags (:standard -w -A))))
10 changes: 7 additions & 3 deletions tests/simple_hello/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 443289c

Please sign in to comment.