doc: restore and add to test

Makefile

@@ -359,14 +359,22 @@ unit-tests: _unit-tests
 
 # Use directly only at your own risk.
 _test: FSTAR_EXE ?= $(abspath out/bin/fstar.exe)
-_test: _unit-tests _examples
+_test: _unit-tests _examples _doc
 
 need_fstar_exe:
 	if [ -z "$(FSTAR_EXE)" ]; then \
 		echo "This rule needs FSTAR_EXE defined."; \
 		false; \
 	fi
 
+_doc: _doc_book_code _doc_old_tutorial
+
+_doc_book_code: need_fstar_exe _force
+	+$(MAKE) -C doc/book/code FSTAR_EXE=$(FSTAR_EXE)
+
+_doc_old_tutorial: need_fstar_exe _force
+	+$(MAKE) -C doc/old/tutorial regressions FSTAR_EXE=$(FSTAR_EXE)
+
 _unit-tests: need_fstar_exe _force
 	+$(MAKE) -C tests all FSTAR_EXE=$(FSTAR_EXE)
 

doc/.gitignore

@@ -0,0 +1,2 @@
+_output
+_cache

doc/book/code/Makefile

@@ -1,32 +1,22 @@
-include ../../Makefile.include
+FSTAR_ROOT ?= ../../..
+include $(FSTAR_ROOT)/mk/test.mk
 
-EXCLUDE_FILES = ContextPollution.fst
-FSTAR_FILES := $(filter-out $(EXCLUDE_FILES),$(wildcard *.fst *.fsti))
-OTHERFLAGS  := --cache_checked_modules $(OTHERFLAGS)
+FSTAR_FILES := $(filter-out ContextPollution.fst,$(FSTAR_FILES))
 
-all: $(addsuffix .checked, $(FSTAR_FILES))
-	$(MAKE) -C exercises
-
-.depend:
-	$(FSTAR) --dep full $(FSTAR_FILES) --output_deps_to .depend
-
-.DELETE_ON_ERROR:
-include .depend
+# Disable context pruning for this file, fails otherwise.
+$(CACHE_DIR)/Alex.fst.checked: OTHERFLAGS += --ext context_pruning=
 
-depend: .depend
+exercises:
+	$(MAKE) -C exercises
 
-%.checked:
-	$(FSTAR) --already_cached '+Prims +FStar +LowStar' $<
-	touch -c $@
+all: exercises
 
 wc:
 	# Prims.fst seems to be missing here?
 	wc -l Prims.fst $(ALL)
 
-
 extract:
 	krml -skip-compilation MemCpy.fst -tmpdir out
 
 clean:
-	rm -rf *.c *.h *~ *.checked *.checked.lax *.krml .depend
 	$(MAKE) -C exercises clean

doc/book/code/exercises/Makefile

@@ -1,27 +1,2 @@
-include ../../../Makefile.include
-
-FSTAR_FILES := $(wildcard *fst *fsti)
-OTHERFLAGS  := --cache_checked_modules $(OTHERFLAGS)
-
-all: $(addsuffix .checked, $(FSTAR_FILES))
-
-.depend:
-	$(FSTAR) --dep full $(FSTAR_FILES) --output_deps_to .depend
-
-depend: .depend
-
--include .depend
-
-%.checked:
-	$(FSTAR) --already_cached '+Prims +FStar +LowStar' $<
-	touch -c $@
-
-wc:
-	wc -l Prims.fst $(ALL)
-
-
-extract:
-	krml -skip-compilation MemCpy.fst -tmpdir out
-
-clean:
-	rm -rf *.c *.h *~ *.checked *.checked.lax *.krml .depend
+FSTAR_ROOT ?= ../../../..
+include $(FSTAR_ROOT)/mk/test.mk

doc/old/tutorial/code/exercises/Makefile

