Update share/, split some of it into test/

share/pulse/Makefile

@@ -1,15 +1,4 @@
-TARGETS=examples
+SUBDIRS += examples
 
-all: $(TARGETS)
-
-$(TARGETS): %:
-	+$(MAKE) -C $@
-
-.PHONY: all $(TARGETS)
-
-.PHONY: install %.install
-
-%.install: %
-	$(INSTALL) -m 644 -D $< $(PREFIX)/share/pulse/$<
-
-install: $(addsuffix .install,Makefile.locate-fstar Makefile.include-base Makefile.include)
+PULSE_ROOT ?= ../..
+include $(PULSE_ROOT)/mk/test.mk

share/pulse/examples/Makefile

@@ -1,66 +1,7 @@
-PULSE_HOME ?= ../../..
-PULSE_SHARE = $(PULSE_HOME)/share/pulse
+SUBDIRS += by-example
+SUBDIRS += c
+SUBDIRS += dice
+SUBDIRS += parallel
 
-SRC_DIRS = bug-reports by-example parallel parix c .
-INCLUDE_PATHS += $(PULSE_HOME)/lib/pulse/c
-OUTPUT_DIRECTORY=_output
-CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache
-
-.PHONY: all
-all: verify test dice
-
-include $(PULSE_SHARE)/Makefile.include
-
-.PHONY: dice
-dice:
-	+$(MAKE) -C dice
-
-$(OUTPUT_DIRECTORY)/Example_Hashtable.c: $(addprefix $(OUTPUT_DIRECTORY)/,\
-	FStar_Pervasives.krml FStar_Pervasives_Native.krml \
-	Pulse_Lib_Vec.krml \
-	Pulse_Lib_HashTable_Type.krml Pulse_Lib_HashTable_Spec.krml Pulse_Lib_HashTable.krml)
-
-$(OUTPUT_DIRECTORY)/Example_Slice.c: $(addprefix $(OUTPUT_DIRECTORY)/,\
-	Pulse_Lib_Slice.krml)
-
-$(OUTPUT_DIRECTORY)/Example_Unreachable.c: $(addprefix $(OUTPUT_DIRECTORY)/,FStar_Pervasives.krml FStar_Pervasives_Native.krml)
-
-$(OUTPUT_DIRECTORY)/%.c: $(EXTRA_KRML_DEPS) $(OUTPUT_DIRECTORY)/%.krml
-	$(KRML_HOME)/krml -bundle $*=* $(EXTRA_KRML_OPTS) -skip-linking $+ -tmpdir $(OUTPUT_DIRECTORY)
-
-.PHONY: extract
-extract: $(OUTPUT_DIRECTORY)/ExtractionTest.ml
-
-.PHONY: extract_unreachable
-extract_unreachable: $(OUTPUT_DIRECTORY)/Example_Unreachable.ml
-
-EXTRACT_C_FILES = $(addprefix $(OUTPUT_DIRECTORY)/,ExtractionTest.c PulsePointStruct.c Bug166.c Example_Unreachable.c Example_Hashtable.c Example_Slice.c)
-
-ifneq (,$(KRML_HOME))
-test-dpe-c: dice
-	+$(MAKE) -C dice test-c
-
-test-cbor: dice
-	+$(MAKE) -C dice/cbor
-
-else
-test-dpe-c:
-
-test-cbor:
-
-EXTRACT_C_FILES =
-
-endif
-
-extract_c: $(EXTRACT_C_FILES)
-
-test: test-cbor extract extract_pulse_c extract_c test-dpe-c test-error-messages
-
-test-error-messages:
-	+$(MAKE) -C bug-reports/error-messages
-
-.PHONY: test-dpe-c test-error-messages
-
-.PHONY: extract_pulse_c extract_c
-
-.PHONY: test test-cbor test-cbor-raw
+PULSE_ROOT ?= ../../..
+include $(PULSE_ROOT)/mk/test.mk

share/pulse/examples/by-example/Makefile

@@ -0,0 +1,2 @@
+PULSE_ROOT ?= ../../../..
+include $(PULSE_ROOT)/mk/test.mk

share/pulse/examples/c/Makefile

@@ -0,0 +1,2 @@
+PULSE_ROOT ?= ../../../..
+include $(PULSE_ROOT)/mk/test.mk

share/pulse/examples/dice/Makefile

