WIP: tests/examples

examples/Makefile

@@ -1,3 +1,7 @@
+FSTAR_ROOT ?= ..
+include $(FSTAR_ROOT)/mk/common.mk
+.DEFAULT_GOAL := all
+
 OTHERFLAGS+=--warn_error -321-274 --ext context_pruning
 all: prep verify special_cases
 
@@ -16,28 +20,13 @@ all: prep verify special_cases
 #   for them to run. Also, these examples are excluded since the binary package
 #   can't verify them.
 #
-# * kv_parsing: Needs Krml to build
-#
-# * miniparse: Needs Krml to build
-
 
-EXCLUDE_DIRS=old/ hello/ native_tactics/ kv_parsing/ miniparse/ sample_project/
-
-# F* contrib directory needed by crypto/ . Since this Makefile
-# supersedes crypto/Makefile, we need to determine the location of the
-# F* contrib directory here.
-ifdef FSTAR_HOME
-FSTAR_UCONTRIB = $(shell if test -d $(FSTAR_HOME)/ucontrib ; then echo $(FSTAR_HOME)/ucontrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi)
-else
-   # FSTAR_HOME not defined, assume fstar.exe installed through opam
-   # or binary package, and reachable from PATH
-FSTAR_UCONTRIB=$(dir $(shell which fstar.exe))/../share/fstar/contrib
-endif
+EXCLUDE_DIRS=old/ hello/ native_tactics/ sample_project/
 
 INCLUDE_PATHS?= \
 	$(filter-out $(EXCLUDE_DIRS),$(shell ls -d */)) \
-	$(FSTAR_UCONTRIB)/CoreCrypto/fst \
-	$(FSTAR_UCONTRIB)/Platform/fst \
+	$(FSTAR_HOME)/ucontrib/CoreCrypto/fst \
+	$(FSTAR_HOME)/ucontrib/Platform/fst \
 	$(shell ls -d dsls/*/) \
 	$(shell ls -d verifythis/*/) \
 	tactics/eci19
@@ -58,10 +47,6 @@ SPECIAL_CASES += hello
 SPECIAL_CASES += native_tactics
 endif
 
-KRML_TESTS += demos
-KRML_TESTS += kv_parsing
-KRML_TESTS += miniparse
-
 special_cases: $(addsuffix .all, $(SPECIAL_CASES))
 
 krml_tests: $(addsuffix .all, $(KRML_TESTS))

examples/Makefile.common

@@ -1,22 +1,10 @@
-ifdef FSTAR_HOME
-  FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi)
-else
-  # FSTAR_HOME not defined, assume fstar.exe installed through opam
-  # or binary package, and reachable from PATH
-  FSTAR_ULIB=$(dir $(shell which fstar.exe))/../lib/fstar
-endif
-include $(FSTAR_ULIB)/gmake/z3.mk
-include $(FSTAR_ULIB)/gmake/fstar.mk
-
-#for getting macros for OCaml commands to compile extracted code
-include $(FSTAR_ULIB)/ml/Makefile.include
-
-ifdef FSTAR_HOME
-  -include $(FSTAR_HOME)/.common.mk
-  FSTAR=$(FSTAR_HOME)/bin/fstar.exe
-else
-  FSTAR=fstar.exe
-endif
+## FIXME: this thing should either be internal
+## or external, we cannot serve both.
+
+FSTAR_HOME ?= ..
+
+include $(FSTAR_HOME)/mk/common.mk
+include $(FSTAR_HOME)/gmake/fstar.mk
 
 #################################################################################
 # Customize these variables for your project
@@ -53,7 +41,7 @@ MAYBE_HINTS = $(if $(HINTS),--use_hints)
 # YOU SHOULDN'T NEED TO TOUCH THE REST
 ################################################################################
 
-VERBOSE_FSTAR=$(BENCHMARK_PRE) $(FSTAR)                     \
+VERBOSE_FSTAR=$(BENCHMARK_PRE) $(FSTAR_EXE)                     \
 		  --cache_checked_modules                   \
 		  --odir $(OUTPUT_DIRECTORY)                \
 		  --cache_dir $(CACHE_DIR)                  \

examples/Makefile.include

@@ -1,25 +1,8 @@
-# --------------------------------------------------------------------
-ifdef FSTAR_HOME
-   -include $(FSTAR_HOME)/.common.mk
-   FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi)
-else
-   # FSTAR_HOME not defined, assume fstar.exe installed through opam
-   # or binary package, and reachable from PATH
-   FSTAR_ULIB=$(dir $(shell which fstar.exe))/../lib/fstar
-endif
+FSTAR_HOME ?= ..
+include $(FSTAR_HOME)/mk/common.mk
+include $(FSTAR_HOME)/gmake/fstar.mk
 
