Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to coqtop.opt$(EXE).

6 files changed, 23 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index ec2ef02d8..df5caf0b7 100644
--- a/Makefile
+++ b/Makefile
@@ -217,7 +217,7 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBIN)
+	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
diff --git a/Makefile.build b/Makefile.build
index c8ab85765..5fd3bd873 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -212,9 +212,17 @@ DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
 LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist")
 CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -)
+CODESIGN_HIDE=$(CODESIGN)
 else
 LINKMETADATA=
 CODESIGN=true
+CODESIGN_HIDE=$(HIDE)true
+endif
+
+ifeq ($(STRIP),true)
+STRIP_HIDE=$(HIDE)true
+else
+STRIP_HIDE=$(STRIP)
 endif
 
 # Best OCaml compiler, used in a generic way
@@ -400,12 +408,12 @@ grammar/%.cmi: grammar/%.mli
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
 coqbyte: $(TOPBYTE) $(CHICKENBYTE)
 
 # Special rule for coqtop, we imitate `ocamlopt` can delete the target
 # to avoid #7666
-$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
+$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
 	rm -f $@ && cp $< $@
 
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
@@ -413,8 +421,8 @@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 
 bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
diff --git a/Makefile.checker b/Makefile.checker
index 0ec565d61..6c19a1a42 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -52,8 +52,8 @@ ifeq ($(BEST),opt)
 $(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 else
 $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
diff --git a/Makefile.common b/Makefile.common
index 94b965a7f..bb6302a98 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -14,8 +14,8 @@
 # Executables
 ###########################################################################
 
-TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
-TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE))
+TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
+TOPBYTE:=$(TOPBINOPT:.opt$(EXE)=.byte$(EXE))
 
 COQTOPEXE:=bin/coqtop$(EXE)
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
diff --git a/Makefile.ide b/Makefile.ide
index 6bb0f62f3..cb5596020 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -99,7 +99,7 @@ $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
+	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
 	cp $< $@
@@ -149,8 +149,8 @@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 
 $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
@@ -229,7 +229,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	        -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
+	$(STRIP_HIDE) $@
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
@@ -275,7 +275,7 @@ $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)
 	$(INSTALLLIB) ide/MacOS/*.icns $@
 
 $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
-	$(CODESIGN) $@
+	$(CODESIGN_HIDE) $@
 
 ###########################################################################
 # CoqIde for Windows special targets
diff --git a/Makefile.install b/Makefile.install
index 010e35d42..21015d336 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -70,7 +70,7 @@ endif
 
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
 
 install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)