[ci] [coq] Complete 4.06.0 support.

Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.

We also refactor travis to test more lablgtk versions.

We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.

Fixes #6140.

7 files changed, 131 insertions, 25 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1742660c8..3117b2b9a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,8 +18,8 @@ variables:
   # some useful values
   COMPILER_32BIT: "4.02.3+32bit"
 
-  COMPILER_BLEEDING_EDGE: "4.05.0"
-  CAMLP5_VER_BLEEDING_EDGE: "7.01"
+  COMPILER_BLEEDING_EDGE: "4.06.0"
+  CAMLP5_VER_BLEEDING_EDGE: "7.03"
 
   TIMING_PACKAGES: "time python"
 
diff --git a/.travis.yml b/.travis.yml
index 7d7a08161..3ebfbefd2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -30,17 +30,21 @@ env:
   - NJOBS=2
   # system is == 4.02.3
   - COMPILER="system"
+  - COMPILER_BE="4.06.0"
   - CAMLP5_VER="6.14"
+  - CAMLP5_VER_BE="7.03"
   - FINDLIB_VER="1.4.1"
+  - FINDLIB_VER_BE="1.7.3"
+  - LABLGTK="lablgtk.2.16.0 lablgtk-extras.1.5"
+  - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
   - NATIVE_COMP="yes"
   - COQ_DEST="-local"
   # Main test suites
   matrix:
   - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
-  - TEST_TARGET="test-suite" COMPILER="4.06.0+trunk" CAMLP5_VER="7.03" EXTRA_OPAM="num" FINDLIB_VER="1.7.3"
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
-  - TEST_TARGET="validate"   COMPILER="4.06.0+trunk+flambda" CAMLP5_VER="7.03" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="1.7.3"
+  - TEST_TARGET="validate"   COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}"
   - TEST_TARGET="ci-bignums TIMED=1"
   - TEST_TARGET="ci-color TIMED=1"
   - TEST_TARGET="ci-compcert TIMED=1"
@@ -82,7 +86,7 @@ matrix:
     - env:
       - TEST_TARGET="test-suite"
       - EXTRA_CONF="-coqide opt -with-doc yes"
-      - EXTRA_OPAM="lablgtk-extras hevea"
+      - EXTRA_OPAM="hevea ${LABLGTK}"
       addons:
         apt:
           sources:
@@ -106,11 +110,11 @@ matrix:
 
     - env:
       - TEST_TARGET="test-suite"
-      - COMPILER="4.05.0"
-      - FINDLIB_VER="1.7.3"
-      - CAMLP5_VER="7.03"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
       - EXTRA_CONF="-coqide opt -with-doc yes"
-      - EXTRA_OPAM="lablgtk-extras hevea"
+      - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
       addons:
         apt:
           sources:
@@ -120,12 +124,12 @@ matrix:
     # Full test-suite with flambda
     - env:
       - TEST_TARGET="test-suite"
-      - COMPILER="4.05.0+flambda"
-      - FINDLIB_VER="1.7.3"
-      - CAMLP5_VER="7.03"
+      - COMPILER="${COMPILER_BE}+flambda"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
       - NATIVE_COMP="no"
       - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
-      - EXTRA_OPAM="lablgtk-extras hevea"
+      - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
       addons:
         apt:
           sources:
@@ -136,7 +140,7 @@ matrix:
     - env:
       - TEST_TARGET="coqocaml"
       - EXTRA_CONF="-coqide opt -warn-error"
-      - EXTRA_OPAM="lablgtk-extras hevea"
+      - EXTRA_OPAM="hevea ${LABLGTK}"
       # dummy target
       - BUILD_TARGET="clean"
       addons:
@@ -151,11 +155,11 @@ matrix:
 
     - env:
       - TEST_TARGET="coqocaml"
-      - COMPILER="4.05.0"
-      - CAMLP5_VER="7.03"
-      - FINDLIB_VER="1.7.3"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
       - EXTRA_CONF="-coqide opt -warn-error"