-include $(FSTAR_ULIB)/gmake/z3.mk
-include $(FSTAR_ULIB)/gmake/fstar.mk
-
-ifeq ($(OS),Windows_NT)
-  ifndef FSTAR_HOME
-     $(error "Please define the `FSTAR_HOME` variable before including this makefile.")
-  endif
-  MSBUILD = $(FSTAR_HOME)/src/msbuild.bat
-else
-  # If can't find msbuild, use xbuild, but throw a warning
-  MSBUILD = $(shell which msbuild || (echo '\n\n\033[0;31mWarning:\033[0m could not find "msbuild", trying (deprecated) "xbuild"\n\n'>&2; which xbuild))
-endif
+OCAMLOPT=OCAMLPATH="$(shell $(FSTAR_EXE) --locate_ocaml)" ocamlfind opt
 
 # we ignore the return result in benchmark runs because we can have micro-benchmarks which
 # produce error asserts when executed with '--admit_smt_queries true'

examples/algorithms/Makefile

@@ -1,33 +1,26 @@
-include ../Makefile.include
-
-include $(FSTAR_ULIB)/ml/Makefile.include
-
-all: uall
-
-uall: BinarySearch.uver IntSort.uver InsertionSort.uver MergeSort.uver QuickSort.List.uver QuickSort.Seq.uver GC.uver Unification.uver Huffman.uver QuickSort.Array.uver IntervalIntersect.uver #downgrade  //TODO
-
-downgrade: QuickSort.Array.fst downgrade.fst
-	$(FSTAR) --include $(FSTAR_ULIB)/reclaimable downgrade.fst
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+all: verify-all
 
 # TODO: restore this OCaml extraction
 
-include $(FSTAR_ULIB)/ml/Makefile.include
+# include $(FSTAR_ULIB)/ml/Makefile.include
 
-huffman-ocaml: out Huffman.fst
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Huffman.fst
-	$(OCAMLOPT) -I out out/FStar_List_Tot_Base.ml out/Huffman.ml -o Huffman.exe
-	./Huffman.exe
+# huffman-ocaml: out Huffman.fst
+# 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Huffman.fst
+# 	$(OCAMLOPT) -I out out/FStar_List_Tot_Base.ml out/Huffman.ml -o Huffman.exe
+# 	./Huffman.exe
 
-OCAML_DEFAULT_FLAGS=
-huffman-ocaml-repl: out Huffman.fst
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Huffman.fst
-	$(OCAMLC) -I out $(ULIB_ML)/prims.ml out/FStar_List_Tot_Base.ml out/Huffman.ml -o Huffman.exe        
-	utop -I out -I $(ULIB_ML) Huffman.repl
+# OCAML_DEFAULT_FLAGS=
+# huffman-ocaml-repl: out Huffman.fst
+# 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Huffman.fst
+# 	$(OCAMLC) -I out $(ULIB_ML)/prims.ml out/FStar_List_Tot_Base.ml out/Huffman.ml -o Huffman.exe        
+# 	utop -I out -I $(ULIB_ML) Huffman.repl
 
-intersect-ocaml: out IntervalIntersect.fst
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract 'IntervalIntersect' IntervalIntersect.fst
-	$(OCAMLOPT) out/IntervalIntersect.ml -o IntervalIntersect.exe
-	./IntervalIntersect.exe
+# intersect-ocaml: out IntervalIntersect.fst
+# 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract 'IntervalIntersect' IntervalIntersect.fst
+# 	$(OCAMLOPT) out/IntervalIntersect.ml -o IntervalIntersect.exe
+# 	./IntervalIntersect.exe
 
-out:
-	mkdir -p out
+# out:
+# 	mkdir -p out

examples/data_structures/Makefile

@@ -1,23 +1,12 @@
-FSTAR_FILES = $(wildcard *.fst)
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 
-all: verify-all
-
-include ../Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+all: verify-all $(OUTPUT_DIR)/test.exe
 
 EXTRACT = RBTreeIntrinsic
 
-OCAML_DEFAULT_FLAGS += -I $(OUTPUT_DIRECTORY) -w -31
+OCAML_DEFAULT_FLAGS += -I $(OUTPUT_DIR) -w -31
 
