From 3f8b702d9c943a47e16a785bf8b2c01457f03321 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 12:21:10 -0700 Subject: [PATCH] Introduce tests/dune_hello --- tests/Makefile | 1 + tests/dune_hello/.gitignore | 3 +++ tests/dune_hello/Hello.fst | 5 +++++ tests/dune_hello/Makefile | 15 +++++++++++++++ tests/dune_hello/dune | 11 +++++++++++ tests/dune_hello/dune-project | 7 +++++++ 6 files changed, 42 insertions(+) create mode 100644 tests/dune_hello/.gitignore create mode 100644 tests/dune_hello/Hello.fst create mode 100644 tests/dune_hello/Makefile create mode 100644 tests/dune_hello/dune create mode 100644 tests/dune_hello/dune-project diff --git a/tests/Makefile b/tests/Makefile index 8fad46f21c1..e864166662f 100644 --- a/tests/Makefile +++ b/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)) diff --git a/tests/dune_hello/.gitignore b/tests/dune_hello/.gitignore new file mode 100644 index 00000000000..dc72cf78a16 --- /dev/null +++ b/tests/dune_hello/.gitignore @@ -0,0 +1,3 @@ +*.ml +_build +lib diff --git a/tests/dune_hello/Hello.fst b/tests/dune_hello/Hello.fst new file mode 100644 index 00000000000..a9517fd46c5 --- /dev/null +++ b/tests/dune_hello/Hello.fst @@ -0,0 +1,5 @@ +module Hello + +open FStar.IO + +let _ = print_string "Hi!\n" diff --git a/tests/dune_hello/Makefile b/tests/dune_hello/Makefile new file mode 100644 index 00000000000..d37c40926e1 --- /dev/null +++ b/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!" diff --git a/tests/dune_hello/dune b/tests/dune_hello/dune new file mode 100644 index 00000000000..9c5f8d0da84 --- /dev/null +++ b/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))) +) diff --git a/tests/dune_hello/dune-project b/tests/dune_hello/dune-project new file mode 100644 index 00000000000..6d145823c5f --- /dev/null +++ b/tests/dune_hello/dune-project @@ -0,0 +1,7 @@ +(lang dune 3.8) +(name hello) + +(package + (name hello) + (synopsis "An example F* application") +)