-      - EXTRA_OPAM="lablgtk-extras hevea"
+      - EXTRA_OPAM="num hevea ${LABLGTK_BE}"
       # dummy target
       - BUILD_TARGET="clean"
       addons:
@@ -184,7 +188,7 @@ matrix:
       - NATIVE_COMP="no"
       - COQ_DEST="-prefix ${PWD}/_install"
       - EXTRA_CONF="-coqide opt -warn-error"
-      - EXTRA_OPAM="lablgtk-extras"
+      - EXTRA_OPAM="${LABLGTK}"
       before_install:
       - brew update
       - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3
diff --git a/API/API.ml b/API/API.ml
index 9a67e3111..f588fe193 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -20,6 +20,10 @@
 (******************************************************************************)
 module Coq_config = Coq_config
 
+(* Reexporting deprecated symbols throu module aliases triggers a
+   warning in 4.06.0 *)
+[@@@ocaml.warning "-3"]
+
 (******************************************************************************)
 (* Kernel *)
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index d0564f9ec..cb945179f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -20,6 +20,10 @@
    See below in the file for their concrete position.
 *)
 
+(* Reexporting deprecated symbols throu module aliases triggers a
+   warning in 4.06.0 *)
+[@@@ocaml.warning "-3"]
+
 (************************************************************************)
 (* Modules from config/                                                 *)
 (************************************************************************)
@@ -300,21 +304,31 @@ sig
   [@@ocaml.deprecated "alias of API.Names.Constant.make3"]
 
   val debug_pr_con : Constant.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_pr_mind : MutInd.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val pr_con : Constant.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val string_of_con : Constant.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val string_of_mind : MutInd.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_string_of_mind : MutInd.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_string_of_con : Constant.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   type identifier = Id.t
+  [@@ocaml.deprecated "Alias of Names"]
+
   module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
+  [@@ocaml.deprecated "Alias of Id.Set.t"]
 
 end
 
@@ -329,6 +343,7 @@ sig
   end
 
   type universe_level = Level.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module LSet :
   sig
@@ -343,6 +358,7 @@ sig
   end
 
   type universe = Universe.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module Instance :
   sig
@@ -374,6 +390,7 @@ sig
   end
 
   type universe_context = UContext.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module AUContext :
   sig
@@ -382,6 +399,7 @@ sig
   end
 
   type abstract_universe_context = AUContext.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module CumulativityInfo :
   sig
@@ -389,12 +407,14 @@ sig
   end
 
   type cumulativity_info = CumulativityInfo.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module ACumulativityInfo :
   sig
     type t
   end
   type abstract_cumulativity_info = ACumulativityInfo.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module ContextSet :
   sig
@@ -408,8 +428,10 @@ sig
   type 'a in_universe_context = 'a * UContext.t
 
   type universe_context_set = ContextSet.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   type universe_set = LSet.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t
 
@@ -586,6 +608,10 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
   val mkApp : t * t array -> t
   val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
 
+  type rec_declaration = Name.t array * types array * constr array
+  type fixpoint = (int array * int) * rec_declaration
+  val mkFix : fixpoint -> constr
+
   val mkConst : Constant.t -> t
   val mkConstU : pconstant -> t
 
@@ -831,8 +857,10 @@ module Term :
 sig
 
   type sorts_family = Sorts.family = InProp | InSet | InType
+  [@@ocaml.deprecated "Alias of Sorts.family"]
 
   type contents = Sorts.contents = Pos | Null
+  [@@ocaml.deprecated "Alias of Sorts.contents"]
 
   type sorts = Sorts.t =
     | Prop of contents
@@ -840,35 +868,48 @@ sig
   [@@ocaml.deprecated "alias of API.Sorts.t"]
 
   type constr = Constr.t
+  [@@ocaml.deprecated "Alias of Constr.t"]
   type types = Constr.t
+  [@@ocaml.deprecated "Alias of Constr.types"]
 
   type metavariable = int
+  [@@ocaml.deprecated "Alias of Constr.metavariable"]
 
   type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array
