No more coqtop.opt, produce directly a coqtop binary

 We now always produce two binaries, coqtop and coqtop.byte :
 - If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
   no more symlinks needed.
 - Otherwise, coqtop is a copy of coqtop.byte.

 The same for coqchk and coqide...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 36 insertions, 55 deletions

diff --git a/Makefile b/Makefile
index a861a2d0a..ff345556b 100644
--- a/Makefile
+++ b/Makefile
@@ -166,7 +166,7 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) bin/fake_ide
+	rm -f $(COQTOPBYTE) $(CHICKENBYTE) bin/fake_ide
 	find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
@@ -199,12 +199,11 @@ archclean: clean-ide optclean voclean
 
 optclean:
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
-	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
 	rm -f $(TOOLS) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
 clean-ide:
-	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
+	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
 	rm -f ide/input_method_lexer.ml
 	rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
 	rm -f ide/utf8_convert.ml
diff --git a/Makefile.build b/Makefile.build
index c94b3d884..d11dcc765 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -80,7 +80,7 @@ TIMECMD=	# is "'time -p'" to get compilation time of .v
 # TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
 COQOPTS=$(COQ_XML) $(VM)
-BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
+BOOTCOQTOP:=$(TIMECMD) $(COQTOPEXE) -boot $(COQOPTS)
 BOOTCOQC:=$(BOOTCOQTOP) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
@@ -144,12 +144,12 @@ ifndef ORDER_ONLY_SEP
 $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
 endif
 
-VO_TOOLS_DEP := $(BESTCOQTOP)
+VO_TOOLS_DEP := $(COQTOPEXE)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif
 ifdef VALIDATE
- VO_TOOLS_DEP += $(BESTCHICKEN)
+ VO_TOOLS_DEP += $(CHICKEN)
 endif
 ifdef NO_RECOMPILE_LIB
  VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP)
@@ -214,35 +214,39 @@ coqlight: theories-light tools coqbinaries
 
 states:: states/initial.coq
 
-$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
+ifeq ($(BEST),opt)
+$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
 	$(STRIP) $@
+else
+$(COQTOPEXE): $(COQTOPBYTE)
+	cp $< $@
+endif
 
 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
 
-$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
-	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
-
 LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
 CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
 CHKBYTEFLAGS:=$(CHKLIBS) $(CAMLDEBUG) $(USERFLAGS)
 CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 
-$(CHICKENOPT): checker/check.cmxa checker/main.ml
+ifeq ($(BEST),opt)
+$(CHICKEN): checker/check.cmxa checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^
 	$(STRIP) $@
+else
+$(CHICKEN): $(CHICKENBYTE)
+	cp $< $@
+endif
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^
 
-$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
-	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
-
 # coqmktop
 $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -305,23 +309,25 @@ IDEFILES=ide/coq.lang ide/coq_style.xml ide/coq.png ide/mac_default_accel_map
 coqide-binaries: coqide-$(HASCOQIDE)
 coqide-no:
 coqide-byte: $(COQIDEBYTE) $(COQIDE)
-coqide-opt:  $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
+coqide-opt:  $(COQIDEBYTE) $(COQIDE)
 coqide-files: $(IDEFILES)
 
-$(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT)
+ifeq ($(HASCOQIDE),opt)
+$(COQIDE): $(LINKIDEOPT) | $(COQTOPEXE)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa\
 	         lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx str.cmxa $(LINKIDEOPT)
 	$(STRIP) $@
+else
+$(COQIDE): $(COQIDEBYTE)
+	cp $< $@
+endif
 
 $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma\
 	        lablgtksourceview2.cma gtkThread.cmo str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
 
-$(COQIDE):
-	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
-
 # install targets
 
 .PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt
@@ -367,15 +373,15 @@ install-ide-info:
 
 VALIDOPTS=-silent -o -m
 
