CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3.

6 files changed, 26 insertions, 36 deletions

diff --git a/INSTALL b/INSTALL
index 44ea195f59..e02439c54b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -43,8 +43,8 @@ WHAT DO YOU NEED ?
 
    - a C compiler
 
-   - for CoqIDE, the lablgtk development files (version >= 2.18.5),
-     and the GTK 2.x libraries including gtksourceview2.
+   - for CoqIDE, the lablgtk development files (version >= 3.0.0),
+     and the GTK 3.x libraries including gtksourceview3.
 
    Note that num and lablgtk should be properly registered with
    findlib/ocamlfind as Coq's makefile will use it to locate the
diff --git a/Makefile.ide b/Makefile.ide
index db1cc3746d..86bdaf62d4 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -17,7 +17,7 @@
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
-#COQIDEINCLUDES : something like -I +lablgtk2
+#COQIDEINCLUDES : something like -I +lablgtk3
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
 #IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
@@ -98,7 +98,7 @@ ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
@@ -108,7 +108,7 @@ endif
 $(COQIDEBYTE): $(LINKIDE)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
 ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
 	@rm -f $@
@@ -128,7 +128,7 @@ ide/%.cmx: ide/%.ml
 	$(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
+# lablgtk API. Other option is to require lablgtk >= 3.0.0
 ide/ideutils.cmo: ide/ideutils.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
@@ -228,7 +228,7 @@ $(COQIDEAPP)/Contents:
 $(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) $^
+	        -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
diff --git a/configure.ml b/configure.ml
index 266abdf3b9..14698c4e61 100644
--- a/configure.ml
+++ b/configure.ml
@@ -700,7 +700,7 @@ let check_for_numlib () =
 let numlib =
   check_for_numlib ()
 
-(** * lablgtk2 and CoqIDE *)
+(** * lablgtk3 and CoqIDE *)
 
 type source = Manual | OCamlFind | Stdlib
 
@@ -716,7 +716,7 @@ let check_lablgtkdir ?(fatal=false) src dir =
   let msg = get_source src in
   if not (dir_exists dir) then
     yell (sprintf "No such directory '%s' (%s)." dir msg)
-  else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then
+  else if not (Sys.file_exists (dir/"gSourceView2.cmi") || Sys.file_exists (dir/"gSourceView3.cmi")) then
     yell (sprintf "Incomplete LablGtk2 (%s): no %s/gSourceView2.cmi." msg dir)
   else if not (Sys.file_exists (dir/"glib.mli")) then
     yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.mli." msg dir)
@@ -732,15 +732,15 @@ let get_lablgtkdir () =
     else "", msg
   | None ->
     let msg = OCamlFind in
-    let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in
+    let d1,_ = tryrun camlexec.find ["query";"lablgtk3.sourceview3"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
-      (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
-      let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in
+      (* In debian wheezy, ocamlfind knows only of lablgtk3 *)
+      let d2,_ = tryrun camlexec.find ["query";"lablgtk3"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
         let msg = Stdlib in
-        let d3 = camllib^"/lablgtk2" in
+        let d3 = camllib^"/lablgtk3" in
         if check_lablgtkdir msg d3 then d3, msg
         else "", msg
 
@@ -748,24 +748,14 @@ let get_lablgtkdir () =
 
 let check_lablgtk_version src dir = match src with
 | Manual | Stdlib ->
-  warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+  warn "Could not check the version of lablgtk3.\nMake sure your version is at least 3.0.0.";
   (true, "an unknown version")
 | OCamlFind ->
-  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
+  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
   try
     let vi = List.map s2i (numeric_prefix_list v) in
-    if vi < [2; 16; 0] then
+    if vi < [3; 0; 0] then
       (false, v)
-    else if vi < [2; 18; 3] then
-      begin
-        (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
-        warn "Your installed lablgtk reports as %s.\n\
-It is possible that the installed version is actually more recent\n\
-but reports an incorrect version. If the installed version is\n\
-actually more recent than 2.18.3, that's fine; if it is not,\n
-CoqIDE will compile but may be very unstable." v;
-        (true, "an unknown version")
-      end
     else
       (true, v)
   with _ -> (false, v)
@@ -791,10 +781,10 @@ let lablgtkdir = ref ""
 let check_coqide () =
   if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
   let dir, via = get_lablgtkdir () in
-  if dir = "" then set_ide No "LablGtk2 not found";
+  if dir = "" then set_ide No "LablGtk3 not found";
   let (ok, version) = check_lablgtk_version via dir in
-  let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in
-  if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")");
+  let found = sprintf "LablGtk3 found (%s, %s)" (get_source via) version in
+  if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
   (* We're now sure to produce at least one kind of coqide *)
   lablgtkdir := shorten_camllib dir;
   if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
@@ -1014,7 +1004,7 @@ let print_summary () =
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
-    pr "  Lablgtk2 library in         : %s\n" (esc !lablgtkdir);
+    pr "  Lablgtk3 library in         : %s\n" (esc !lablgtkdir);
   if !idearchdef = "QUARTZ" then
     pr "  Mac OS integration is on\n";
   pr "  CoqIde                      : %s\n" coqide;
diff --git a/coqide.opam b/coqide.opam
index 314943a881..9e22091898 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -19,8 +19,8 @@ license: "LGPL-2.1"
 depends: [
   "dune"               { build & >= "1.4.0" }
   "coqide-server"
-  "conf-gtksourceview"
-  "lablgtk"            {         >= "2.18.5" }
+  "conf-gtksourceview3"
+  "lablgtk3"
 ]
 
 build-env: [
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index ac763547b6..c95bcf5573 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -10,7 +10,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
         # Dependencies of lablgtk (for CoqIDE)
-        libgtk2.0-dev libgtksourceview2.0-dev \
+        libgtk3.0-dev libgtksourceview3.0-dev \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
     CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
+ENV COQIDE_OPAM="lablgtk3 conf-gtksourceview3"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
@@ -53,7 +53,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
+    COQIDE_OPAM_EDGE="lablgtk3 conf-gtksourceview3" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/ide/dune b/ide/dune
index 3618e4f05d..5082d84c4f 100644
--- a/ide/dune
+++ b/ide/dune
@@ -29,7 +29,7 @@
  (wrapped false)
  (modules (:standard \ document fake_ide idetop coqide_main))
  (optional)
- (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
+ (libraries coqide-server.protocol coqide-server.core lablgtk3.sourceview3))
 
 (rule
  (targets coqide_os_specific.ml)