+  [@@ocaml.deprecated "Alias of Constr.prec_declaration"]
 
   type 'constr pexistential = 'constr Constr.pexistential
+  [@@ocaml.deprecated "Alias of Constr.pexistential"]
+
   type cast_kind = Constr.cast_kind =
                  | VMcast
                  | NATIVEcast
                  | DEFAULTcast
                  | REVERTcast
+  [@@ocaml.deprecated "Alias of Constr.cast_kind"]
 
   type 'a puniverses = 'a Univ.puniverses
+  [@@ocaml.deprecated "Alias of Constr.puniverses"]
   type pconstant = Names.Constant.t puniverses
+  [@@ocaml.deprecated "Alias of Constr.pconstant"]
   type pinductive = Names.inductive puniverses
+  [@@ocaml.deprecated "Alias of Constr.pinductive"]
   type pconstructor = Names.constructor puniverses
+  [@@ocaml.deprecated "Alias of Constr.pconstructor"]
   type case_style = Constr.case_style =
     | LetStyle
     | IfStyle
     | LetPatternStyle
     | MatchStyle
     | RegularStyle
+  [@@ocaml.deprecated "Alias of Constr.case_style"]
 
   type case_printing = Constr.case_printing =
     { ind_tags  : bool list;
       cstr_tags : bool list array;
       style     : case_style
     }
+  [@@ocaml.deprecated "Alias of Constr.case_printing"]
 
   type case_info = Constr.case_info =
     { ci_ind        : Names.inductive;
@@ -877,12 +918,15 @@ sig
       ci_cstr_nargs : int array;
       ci_pp_info    : case_printing
     }
+  [@@ocaml.deprecated "Alias of Constr.case_info"]
 
   type ('constr, 'types) pfixpoint =
     (int array * int) * ('constr, 'types) prec_declaration
+  [@@ocaml.deprecated "Alias of Constr.pfixpoint"]
 
   type ('constr, 'types) pcofixpoint =
     int * ('constr, 'types) prec_declaration
+  [@@ocaml.deprecated "Alias of Constr.pcofixpoint"]
 
   type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
      | Rel       of int
@@ -902,11 +946,17 @@ sig
      | Fix       of ('constr, 'types) pfixpoint
      | CoFix     of ('constr, 'types) pcofixpoint
      | Proj      of Names.Projection.t * 'constr
+  [@@ocaml.deprecated "Alias of Constr.kind_of_term"]
   type existential = Constr.existential_key * constr array
+  [@@ocaml.deprecated "Alias of Constr.existential"]
   type rec_declaration = Names.Name.t array * constr array * constr array
+  [@@ocaml.deprecated "Alias of Constr.rec_declaration"]
   type fixpoint = (int array * int) * rec_declaration
+  [@@ocaml.deprecated "Alias of Constr.fixpoint"]
   type cofixpoint = int * rec_declaration
+  [@@ocaml.deprecated "Alias of Constr.cofixpoint"]
   val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
+  [@@ocaml.deprecated "Alias of Constr.kind"]
   val applistc : constr -> constr list -> constr
 
   val applist : constr * constr list -> constr
@@ -914,29 +964,52 @@ sig
 
   val mkArrow : types -> types -> constr
   val mkRel : int -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkVar : Names.Id.t -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
 
   val mkMeta : Constr.metavariable -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
 
   val mkEvar : existential -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkSort : Sorts.t -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProp : types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkSet  : types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkType : Univ.Universe.t -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCast : constr * cast_kind * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProd : Names.Name.t * types * types -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkLambda : Names.Name.t * types * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkLetIn : Names.Name.t * constr * types * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkApp : constr * constr array -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConst : Names.Constant.t -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProj : Names.Projection.t * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkInd : Names.inductive -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstruct : Names.constructor -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstructU : Names.constructor puniverses -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstructUi : (pinductive * int) -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCase : case_info * constr * constr * constr array -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkFix : fixpoint -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCoFix : cofixpoint -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
+
   val mkNamedLambda : Names.Id.t -> types -> constr -> constr
   val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
   val mkNamedProd : Names.Id.t -> types -> types -> types
