From 29f634ac3c2205104a69e8560a0099ac85c1d954 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 6 Oct 2024 12:42:09 -0700 Subject: [PATCH] Makefile: fix clean rule The clean-buildfiles subrule could only work after a build, and failed on a fresh repo. Given we only needed it to decrease the size of docker images after a build (which we soon won't do) and didn't have automatic pruning (we do now), this is not that useful. Just remove it and clean as before. --- .docker/build/build_funs.sh | 4 ---- Makefile | 14 +------------- src/Makefile | 8 ++++---- 3 files changed, 5 insertions(+), 21 deletions(-) diff --git a/.docker/build/build_funs.sh b/.docker/build/build_funs.sh index 432f86e9d62..fdea427cb30 100644 --- a/.docker/build/build_funs.sh +++ b/.docker/build/build_funs.sh @@ -78,10 +78,6 @@ function fstar_default_build () { return 1 fi - # Clean temporary build files, not needed and saves - # several hundred MB - make clean-buildfiles || true - export_home FSTAR "$(pwd)" wait # for fetches above diff --git a/Makefile b/Makefile index 8e8e7f21f07..9e2af429faf 100644 --- a/Makefile +++ b/Makefile @@ -98,21 +98,9 @@ package: all # Removes everything created by `make all`. MUST NOT be used when # bootstrapping. .PHONY: clean -clean: clean-intermediate clean-buildfiles +clean: clean-intermediate $(call msg, "CLEAN") - $(Q)cd $(DUNE_SNAPSHOT) && { dune uninstall --prefix=$(FSTAR_CURDIR) || true ; } - -# Clean temporary dune build files, while retaining all checked files -# and installed files. Used to save space after building, particularly -# after CI. Note we have to keep fstar.install or otherwise `dune -# uninstall` cannot work. -.PHONY: clean-buildfiles -clean-buildfiles: - $(call msg, "CLEAN BUILDFILES") - $(Q)cp -f $(DUNE_SNAPSHOT)/_build/default/fstar.install ._fstar.install $(Q)cd $(DUNE_SNAPSHOT) && { dune clean || true ; } - $(Q)mkdir -p $(DUNE_SNAPSHOT)/_build/default/ - $(Q)cp -f ._fstar.install $(DUNE_SNAPSHOT)/_build/default/fstar.install # Removes all .checked files and other intermediate files # Does not remove the object files from the dune snapshot. diff --git a/src/Makefile b/src/Makefile index 0e619b3f4f4..6166f754a8d 100644 --- a/src/Makefile +++ b/src/Makefile @@ -18,9 +18,9 @@ clean: clean-ocaml # -------------------------------------------------------------------- clean_boot: - rm -rf .cache.boot - rm -f ._depend - rm -f .depend + $(Q)rm -rf .cache.boot + $(Q)rm -f ._depend + $(Q)rm -f .depend # -------------------------------------------------------------------------------- # Now we have some make targets wrap calls to other makefiles, @@ -31,7 +31,7 @@ ocaml: $(Q)+$(MAKE) -f Makefile.boot all-ml clean-ocaml: clean_boot - +$(MAKE) -C ocaml-output clean + +$(Q)$(MAKE) -C ocaml-output clean # -------------------------------------------------------------------- # Testing