@@ -1,4 +1,11 @@
-VERFILES=Ex01a.fst \
+FSTAR_ROOT ?= ../../../../../
+FSTAR_CONTRIB := $(FSTAR_ROOT)/contrib
+OTHERFLAGS += --include $(FSTAR_CONTRIB)/Platform/fst --include $(FSTAR_CONTRIB)/CoreCrypto/fst
+
+# exercises have val without definitions, by design
+OTHERFLAGS += --warn_error -240
+
+FSTAR_FILES := Ex01a.fst \
 Ex02a.fst \
 Ex03a.fst \
 Ex03b.fst \
@@ -34,39 +41,7 @@ LowStar.Ex1.fst \
 LowStar.Ex2.fst \
 LowStar.Ex3.fst
 
-include ../../../../Makefile.include
-
-# exercises have val without definitions, by design
-OTHERFLAGS+=--warn_error -240
-
-verify-%: __force__
-	$(FSTAR) --include $(FSTAR_CONTRIB)/Platform/fst --include $(FSTAR_CONTRIB)/CoreCrypto/fst $*
-
-
-all: uall sall
-
-sall:
-
-uall: $(VERFILES:%=verify-%)
-
-# Importing targets for simplified extraction to Ocaml
-
-include $(FSTAR_ULIB)/ml/Makefile.include
-
-out:
-	mkdir -p out
-
-
-HAS_OCAMLFIND := $(shell which ocamlfind 2>/dev/null)
-
-Ex01a-ocaml: out Ex01a.fst
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Ex01a.fst
-ifdef HAS_OCAMLFIND
-	$(OCAMLOPT) out/Ex01a.ml -o Ex01a.exe
-	-./Ex01a.exe
-endif
+include $(FSTAR_ROOT)/mk/test.mk
 
-# # Parameter for interactive mode
-# %.fst-in: 
-# 	@echo $(OPTIONS) \
-# 	--include $(FSTAR_HOME)/ulib/hyperstack \
+Ex01a-ocaml: $(OUTPUT_DIR)/Ex01a.exe
+	-./$(OUTPUT_DIR)/Ex01a.exe

doc/old/tutorial/code/solutions/Makefile

@@ -1,5 +1,8 @@
-VERFILES= \
-Ex01a.fst \
+FSTAR_ROOT ?= ../../../../../
+FSTAR_CONTRIB := $(FSTAR_ROOT)/contrib
+OTHERFLAGS += --include $(FSTAR_CONTRIB)/Platform/fst --include $(FSTAR_CONTRIB)/CoreCrypto/fst
+
+FSTAR_FILES := Ex01a.fst \
 Ex02a.fst \
 Ex03a.fst \
 Ex03b.fst \
@@ -43,35 +46,7 @@ LowStar.Ex1.fst \
 LowStar.Ex2.fst \
 LowStar.Ex3.fst
 
-include ../../../../Makefile.include
-
-verify-%: __force__
-	$(FSTAR) --include $(FSTAR_CONTRIB)/Platform/fst --include $(FSTAR_CONTRIB)/CoreCrypto/fst $*
-
-all: uall sall Ex01a-ocaml
-
-sall:
-
-uall: $(VERFILES:%=verify-%)
-
-
-# Importing targets for simplified extraction to Ocaml
-
-include $(FSTAR_ULIB)/ml/Makefile.include
-
-out:
-	mkdir -p out
-
-HAS_OCAMLFIND := $(shell which ocamlfind 2>/dev/null)
-
-Ex01a-ocaml: out Ex01a.fst
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml Ex01a.fst
-ifdef HAS_OCAMLFIND
-	$(OCAMLOPT) out/Ex01a.ml -o Ex01a.exe 2>&1
-	-./Ex01a.exe 2>&1
-endif
+include $(FSTAR_ROOT)/mk/test.mk
 
-# # Parameter for interactive mode
-# %.fst-in:
-# 	@echo $(OPTIONS) \
-#  	--include $(FSTAR_HOME)/ulib/hyperstack \
+Ex01a-ocaml: $(OUTPUT_DIR)/Ex01a.exe
+	-./$(OUTPUT_DIR)/Ex01a.exe