-$(OUTPUT_DIRECTORY)/test.exe: $(OUTPUT_DIRECTORY)/$(EXTRACT).ml | $(OUTPUT_DIRECTORY)
+$(OUTPUT_DIR)/test.exe: $(OUTPUT_DIR)/$(EXTRACT).ml | $(OUTPUT_DIR)
 	@echo 'let _ = test()' >> $^
-	$(OCAMLC) -o $(OUTPUT_DIRECTORY)/test.exe $^
-
-test: $(OUTPUT_DIRECTORY)/test.exe
-	$(OUTPUT_DIRECTORY)/test.exe
-
-clean:
-	rm -rf $(OUTPUT_DIRECTORY) $(CACHE_DIR) .depend
-
-.PHONY: depend verify-all test clean
+	$(OCAMLOPT) -package fstar_lib -linkpkg -o $(OUTPUT_DIR)/test.exe $^

examples/hello/Makefile

@@ -1,22 +1,22 @@
+FSTAR_HOME ?= ../..
+include $(FSTAR_HOME)/mk/common.mk
 include ../Makefile.include
 
-include $(FSTAR_ULIB)/ml/Makefile.include
-
 all: hello testseq multi strings
 
 hello: out Hello/Hello.fst
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract 'Hello' Hello/Hello.fst
-	$(OCAMLOPT) out/Hello.ml -o hello.exe
+	$(OCAMLOPT) -linkpkg -package fstar_lib out/Hello.ml -o hello.exe
 	./hello.exe
 
 testseq: out TestSeq/TestSeq.fst
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract 'TestSeq' TestSeq/TestSeq.fst
-	$(OCAMLOPT) out/TestSeq.ml -o testseq.exe
+	$(OCAMLOPT) -linkpkg -package fstar_lib out/TestSeq.ml -o testseq.exe
 	./testseq.exe
 
 strings: out strings/TestStrings.fst
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract 'TestStrings' strings/TestStrings.fst
-	$(OCAMLOPT) out/TestStrings.ml -o teststrings.exe
+	$(OCAMLOPT) -linkpkg -package fstar_lib out/TestStrings.ml -o teststrings.exe
 
 multi:
 	$(MAKE) -C multifile

examples/hello/multifile/Makefile

@@ -6,16 +6,6 @@ MAIN=Main.fst #this is the main entry point file of your project
 EXECUTABLE=$(subst .fst,.exe, $(MAIN))
 INCLUDE_PATHS=
 
-ifdef FSTAR_HOME
-  ifeq ($(OS),Windows_NT)
-    FSTAR_EXE := $(shell cygpath -m $(FSTAR_HOME)/bin/fstar.exe)
-  else
-    FSTAR_EXE := $(FSTAR_HOME)/bin/fstar.exe
-  endif
-else
-  FSTAR_EXE := fstar.exe
-endif
-
 #cache_dir: where to find checked files
 #odir: where to put all output artifacts
 #include: where to find source and checked files

examples/hello/multifile/output/Makefile

@@ -7,8 +7,9 @@
 #   endif
 # endif
 
-FSTAR_OCAML := $(shell $(FSTAR_HOME)/bin/fstar.exe --locate_ocaml)
+FSTAR_OCAML := $(shell $(FSTAR_EXE) --locate_ocaml)
 OCAMLPATH := $(FSTAR_OCAML):$(OCAMLPATH)
+
 # with dune
 Main.exe: $(wildcard *.ml)
 	OCAMLPATH="$(OCAMLPATH)" dune build

examples/hello/multifile/output/dune

