Merge pull request #3147 from FStarLang/nik_example_cleanup

Cleaning up FStar/examples so that they all build cleanly into .checked files

examples/Makefile

@@ -1,72 +1,69 @@
-include Makefile.include
-
-# Note: native_tactics is not included in the list below, it is called
-# explicitly by the uexamples rule from the Makefile in ../src/Makefile.
-# These examples are excluded since the binary package can't verify
-# them.
-
-# Scheduling these first as some files take very long.
-ALL_EXAMPLE_DIRS += layeredeffects
-ALL_EXAMPLE_DIRS += dsls
-ALL_EXAMPLE_DIRS += data_structures
-
-ALL_EXAMPLE_DIRS += algorithms
-ALL_EXAMPLE_DIRS += calc
-ALL_EXAMPLE_DIRS += crypto
-ALL_EXAMPLE_DIRS += demos
-ALL_EXAMPLE_DIRS += doublylinkedlist
-ALL_EXAMPLE_DIRS += generic
-ALL_EXAMPLE_DIRS += indexed_effects
-ALL_EXAMPLE_DIRS += low-mitls-experiments
-ALL_EXAMPLE_DIRS += maths
-ALL_EXAMPLE_DIRS += metatheory
-ALL_EXAMPLE_DIRS += misc
-ALL_EXAMPLE_DIRS += oplss2021
-ALL_EXAMPLE_DIRS += paradoxes
-ALL_EXAMPLE_DIRS += param
-ALL_EXAMPLE_DIRS += preorders
-ALL_EXAMPLE_DIRS += printf
-ALL_EXAMPLE_DIRS += regional
-ALL_EXAMPLE_DIRS += rel
-ALL_EXAMPLE_DIRS += sequence
-ALL_EXAMPLE_DIRS += software_foundations
-ALL_EXAMPLE_DIRS += tactics
-ALL_EXAMPLE_DIRS += termination
-ALL_EXAMPLE_DIRS += typeclasses
-ALL_EXAMPLE_DIRS += verifythis
+OTHERFLAGS+=--warn_error -321-274
+all: prep verify special_cases
+
+# Note:
+#
+# * old: examples that are not maintained anymore, though may be worth recovering
+#
+# * hello: the main point of the hello example is to test extraction and build
+#   things in OCaml and F#. So, we handle that separately.
+#
+# * native_tactics: called explicitly by the uexamples rule from
+#	the Makefile in ../src/Makefile and need special rules to build the plugins
+#   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/ 
+
+INCLUDE_PATHS?= \
+	$(filter-out $(EXCLUDE_DIRS),$(shell ls -d */)) \
+	../ucontrib/CoreCrypto/fst \
+	../ucontrib/Platform/fst \
+	$(shell ls -d dsls/*/) \
+	$(shell ls -d verifythis/*/) \
+	$(shell ls -d demos/*/) \
+	tactics/eci19
+
+include Makefile.common
+
+verify: prep $(filter-out $(CACHE_DIR)/Launch.fst.checked, $(ALL_CHECKED_FILES))
 
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))
-ALL_EXAMPLE_DIRS += hello
-ALL_EXAMPLE_DIRS += extraction
+SPECIAL_CASES += hello
+SPECIAL_CASES += native_tactics
 endif
 
 ifdef KRML_HOME
-ALL_EXAMPLE_DIRS += kv_parsing
-ALL_EXAMPLE_DIRS += miniparse
-endif
-
-ifneq (,$(CHECK_OLD_EXAMPLES))
-ALL_EXAMPLE_DIRS += old/csl
-ALL_EXAMPLE_DIRS += old/seplogic
+SPECIAL_CASES += kv_parsing
+SPECIAL_CASES += miniparse
 endif
 
-# low-level \  ... NS: removing from CI for this branch
-
-all: $(addsuffix .all, $(ALL_EXAMPLE_DIRS))
+special_cases: $(addsuffix .all, $(SPECIAL_CASES))
+	$(MAKE) -C semiring CanonCommSemiring.native
 
 %.all: %
 	+$(MAKE) -C $^ all
 
-test: all
-
-stdlib: $(addprefix ../lib/, FStar.List.fst FStar.String.fsti partialmap.fst FStar.ST.fst)
-	mkdir -p ../cache
-	$(FSTAR) $^ --serialize_mods
+prep:
+	mkdir -p $(OUTPUT_DIRECTORY) $(CACHE_DIR)
 
-clean:
-	rm ../cache/*.cache
+FILTER_OUT = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
 
 wc:
-	find . -name "*.fst" | grep -v -e to_be_ported | xargs sloccount
+	wc -l $(call FILTER_OUT,ulib, $(ALL_FST_FILES) $(ALL_FSTI_FILES))
+
+clean: $(addsuffix .clean, $(SPECIAL_CASES))
+	rm -rf $(OUTPUT_DIRECTORY) $(CACHE_DIR) .depend
+
+%.clean: %
+	+$(MAKE) -C $^ clean
+
+.PHONY: prep clean special_cases wc
+

examples/algorithms/Coincidence.fst

@@ -37,7 +37,7 @@ let rec sorted l =
 
 
 val lemma1 : y:int -> xs:list int ->
-  Lemma (requires (sorted xs && (xs = [] || y < Cons.hd xs)))
+  Lemma (requires (sorted xs && (xs = [] || y < Cons?.hd xs)))
         (ensures (not (mem y xs)))
 let rec lemma1 y xs =
   match xs with

examples/algorithms/Makefile

@@ -31,29 +31,3 @@ intersect-ocaml: out IntervalIntersect.fst
 
 out:
 	mkdir -p out
-
-# $ ocaml
-#         OCaml version 4.03.0
-
-# # #use "topfind";;
-# - : unit = ()
-# Findlib has been successfully loaded. Additional directives:
-#   #require "package";;      to load a package
-#   #list;;                   to list the available packages
-#   #camlp4o;;                to load camlp4 (standard syntax)
-#   #camlp4r;;                to load camlp4 (revised syntax)
-#   #predicates "p,q,...";;   to set these predicates
-#   Topfind.reset();;         to force that packages will be reloaded
-#   #thread;;                 to enable threads
-
-# - : unit = ()
-# # #require "unix";;
-# /Users/jonathan/.opam/4.03.0/lib/ocaml/unix.cma: loaded
-# # #require "zarith";;
-# /Users/jonathan/.opam/4.03.0/lib/zarith: added to search path
-# /Users/jonathan/.opam/4.03.0/lib/zarith/zarith.cma: loaded
-# # #require "stdint";;
-# /Users/jonathan/.opam/4.03.0/lib/bytes: added to search path
-# /Users/jonathan/.opam/4.03.0/lib/stdint: added to search path
-# /Users/jonathan/.opam/4.03.0/lib/stdint/stdint.cma: loaded
-# # #require "batteries";;

examples/dm4free/FStar.DM4F.Heap.ST.fst

@@ -26,4 +26,5 @@ module FStar.DM4F.Heap.ST
 open FStar.DM4F.Heap
 open FStar.DM4F.ST
 
+let refine_st #a = admit()
 let runST #a #post s = fst (reify (s ()) FStar.DM4F.Heap.emp)