Merge PR coq#9279: CoqIDE on lablgtk3

Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: garrigue
Ack-by: herbelin

.gitlab-ci.yml

@@ -10,7 +10,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2019-03-11-V1"
+  CACHEKEY: "bionic_coq-V2019-03-12-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"

CHANGES.md

@@ -17,6 +17,8 @@ OCaml and dependencies
 
 Coqide
 
+- CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2.
+
 - CoqIDE now properly sets the module name for a given file based on
   its path, see -topfile change entry for more details.
 

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

Makefile.ide

@@ -17,7 +17,6 @@
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
-#COQIDEINCLUDES : something like -I +lablgtk2
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
 #IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
@@ -41,7 +40,11 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 
 IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
 
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+ifeq ($(HASCOQIDE),no)
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS))
+else
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3-sourceview3
+endif
 
 IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
 IDECMA:=ide/ide.cma
@@ -56,11 +59,11 @@ IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_
 
 ## GTK for Coqide MacOS bundle
 
-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
+GTKSHARE=$(shell pkg-config --variable=prefix gtk+-3.0)/share
+GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin
+GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0)
+PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-3.0)/bin
+SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share
 
 ###########################################################################
 # CoqIde special targets
@@ -98,7 +101,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 -linkall $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
@@ -108,7 +111,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 +131,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 +231,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

configure.ml

@@ -150,7 +150,11 @@ let numeric_prefix_list s =
   let max = String.length s in
   let i = ref 0 in
   while !i < max && isnum s.[!i] do incr i done;
-  string_split '.' (String.sub s 0 !i)
+  match string_split '.' (String.sub s 0 !i) with
+  | [v] -> [v;"0";"0"]
+  | [v1;v2] -> [v1;v2;"0"]
+  | [v1;v2;""] -> [v1;v2;"0"] (* e.g. because it ends with ".beta" *)
+  | v -> v
 
 (** Combined existence and directory tests *)
 
