From c13a1e2f789ea6a3bb437c63aece48d1810e0021 Mon Sep 17 00:00:00 2001
From: Amos Robinson <amos.robinson@gmail.com>
Date: Wed, 9 Oct 2024 15:17:02 +1100
Subject: [PATCH] add test for no_inline_let pragma

---
 tests/extraction/Makefile                |  7 ++++++-
 tests/extraction/NoInlineLet.fst         | 11 +++++++++++
 tests/extraction/NoInlineLet.ml.expected |  0
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/extraction/NoInlineLet.fst
 create mode 100644 tests/extraction/NoInlineLet.ml.expected

diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
index 84952c9372c..c7b546a16df 100644
--- a/tests/extraction/Makefile
+++ b/tests/extraction/Makefile
@@ -2,7 +2,7 @@ FSTAR_EXAMPLES=$(realpath ../../examples)
 include $(FSTAR_EXAMPLES)/Makefile.include
 include $(FSTAR_ULIB)/ml/Makefile.include
 
-all: inline_let all_cmi Eta_expand.test Div.test
+all: inline_let all_cmi Eta_expand.test Div.test no_inline_let
 
 %.exe: %.fst | out
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
@@ -25,6 +25,11 @@ inline_let: InlineLet.fst
 	egrep -A 10 test InlineLet.ml | grep -qs "17"
 	@touch $@
 
+no_inline_let: NoInlineLet.fst
+	$(FSTAR) --codegen OCaml NoInlineLet.fst
+	diff -u --strip-trailing-cr NoInlineLet.ml.expected NoInlineLet.ml
+	@touch $@
+
 all_cmi:
 	+$(MAKE) -C cmi all
 
diff --git a/tests/extraction/NoInlineLet.fst b/tests/extraction/NoInlineLet.fst
new file mode 100644
index 00000000000..287e1e2ccc5
--- /dev/null
+++ b/tests/extraction/NoInlineLet.fst
@@ -0,0 +1,11 @@
+module NoInlineLet
+
+let test_no_inline (f: int): int =
+  [@@no_inline_let]
+  let x = f * 2 in
+  x + x
+
+[@preprocess_with (fun i -> norm [delta_only [`%test_no_inline]])]
+let test_preeprocess (f: int): int =
+  let x = test_no_inline f in
+  x
diff --git a/tests/extraction/NoInlineLet.ml.expected b/tests/extraction/NoInlineLet.ml.expected
new file mode 100644
index 00000000000..e69de29bb2d