From aef4c7bd50e436b2c8f4f96fcc8db4cbc6f4c96f Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Mon, 28 Feb 2022 16:52:45 -0800 Subject: [PATCH] remove tests/, examples/, doc/ from binary package Suggested by @nikswamy --- .docker/package.Dockerfile | 29 +++++++++++++++++------------ .scripts/process_build.sh | 23 ++++++++++++----------- src/ocaml-output/Makefile | 15 --------------- 3 files changed, 29 insertions(+), 38 deletions(-) diff --git a/.docker/package.Dockerfile b/.docker/package.Dockerfile index 7c4a5684b8d..35c111674eb 100644 --- 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 index 1ee9cd777a5..1c58ccb2f0e 100755 --- 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,7 +96,7 @@ 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 @@ -106,6 +104,9 @@ 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 index eec378c0f90..edaf259971f 100644 --- 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