@@ -226,7 +230,6 @@ type preferences = {
   docdir : string option;
   coqdocdir : string option;
   ocamlfindcmd : string option;
-  lablgtkdir : string option;
   arch : string option;
   natdynlink : bool;
   coqide : ide option;
@@ -263,7 +266,6 @@ let default = {
   docdir = None;
   coqdocdir = None;
   ocamlfindcmd = None;
-  lablgtkdir = None;
   arch = None;
   natdynlink = true;
   coqide = None;
@@ -368,8 +370,6 @@ let args_options = Arg.align [
     "<dir> Where to install Coqdoc style files";
   "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }),
     "<dir> Specifies the ocamlfind command to use";
-  "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }),
-    "<dir> Specifies the path to the Lablgtk library";
   "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }),
     "<flags> Specifies additional flags to be passed to the flambda optimizing compiler";
   "-arch", arg_string_option (fun p arch -> { p with arch }),
@@ -697,75 +697,31 @@ let check_for_numlib () =
 let numlib =
   check_for_numlib ()
 
-(** * lablgtk2 and CoqIDE *)
+(** * lablgtk3 and CoqIDE *)
 
-type source = Manual | OCamlFind | Stdlib
-
-let get_source = function
-| Manual -> "manually provided"
-| OCamlFind -> "via ocamlfind"
-| Stdlib -> "in OCaml library"
-
-(** Is some location a suitable LablGtk2 installation ? *)
-
-let check_lablgtkdir ?(fatal=false) src dir =
-  let yell msg = if fatal then die msg else (warn "%s" msg; false) in
-  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
-    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)
-  else true
-
-(** Detect and/or verify the Lablgtk2 location *)
+(** Detect and/or verify the Lablgtk3 location *)
 
 let get_lablgtkdir () =
-  match !prefs.lablgtkdir with
-  | Some dir ->
-    let msg = Manual in
-    if check_lablgtkdir ~fatal:true msg dir then dir, msg
-    else "", msg
-  | None ->
-    let msg = OCamlFind in
-    let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] 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
-      if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
-      else
-        let msg = Stdlib in
-        let d3 = camllib^"/lablgtk2" in
-        if check_lablgtkdir msg d3 then d3, msg
-        else "", msg
+  tryrun camlexec.find ["query";"lablgtk3-sourceview3"]
 
 (** Detect and/or verify the Lablgtk2 version *)
 
-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.";
-  (true, "an unknown version")
-| OCamlFind ->
-  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
-  try
-    let vi = List.map s2i (numeric_prefix_list v) in
-    if vi < [2; 16; 0] then
+let check_lablgtk_version () =
+  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
+  (true, v)
+
+(* ejgallego: we wait to do version checks until an official release is out *)
+(*  try
+    let vi = numeric_prefix_list v in
+    (* Temporary hack *)
+    if vi = ["3";"0";"beta3"] then (false, v) else
+    let vi = List.map s2i vi in
+    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)
+*)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -788,39 +744,36 @@ 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";
-  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 ^ ")");
-  (* 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");
-  if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler");
-  if not (Sys.file_exists (dir/"gtkThread.cmx")) then
-    set_ide Byte (found^", but no native LablGtk2");
-  if not (Sys.file_exists (camllib/"threads"/"threads.cmxa")) then
-    set_ide Byte (found^", but no native threads");
-  set_ide Opt (found^", with native threads")
+  if dir = ""
+  then set_ide No "LablGtk3 not found"
+  else
+    let (ok, version) = check_lablgtk_version () in
+    let found = sprintf "LablGtk3 found (%s)" 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");
+    if best_compiler <> "opt" then set_ide Byte (found^", but no native compiler");
+    if not (Sys.file_exists (camllib/"threads"/"threads.cmxa")) then
+      set_ide Byte (found^", but no native threads");
+    set_ide Opt (found^", with native threads")
 
 let coqide =
   try check_coqide ()
   with Ide Opt -> "opt" | Ide Byte -> "byte" | Ide No -> "no"
 
 (** System-specific CoqIde flags *)
 
-let lablgtkincludes = ref ""
 let idearchflags = ref ""
 let idearchfile = ref ""
 let idecdepsflags = ref ""
 let idearchdef = ref "X11"
 
 let coqide_flags () =
-  if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir;
   match coqide, arch with
     | "opt", "Darwin" when !prefs.macintegration ->
       let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in
       if osxdir <> "" then begin
-        lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
         idearchflags := "lablgtkosx.cma";
         idearchdef := "QUARTZ"
       end
@@ -1011,7 +964,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;
@@ -1203,7 +1156,6 @@ let write_makefile f =
   pr "# Unix systems and no profiling: strip\n";
   pr "STRIP=%s\n\n" strip;
   pr "# LablGTK\n";
-  pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
   pr "# CoqIde (no/byte/opt)\n";
   pr "HASCOQIDE=%s\n" coqide;
   pr "IDEFLAGS=%s\n" !idearchflags;

coqide.opam

@@ -17,10 +17,10 @@ dev-repo: "git+https://github.com/coq/coq.git"
 license: "LGPL-2.1"
 
 depends: [
-  "dune"               { build & >= "1.4.0" }
+  "dune"                 { build & >= "1.4.0" }
   "coqide-server"
-  "conf-gtksourceview"
-  "lablgtk"            {         >= "2.18.5" }
+  "lablgtk3"             {         >= "3.0.beta5" }
+  "lablgtk3-sourceview3" {         >= "3.0.beta5" }
 ]
 
 build-env: [

default.nix

@@ -45,7 +45,10 @@ stdenv.mkDerivation rec {
     dune
   ]
   ++ (with ocamlPackages; [ ocaml findlib num ])
-  ++ optional buildIde ocamlPackages.lablgtk
+  ++ optionals buildIde [
+    ocamlPackages.lablgtk3-sourceview3
+    glib gnome3.defaultIconTheme wrapGAppsHook
+  ]
   ++ optionals buildDoc [
     # Sphinx doc dependencies
     pkgconfig (python3.withPackages

dev/build/windows/MakeCoq_MinGW.bat

@@ -331,7 +331,7 @@ IF "%CYGWIN_QUIET%" == "Y" (
 )
 
 IF "%GTK_FROM_SOURCES%"=="N" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
 )
 
 REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.