@@ -1,18 +1,31 @@
-PULSE_HOME ?= ../../../..
-PULSE_EXAMPLES_ROOT = $(PULSE_HOME)/share/pulse/examples
-OUTPUT_DIRECTORY=_output
-CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache
-SRC_DIRS = dpe engine l0 external external/hacl external/l0
-INCLUDE_PATHS += cbor
-#/Pulse.Lib.HashTable.fst
-FSTAR_OPTIONS += --warn_error -342
-FSTAR_DEP_OPTIONS=--extract '* -FStar.Tactics -FStar.Reflection -Pulse +Pulse.Class +Pulse.Lib -Pulse.Lib.Core'
+# PULSE_HOME ?= ../../../..
+# PULSE_EXAMPLES_ROOT = $(PULSE_HOME)/share/pulse/examples
+# OUTPUT_DIRECTORY=_output
+# CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache
+# SRC_DIRS = dpe engine l0 external external/hacl external/l0
+# INCLUDE_PATHS += cbor
+# #/Pulse.Lib.HashTable.fst
+# FSTAR_OPTIONS += --warn_error -342
+# FSTAR_DEP_OPTIONS=--extract '* -FStar.Tactics -FStar.Reflection -Pulse +Pulse.Class +Pulse.Lib -Pulse.Lib.Core'
+# all: verify
 
-.PHONY: all test-c
-all: verify
+# include $(PULSE_HOME)/share/pulse/Makefile.include
 
-include $(PULSE_HOME)/share/pulse/Makefile.include
+# .PHONY: test-c
+# test-c: verify
+#         +$(MAKE) -f c.Makefile
 
-.PHONY: test-c
-test-c: verify
-	+$(MAKE) -f c.Makefile
+
+# NOTE!!!!: no subdirs, we just rely on fstar.include
+# Otherwise we need to state cross-dependencies in each of them,
+# SUBDIRS += cbor
+# SUBDIRS += dpe
+# SUBDIRS += engine
+# SUBDIRS += l0
+# SUBDIRS += external
+
+# Start dep analysis from every file under here.
+FSTAR_FILES != find . -name '*.fst' -o -name '*.fsti'
+
+PULSE_ROOT ?= ../../../..
+include $(PULSE_ROOT)/mk/test.mk

share/pulse/examples/dice/external/Makefile

@@ -1,19 +1,19 @@
-PULSE_HOME ?= ../../../../..
-OUTPUT_DIRECTORY=_output
-CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache
-INCLUDE_PATHS += .. hacl
-ifneq (,$(wildcard ../../_output/cache))
-  INCLUDE_PATHS += ../../_output/cache
-endif
-ALREADY_CACHED_LIST = *,-HACL,-EverCrypt,-Spec.Hash.Definitions
-FSTAR_OPTIONS += --warn_error -342
-FSTAR_DEP_OPTIONS=--extract '+EverCrypt'
-all: verify extract
+# PULSE_HOME ?= ../../../../..
+# OUTPUT_DIRECTORY=_output
+# CACHE_DIRECTORY=$(OUTPUT_DIRECTORY)/cache
+# INCLUDE_PATHS += .. hacl
+# ifneq (,$(wildcard ../../_output/cache))
+#   INCLUDE_PATHS += ../../_output/cache
+# endif
+# ALREADY_CACHED_LIST = *,-HACL,-EverCrypt,-Spec.Hash.Definitions
+# FSTAR_OPTIONS += --warn_error -342
+# FSTAR_DEP_OPTIONS=--extract '+EverCrypt'
+# all: verify extract
 
-include $(PULSE_HOME)/share/pulse/Makefile.include
+# include $(PULSE_HOME)/share/pulse/Makefile.include
 
-KRML ?= $(KRML_HOME)/krml
+# KRML ?= $(KRML_HOME)/krml
 
-.PHONY: extract
-extract: $(ALL_KRML_FILES)
-	$(KRML) -skip-makefiles -skip-compilation -bundle 'EverCrypt.Hash.Incremental=Spec.Hash.Definitions[rename=EverCrypt_Hash]' -warn-error @4 -tmpdir $(OUTPUT_DIRECTORY) -add-include '"EverCrypt_Base.h"' $^
+# .PHONY: extract
+# extract: $(ALL_KRML_FILES)
+#         $(KRML) -skip-makefiles -skip-compilation -bundle 'EverCrypt.Hash.Incremental=Spec.Hash.Definitions[rename=EverCrypt_Hash]' -warn-error @4 -tmpdir $(OUTPUT_DIRECTORY) -add-include '"EverCrypt_Base.h"' $^