-validate:: $(BESTCHICKEN) $(ALLVO)
+validate:: $(CHICKEN) $(ALLVO)
 	$(SHOW)'COQCHK <theories & plugins>'
-	$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
+	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
 $(ALLSTDLIB).v:
 	$(SHOW)'MAKE $(notdir $@)'
 	$(HIDE)echo "Require $(ALLMODS)." > $@
 
-MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE)
+MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
 check:: validate test-suite
 
@@ -590,17 +596,9 @@ endif
 install-coq: install-binaries install-library install-coq-info install-devfiles
 install-coqlight: install-binaries install-library-light
 
-install-binaries:: install-$(BEST)  install-tools
-
-install-byte::
-	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
-	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
-
-install-opt::
+install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
-	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
+	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
 
 install-tools::
 	$(MKDIR) $(FULLBINDIR)
@@ -913,7 +911,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)$(BOOTCOQC) $*
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
-	$(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
+	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
diff --git a/Makefile.common b/Makefile.common
index 7925474ba..d38c6475d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -17,13 +17,9 @@ COQMKTOP:=bin/coqmktop$(EXE)
 COQC:=bin/coqc$(EXE)
 
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
-COQTOPOPT:=bin/coqtop.opt$(EXE)
-BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
 
 CHICKENBYTE:=bin/coqchk.byte$(EXE)
-CHICKENOPT:=bin/coqchk.opt$(EXE)
-BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
 
 FAKEIDE:=bin/fake_ide$(EXE)
@@ -50,7 +46,6 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 COQIDEBYTE:=bin/coqide.byte$(EXE)
-COQIDEOPT:=bin/coqide.opt$(EXE)
 COQIDE:=bin/coqide$(EXE)
 
 ifeq ($(BEST),opt)
@@ -63,8 +58,8 @@ BESTOBJ:=$(if $(OPT),.cmx,.cmo)
 BESTLIB:=$(if $(OPT),.cmxa,.cma)
 
 COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \
-  $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN)
+  $(COQTOPBYTE) $(COQTOPEXE) \
+  $(CHICKENBYTE) $(CHICKEN)
 
 CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 5a0c0623c..0a3938ae1 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -22,8 +22,7 @@
 
 let environment = Unix.environment ()
 
-let best = if Coq_config.arch = "win32" then "" else ("."^Coq_config.best)
-let binary = ref ("coqtop" ^ best)
+let binary = ref "coqtop"
 let image = ref ""
 
 (* coqc options *)
@@ -110,8 +109,7 @@ let parse_args () =
 	usage ()
     | "-byte" :: rem ->
        binary := "coqtop.byte"; parse (cfiles,args) rem
-    | "-opt" :: rem ->
-       binary := "coqtop.opt"; parse (cfiles,args) rem
+    | "-opt" :: rem -> (* now a no-op *) parse (cfiles,args) rem
     | "-libdir" :: _ :: rem ->
         print_string "Warning: option -libdir deprecated and ignored\n"; flush stdout;
         parse (cfiles,args) rem
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f3013c04d..acf5600d2 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,13 +30,8 @@
 BIN := ../bin/
 LIB := ..
 
-ifeq ($(BEST),byte)
-  coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
-  bincoqc := $(BIN)coqc -coqlib $(LIB) -byte -I prerequisite
-else
-  coqtop := $(BIN)coqtop -boot -q -batch -I prerequisite
-  bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
-endif
+coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
+bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
 
 command := $(coqtop) -top Top -load-vernac-source
 coqc := $(coqtop) -compile
diff --git a/test-suite/check b/test-suite/check
index 48a674490..3d14f6bc0 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -2,10 +2,6 @@
 
 MAKE="${MAKE:=make}"
 
-if [ "$1" = -byte ]; then
-  export BEST=byte
-fi
-
 ${MAKE} clean > /dev/null 2>&1
 ${MAKE} all > /dev/null 2>&1
 cat summary.log