@@ -975,26 +1048,37 @@ sig
   val isApp : constr -> bool
 
   val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
+  [@@ocaml.deprecated "Alias of Constr.fold"]
 
   val eq_constr : constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.equal"]
 
   val hash_constr : constr -> int
+  [@@ocaml.deprecated "Alias of Constr.hash"]
+
   val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
   val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
   val prod_applist : constr -> constr list -> constr
   exception DestKO
   val map_constr : (constr -> constr) -> constr -> constr
+  [@@ocaml.deprecated "Alias of Constr.map"]
 
   val mkIndU : pinductive -> constr
+  [@@ocaml.deprecated "Alias of Constr.mkIndU"]
   val mkConstU : pconstant -> constr
+  [@@ocaml.deprecated "Alias of Constr.mkConstU"]
   val map_constr_with_binders :
     ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+  [@@ocaml.deprecated "Alias of Constr.map_with_binders"]
+
   val iter_constr : (constr -> unit) -> constr -> unit
+  [@@ocaml.deprecated "Alias of Constr.iter."]
 
   (* Quotients away universes: really needed?
    * Can't we just call eq_c_univs_infer and discard the inferred csts?
    *)
   val eq_constr_nounivs : constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.qe_constr_nounivs."]
 
   type ('constr, 'types) kind_of_type =
     | SortType   of Sorts.t
@@ -1009,13 +1093,16 @@ sig
   [@@ocaml.deprecated "alias of API.Sorts.is_prop"]
 
   type existential_key = Constr.existential_key
+  [@@ocaml.deprecated "Alias of Constr.existential_key"]
 
   val family_of_sort : Sorts.t -> Sorts.family
+  [@@ocaml.deprecated "Alias of Sorts.family"]
 
   val compare : constr -> constr -> int
+  [@@ocaml.deprecated "Alias of Constr.compare."]
 
   val constr_ord : constr -> constr -> int
-  [@@ocaml.deprecated "alias of API.Term.compare"]
+  [@@ocaml.deprecated "alias of Term.compare"]
 
   val destInd : constr -> Names.inductive puniverses
   val univ_of_sort : Sorts.t -> Univ.Universe.t
@@ -1027,6 +1114,8 @@ sig
   val destFix : constr -> fixpoint
 
   val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.compare_head."]
+
 end
 
 module Mod_subst :
@@ -1673,6 +1762,7 @@ sig
     | LetPatternStyle
     | MatchStyle
     | RegularStyle (** infer printing form from number of constructor *)
+  [@@ocaml.deprecated "Alias for Constr.case_style."]
 
   type 'a cast_type =
                     | CastConv of 'a
diff --git a/Makefile.ide b/Makefile.ide
index 7593a9f2e..7d809f67a 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -123,6 +123,15 @@ ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(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
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 83e5da950..0977a1890 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -372,8 +372,7 @@ let read_file name buf =
 let io_read_all chan =
   Buffer.clear read_buffer;
   let read_once () =
-    (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
-    let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
+    let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
     Buffer.add_subbytes read_buffer read_string 0 len
   in
   begin
diff --git a/kernel/term.mli b/kernel/term.mli
index cb782afac..33c6b0b08 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -369,11 +369,11 @@ val mkConstructU : constructor puniverses -> constr
 val mkConstructUi : (pinductive * int) -> constr
 [@@ocaml.deprecated "Alias for Constr"]
 val mkCase : case_info * constr * constr * constr array -> constr
-[@@ocaml.deprecated "Alias for Constr"]
+[@@ocaml.deprecated "Alias for Constr.mkCase"]
 val mkFix : fixpoint -> constr
-[@@ocaml.deprecated "Alias for Constr"]
+[@@ocaml.deprecated "Alias for Constr.mkFix"]
 val mkCoFix : cofixpoint -> constr
-[@@ocaml.deprecated "Alias for Constr"]
+[@@ocaml.deprecated "Alias for Constr.mkCoFix"]
 
 (** {6 Aliases} *)