@@ -2,8 +2,7 @@
 (executable
   (name Main)
   (libraries
-    batteries
-    fstar.lib
+    fstar_lib
   )
   (preprocess (pps ppx_deriving_yojson))
   (flags (:standard -w -8-9-11-26-27-33-39))

examples/native_tactics/Makefile

@@ -1,5 +1,7 @@
-FSTAR_HOME=../..
-FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
+FSTAR_HOME ?= ../..
+include $(FSTAR_HOME)/mk/common.mk
+
+FSTAR=$(FSTAR_EXE) $(SIL) $(OTHERFLAGS)
 
 # Tests for which the native tactics used in module named Sample.Test.fst are
 # declared in a corresponding module named Sample.fst
@@ -33,10 +35,12 @@ ALL=Apply\
     Rename\
     Retype\
     Sequences\
-    Simplifier\
     Tutorial\
     Unify
 
+# FIXME: Add back
+    # Simplifier\
+
 OTHERFLAGS +=
 
 all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
@@ -50,24 +54,29 @@ all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
 .PRECIOUS: %.ml
 
 %.test: %.fst %.ml
+	$(call msg, "CHECK", $<)
 	$(FSTAR) $*.fst --load $*
-	touch $@
+	touch -c $@
 
 %.sep.test: %.fst %.ml
+	$(call msg, "CHECK", $<)
 	$(FSTAR) $*.Test.fst --load $*
-	touch $@
+	touch -c $@
 
 %.ml: %.fst
+	$(call msg, "EXTRACT", $<)
 	$(FSTAR) $*.fst --cache_checked_modules --codegen Plugin --extract $*
 	touch $@
 
 %.clean:
 	rm -f Registers_List.ml Registers.List.ml Registers_List.cmxs
 
 %.native: %.fst Registers.List.ml
+	$(call msg, "NATIVE", $<)
 	$(FSTAR) $*.fst --load Registers.List --warn_error -266
 
 %.interp: %.fst Registers.List.fst
+	$(call msg, "INTERP", $<)
 	$(FSTAR) $*.fst
 
 

mk/test.mk

@@ -5,7 +5,7 @@ include $(FSTAR_ROOT)/mk/common.mk
 .DEFAULT_GOAL := all
 
 # Set a default FSTAR_EXE for most clients.
-FSTAR_EXE ?= $(FSTAR_ROOT)/bin/fstar.exe
+FSTAR_EXE ?= $(FSTAR_ROOT)/out/bin/fstar.exe
 
 OCAMLOPT := $(FSTAR_EXE) --ocamlenv ocamlfind opt
 

tests/bug-reports/Makefile.include

@@ -1,7 +1,7 @@
 FSTAR_EXE ?= ../../bin/fstar.exe
 FSTAR_ROOT ?= ../..
 include $(FSTAR_ROOT)/mk/common.mk
-include $(FSTAR_ROOT)/ulib/gmake/fstar.mk
+include $(FSTAR_ROOT)/gmake/fstar.mk
 
 # we ignore the return result in benchmark runs because we can have micro-benchmarks which
 # produce error asserts when executed with '--admit_smt_queries true'

tests/dune_hello/Makefile

@@ -1,4 +1,4 @@
-FSTAR_EXE ?= ../../bin/fstar.exe
+FSTAR_EXE ?= ../../out/bin/fstar.exe
 
 .PHONY: all
 all: run

tests/dune_hello/dune

@@ -1,6 +1,6 @@
 (executable
  (name hello)
  (public_name hello.exe)
- (libraries fstar.lib)
+ (libraries fstar_lib)
  (modes native)
 )

tests/extraction/Makefile

@@ -6,7 +6,7 @@ all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test
 
 %.exe: %.fst
 	$(FSTAR) --codegen OCaml $<
-	$(OCAMLOPT) -package fstar.lib -linkpkg $(OUTPUT_DIR)/$(patsubst %.fst,%.ml,$<) -o $@
+	$(OCAMLOPT) -package fstar_lib -linkpkg $(OUTPUT_DIR)/$(patsubst %.fst,%.ml,$<) -o $@
 
 %.test: %.exe
 	$(call msg,RUN,$<)

tests/machine_integers/Makefile

@@ -14,7 +14,7 @@ accept: $(patsubst %.fst,%.run-accept,$(FSTAR_FILES))
 	$(eval B := $(patsubst %.exe,%,$@))
 	$(Q)$(FSTAR) --odir out --codegen OCaml --extract '${B}' '${B}.fst'
 	$(Q)/bin/echo -e '\n\nlet _ = main ()\n' >> out/${B}.ml
-	$(Q)$(OCAMLOPT) -package fstar.lib -linkpkg out/${B}.ml -o $@
+	$(Q)$(OCAMLOPT) -package fstar_lib -linkpkg out/${B}.ml -o $@
 
 %.out: %.exe
 	$(call msg, "OUTPUT", $(notdir $@))

tests/semiring/CanonCommSemiring.ml.fixup

@@ -2,6 +2,7 @@
 (* ^ Empty line above since extracted files may not have a newline at the end. *)
 (* This is needed since we have no automatic embeddings for Tac functions, but we
 should add them *)
+open Fstar_guts
 let _ =
   FStarC_Tactics_Native.register_tactic "CanonCommSemiring.canon_semiring_aux"
     (Prims.parse_int "11")

tests/simple_hello/Makefile

@@ -2,7 +2,7 @@
 # We should not need to include any other internal makefiles.
 # Dune also works fine under the --ocamlenv.
 
-FSTAR ?= ../../bin/fstar.exe
+FSTAR ?= ../../out/bin/fstar.exe
 
 all: Hello.test