Merge pull request #3535 from mtzguido/clean

Makefile: fix clean rule

.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

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.

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