remove tests/, examples/, doc/ from binary package

Suggested by @nikswamy
FStarLang · Mar 1, 2022 · aef4c7b · aef4c7b
1 parent 89ed54c
commit aef4c7b
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 38 deletions.
diff --git a/.docker/package.Dockerfile b/.docker/package.Dockerfile
@@ -32,21 +32,24 @@ RUN tar xzf fstar.tar.gz
 ENV FSTAR_HOME /home/opam/fstar
 ENV PATH="${FSTAR_HOME}/bin:${PATH}"
 
+# Copy examples and docs
+ADD --chown=opam:opam examples/ fstar_examples/
+ADD --chown=opam:opam doc/ fstar_doc/
+
 # Test the F* binary package
 
 # Case 1: test the fresh package
 FROM fstarbin
-RUN eval $(opam env) && make -C $FSTAR_HOME/tests/micro-benchmarks -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/examples -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
+RUN eval $(opam env) && make -C fstar_examples -j $opamthreads
+RUN eval $(opam env) && make -C fstar_doc/tutorial -j $opamthreads regressions
 
 # Case 2: rebuild ulib and test again
 FROM fstarbin
 RUN eval $(opam env) && make -C $FSTAR_HOME/ulib rebuild -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/examples/hello -j $opamthreads
+RUN eval $(opam env) && make -C fstar_examples/hello -j $opamthreads
 RUN eval $(opam env) && make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/examples -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
+RUN eval $(opam env) && make -C fstar_examples -j $opamthreads
+RUN eval $(opam env) && make -C fstar_doc/tutorial -j $opamthreads regressions
 
 # Test the fresh package without OCaml
 FROM ubuntu:20.04 AS fstarnoocaml
@@ -70,18 +73,20 @@ RUN tar xzf fstar.tar.gz
 ENV FSTAR_HOME /home/test/fstar
 ENV PATH="${FSTAR_HOME}/bin:${PATH}"
 
+# Copy tests, examples and docs
+ADD --chown=test:test examples/ fstar_examples/
+ADD --chown=test:test doc/ fstar_doc/
+
 # Case 3: test F* package without OCaml
 FROM fstarnoocaml
-RUN make -C $FSTAR_HOME/tests/micro-benchmarks -j $opamthreads
-RUN make -C $FSTAR_HOME/examples -j $opamthreads
-RUN make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
+RUN make -C fstar_examples -j $opamthreads
+RUN make -C fstar_doc/tutorial -j $opamthreads regressions
 
 # Case 4: test F* package without OCaml, but recheck ulib
 FROM fstarnoocaml
 RUN make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
-RUN make -C $FSTAR_HOME/tests/micro-benchmarks -j $opamthreads
-RUN make -C $FSTAR_HOME/examples -j $opamthreads
-RUN make -C $FSTAR_HOME/doc/tutorial -j $opamthreads regressions
+RUN make -C fstar_examples -j $opamthreads
+RUN make -C fstar_doc/tutorial -j $opamthreads regressions
 
 # This is the last image. So we can also copy the file that contains
 # the desired filename for the package, to be extracted via

diff --git a/.scripts/process_build.sh b/.scripts/process_build.sh
@@ -63,21 +63,19 @@ cd fstar
 # to export it from here.
 export FSTAR_HOME="$PWD"
 
+# Copy tests and examples to the tmp directory, since they are no
+# longer included in the package. We copy them elsewhere since we
+# don't want to rely on relative paths in their Makefiles.
+rm -rf /tmp/fstar_examples /tmp/fstar_doc
+cp -r $FSTAR_HOST_HOME/examples /tmp/fstar_examples
+cp -r $FSTAR_HOST_HOME/doc /tmp/fstar_doc
+
 diag "-- Versions --"
 bin/fstar.exe --version
 bin/z3 --version
 
-diag "-- Verify micro benchmarks --"
-make -C tests/micro-benchmarks
-if [ $? -ne 0 ]; then
-  echo -e "* ${RED}FAIL!${NC} for micro benchmarks - make returned $?"
-  exit 1
-else
-  echo -e "* ${GREEN}PASSED!${NC} for micro benchmarks"
-fi
-
 diag "-- Execute examples/hello via OCaml -- should output Hello F*! --"
-make -C examples/hello hello | tee HelloOcamlOutput.log
+make -C /tmp/fstar_examples/hello hello | tee HelloOcamlOutput.log
 if [ $? -ne 0 ]; then
   echo -e "* ${RED}FAIL!${NC} for examples/hello - make failed withexit code $?"
   exit 1
@@ -98,14 +96,17 @@ else
 fi
 
 diag "-- Verify all examples --"
-make -j6 -C examples
+make -j6 -C /tmp/fstar_examples
 if [ $? -ne 0 ]; then
   echo -e "* ${RED}FAIL!${NC} for all examples - make returned $?"
   exit 1
 else
   echo -e "* ${GREEN}PASSED!${NC} for all examples"
 fi
 
+# Cleanup
+rm -rf /tmp/fstar_examples /tmp/fstar_doc
+
 # From this point on, we should no longer need FSTAR_HOME.
 export FSTAR_HOME=
 

diff --git a/src/ocaml-output/Makefile b/src/ocaml-output/Makefile
@@ -45,9 +45,6 @@ PREFIX=$(shell pwd)/fstar
 # The string "Madoko" if madoko is installed, something else otherwise.
 MADOKO = $(shell madoko --version 2>/dev/null | cut -c -6)
 DOS2UNIX=$(shell which dos2unix >/dev/null 2>&1 && echo dos2unix || echo true)
-# Set PACKAGE_DOCS to 1 if you want to include html docs into the binary package.
-# If so, then Madoko MUST be installed on the machine building the package.
-PACKAGE_DOCS?=0
 
 # Detect the GNU utilities
 INSTALL_EXEC := $(shell ginstall --version 2>/dev/null | cut -c -8 | head -n 1)
@@ -277,19 +274,7 @@ package:
 	cp ../../_tags $(PREFIX)/
 	cp ../../.common.mk $(PREFIX)/
 	@# Then the rest of the static files.
-	$(call fexport,examples)
-	$(call fexport,tests)
 	$(call fexport,ucontrib)
-	$(call fexport,doc/tutorial)
-ifeq ($(MADOKO),Madoko)
-	@# Build the tutorial
-	+$(MAKE) -C fstar/doc/tutorial
-else
-	@echo " ********** You don't have Madoko installed. Binary package will not include tutorial in html form."
-ifeq ($(PACKAGE_DOCS),1)
-	false
-endif
-endif
 	@# Documentation and licenses
 	cp ../../README.md ../../INSTALL.md ../../LICENSE ../../LICENSE-fsharp.txt $(PREFIX)
 	cp $(Z3_LICENSE) $(PREFIX)/LICENSE-z3.txt