Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 77 insertions, 61 deletions

diff --git a/Makefile.ide b/Makefile.ide
index 48a269ab..ac4ba75d 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -1,10 +1,12 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################
 
 ## Makefile rules for building the CoqIDE interface
 
@@ -41,12 +43,12 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
-IDEDEPS:=lib/clib.cma lib/cErrors.cmo lib/spawn.cmo
+IDEDEPS:=clib/clib.cma lib/lib.cma
 IDECMA:=ide/ide.cma
 IDETOPLOOPCMA=ide/coqidetop.cma
 
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml
 
 IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
 
@@ -55,29 +57,41 @@ IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_
 GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
 GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
 GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
-
+PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin
+SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
 
 ###########################################################################
 # CoqIde special targets
 ###########################################################################
 
-.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
-.PHONY: ide-toploop
+.PHONY: coqide coqide-opt coqide-byte coqide-files coqide-binaries
+.PHONY: ide-toploop ide-byteloop ide-optloop
 
-# target to build CoqIde
-coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
+# target to build CoqIde (native version) and the stuff needed to lauch it
+coqide: coqide-files coqide-opt theories/Init/Prelude.vo
 
-coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
-coqide-no:
-coqide-byte: $(COQIDEBYTE) $(COQIDE)
-coqide-opt:  $(COQIDEBYTE) $(COQIDE)
-coqide-files: $(IDEFILES)
-ifeq ($(BEST),opt)
-ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+# target to build CoqIde (in native and byte versions), and no more
+# NB: this target is used in the opam package coq-coqide
+coqide-binaries: coqide-opt coqide-byte
+
+ifeq ($(HASCOQIDE),opt)
+coqide-opt: $(COQIDE) ide-toploop
 else
-ide-toploop: $(IDETOPLOOPCMA)
+coqide-opt: ide-toploop
 endif
 
+ifeq ($(HASCOQIDE),no)
+coqide-byte: ide-byteloop
+else
+coqide-byte: $(COQIDEBYTE) ide-byteloop
+endif
+
+coqide-files: $(IDEFILES)
+
+ide-byteloop: $(IDETOPLOOPCMA)
+ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs)
+ide-toploop: ide-$(BEST)loop
+
 ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
@@ -94,9 +108,9 @@ $(COQIDEBYTE): $(LINKIDE)
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
 	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
-ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
+ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here
+	$(SHOW)'CAMLP5O   $<'
+	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@
 
 
 ide/%.cmi: ide/%.mli
@@ -109,35 +123,59 @@ ide/%.cmo: ide/%.ml
 
 ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
+# We need to compile this file without -safe-string due mess with
+# lablgtk API. Other option is to require lablgtk >= 2.8.16
+ide/ideutils.cmo: ide/ideutils.ml
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/ideutils.cmx: ide/ideutils.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $<
 
 ####################
 ## Install targets
 ####################
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte install-ide-toploop-byte install-coqide-byte
 
 ifeq ($(HASCOQIDE),no)
 install-coqide: install-ide-toploop
 else
 install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 endif
+ifeq ($(HASCOQIDE),no)
+install-coqide-byte: install-ide-toploop-byte
+else
+install-coqide-byte: install-ide-toploop-byte install-ide-byte
+endif
+
+# Apparently, coqide.byte is not meant to be installed
+
+install-ide-byte:
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA)
 
 install-ide-bin:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
 
 install-ide-toploop:
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
 ifeq ($(BEST),opt)
+	$(MKDIR) $(FULLCOQLIB)/toploop/
 	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
 endif
+install-ide-toploop-byte:
+ifneq ($(BEST),opt)
+	$(MKDIR) $(FULLCOQLIB)/toploop/
+	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+endif
 
 install-ide-devfiles:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
+	$(INSTALLSH) $(FULLCOQLIB) \
 	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
 ifeq ($(BEST),opt)
 	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
@@ -176,15 +214,14 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
 	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
 	$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
-	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
-	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
+	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
+	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
 	cp -R "$(GTKSHARE)/"locale $@
-	cp -R "$(GTKSHARE)/"icons $@
 	cp -R "$(GTKSHARE)/"themes $@
 
 $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
 	$(MKDIR) $@
-	$(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
+	$(INSTALLLIB) $$("$(PIXBUFBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
 
 $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
 	$(MKDIR) $@
@@ -195,7 +232,7 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
 	$(MKDIR) $@/xdg/coq
 	$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
 	$(MKDIR) $@/gtk-2.0
-	{ "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
+	{ "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
 	 sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
 	> $@/gtk-2.0/gdk-pixbuf.loaders
 	{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
@@ -207,32 +244,11 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
 
 $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
 	$(MKDIR) $@
-	$(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
-	$(MKDIR) $@/pango/1.8.0/modules
-	$(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
-	{ "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
-	 sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
-	> $@/pango/1.8.0/modules.cache
-
-	for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-	    do cp $$i $@/; \
-	    ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
-	done
-	for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
-	    do \
-		for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-		do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
-		ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
-	    done
-	EXTRAWORK=1; \
-	while [ $${EXTRAWORK} -eq 1 ]; \
-	do EXTRAWORK=0; \
-	    for i in $@/*.dylib; \
-	    do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
-		do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
-	    done; \
+	macpack -d ../Resources/lib $(COQIDEINAPP)
+	for i in $@/../loaders/*.so $@/../immodules/*.so; \
+	do \
+	  macpack -d ../lib $$i; \
 	done
-	ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
 
 $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
 	$(INSTALLLIB) ide/MacOS/*.icns $@