[coqide] [ci] Update GTK toolchain to lablgtk3

- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile

16 files changed, 172 insertions, 479 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 309044a1e9..58bf6bf065 100644
--- a/.gitlab-ci.yml
+++ b/.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"
diff --git a/Makefile.ide b/Makefile.ide
index 86bdaf62d4..778863d1fc 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -17,7 +17,6 @@
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
-#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
@@ -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,lablgtk3.sourceview3 $(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,lablgtk3.sourceview3 $(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 $@
diff --git a/configure.ml b/configure.ml
index 14698c4e61..5b99851f83 100644
--- a/configure.ml
+++ b/configure.ml
@@ -153,6 +153,7 @@ let numeric_prefix_list s =
   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 *)
@@ -229,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;
@@ -266,7 +266,6 @@ let default = {
   docdir = None;
   coqdocdir = None;
   ocamlfindcmd = None;
-  lablgtkdir = None;
   arch = None;
   natdynlink = true;
   coqide = None;
@@ -371,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 }),
@@ -702,63 +699,29 @@ let numlib =
 
 (** * 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") || 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)
-  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";"lablgtk3.sourceview3"] in
-    if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
-    else
-      (* 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^"/lablgtk3" 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 lablgtk3.\nMake sure your version is at least 3.0.0.";
-  (true, "an unknown version")
-| OCamlFind ->
+let check_lablgtk_version () =
   let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
-  try
-    let vi = List.map s2i (numeric_prefix_list v) 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
       (true, v)
   with _ -> (false, v)
+*)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -781,19 +744,19 @@ 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 "LablGtk3 not found";
-  let (ok, version) = check_lablgtk_version via dir in
-  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");
-  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 ()
@@ -801,19 +764,16 @@ let coqide =
 
 (** 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
@@ -1196,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;
diff --git a/coqide.opam b/coqide.opam
index 9e22091898..c82fa72564 100644
--- a/coqide.opam
+++ b/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-gtksourceview3"
-  "lablgtk3"
+  "lablgtk3"             {         >= "3.0.beta5" }
+  "lablgtk3-sourceview3" {         >= "3.0.beta5" }
 ]
 
 build-env: [
diff --git a/default.nix b/default.nix
index cede0cd6b1..3cc0bfb11f 100644
--- a/default.nix
+++ b/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
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index c8cfcf60c8..c3f3a97ff5 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/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.

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 43f44a80b4..03bda8d0c0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -742,7 +742,7 @@ function make_fontconfig {
 ##### ICONV #####
 
 function make_libiconv {
-  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.14  tar.gz  true
+  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.15  tar.gz  true
 }
 
 ##### UNISTRING #####
@@ -816,7 +816,9 @@ function make_glib {
   make_gettext
   make_libffi
   make_libpcre
+
   build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/glib/2.57  glib-2.57.1  tar.xz  true
+
 }
 
 ##### ATK #####
@@ -824,7 +826,7 @@ function make_glib {
 function make_atk {
   make_gettext
   make_glib
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.29  atk-2.29.1  tar.xz  true
+  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.30  atk-2.30.0  tar.xz  true
 }
 
 ##### PIXBUF #####
@@ -837,7 +839,7 @@ function make_gdk-pixbuf {
   # CONFIGURE PARAMETERS
   # --with-included-loaders=yes statically links the image file format handlers
   # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36  gdk-pixbuf-2.36.12  tar.xz  true  --with-included-loaders=yes
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.38  gdk-pixbuf-2.38.0  tar.xz  true  --with-included-loaders=yes
 }
 
 ##### CAIRO #####
@@ -848,7 +850,7 @@ function make_cairo {
   make_glib
   make_pixman
   make_fontconfig
-  build_conf_make_inst  http://cairographics.org/releases  rcairo-1.15.13  tar.xz  true
+  build_conf_make_inst  http://cairographics.org/releases  rcairo-1.16.2  tar.xz  true
 }
 
 ##### PANGO #####
@@ -857,37 +859,23 @@ function make_pango {
   make_cairo
   make_glib
   make_fontconfig
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.42  pango-1.42.1  tar.xz  true
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.42  pango-1.42.4  tar.xz  true
 }
 
-##### GTK2 #####
+##### GTK3 #####
 
-function patch_gtk2 {
-  rm gtk/gtk.def
-}
+function make_gtk3 {
 
-function make_gtk2 {
-  # Cygwin packet dependencies: gtk-update-icon-cache
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    make_glib
-    make_atk
-    make_pango
-    make_gdk-pixbuf
-    make_cairo
-    build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24  gtk+-2.24.32  tar.xz  patch_gtk2
-  fi
-}
-
-##### GTK3 #####
 
-function make_gtk3 {
-  make_glib
-  make_atk
-  make_pango
-  make_gdk-pixbuf
-  make_cairo
-  make_libepoxy
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22  gtk+-3.22.30  tar.xz  true
+      make_glib
+      make_atk
+      make_pango
+      make_gdk-pixbuf
+      make_cairo
+      make_libepoxy
+      build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.24  gtk+-3.24.5  tar.xz  true
+  fi
 
   # make all incl. tests and examples runs through fine
   # make install fails with issue with
@@ -918,17 +906,17 @@ function make_libxml2 {
   fi
 }
 
-##### GTK-SOURCEVIEW2 #####
+##### GTK-SOURCEVIEW3 #####
 
-function make_gtk_sourceview2 {
+function make_gtk_sourceview3 {
   # Cygwin packet dependencies: intltool
   # gtksourceview-2.11.2 requires GTK2
   # gtksourceview-2.91.9 requires GTK3
   # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    make_gtk2
+    make_gtk3
     make_libxml2
-    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/2.11  gtksourceview-2.11.2  tar.bz2  true
+    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.9  tar.bz2  true
   fi
 }
 
@@ -1018,7 +1006,7 @@ function make_ln {
 
 function make_ocaml {
   get_flex_dll_link_bin
-  if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then
+  if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then
     # See README.win32.adoc
     cp config/m-nt.h byterun/caml/m.h
     cp config/s-nt.h byterun/caml/s.h
@@ -1073,7 +1061,6 @@ function make_ocaml {
 
 function make_ocaml_tools {
   make_findlib
-  # make_camlp5
 }
 
 ##### OCAML EXTRA LIBRARIES #####
@@ -1081,8 +1068,7 @@ function make_ocaml_tools {
 function make_ocaml_libs {
   make_num
   make_findlib
-  make_lablgtk
-  # make_stdint
+  # make_lablgtk
 }
 
 ##### Ocaml num library #####
@@ -1130,6 +1116,20 @@ function make_findlib {
   fi
 }
 
+##### Dune build system #####
+
+function make_dune {
+  make_ocaml
+
+  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 ; then
+
+    log2 make release
+    log2 make install
+
+    build_post
+  fi
+}
+
 ##### MENHIR Ocaml Parser Generator #####
 
 function make_menhir {
@@ -1144,108 +1144,50 @@ function make_menhir {
   fi
 }
 
-##### CAMLP4 Ocaml Preprocessor #####
-
-function make_camlp4 {
-  # OCaml up to 4.01 includes camlp4, from 4.02 it isn't included
-  # Check if command camlp4 exists, if not build camlp4
-  if ! command camlp4 ; then
-    make_ocaml
-    make_findlib
-    if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then
-      # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910
-      logn configure ./configure
-      # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT
-      log2 make all
-      log2 make install
-      log2 make clean
-      build_post
-    fi
-  fi
-}
-
-##### CAMLP5 Ocaml Preprocessor #####
-
-function make_camlp5 {
-  make_ocaml
-  make_findlib
-
-  if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then
-    logn configure ./configure
-    # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
-    sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
-    # shellcheck disable=SC2086
-    log1 make world.opt $MAKE_OPT
-    log2 make install
-    # For some reason gramlib.a is not copied, but it is required by Coq
-    cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
-    # For some reason META is not copied, but it is required by coq_makefile
-    log2 make -C etc META
-    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    log2 make clean
-    build_post
-  fi
-}
-
 ##### LABLGTK Ocaml GTK binding #####
 
 # Note: when rebuilding lablgtk by deleting the .finished file,
 # also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib
 # Otherwise make install fails
 
-function make_lablgtk {
-  make_ocaml
-  make_findlib
-  # make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5
-  make_gtk2
-  make_gtk_sourceview2
-  if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
-    cp "/bin/$TARGET_ARCH-pkg-config"  bin_special/pkg-config
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
-
-    # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
+function make_ocaml_cairo2 {
 
-    # lablgtk binary needs to be stripped - otherwise flexdll goes wild
-    # Fix version 1: explicit strip after failed build - this randomly fails in CI
-    # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html
-    # logn make-world-pre make world || true
-    # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
+  if build_prep https://github.com/Chris00/ocaml-cairo/archive  0.6  tar.gz  1 ; then
 
-    # Fix version 2: Strip by passing linker argument rather than explicit call to strip
-    # See https://github.com/alainfrisch/flexdll/issues/6
-    # Argument to ocamlmklib: -ldopt "-link -Wl,-s"
-    # -ldopt is the okamlmklib linker prefix option
-    # -link is the flexlink linker prefix option
-    # -Wl, is the gcc (linker driver) linker prefix option
-    # -s is the gnu linker option for stripping symbols
-    # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch
-
-    log2 make world
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
+    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
 
-    # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
-    sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+    log2 dune build cairo2.install
+    log2 dune install cairo2
 
-    log2 make install
-    log2 make clean
+    log2 dune clean
     build_post
+
   fi
 }
 
-##### Ocaml Stdint #####
-
-function make_stdint {
+function make_lablgtk {
   make_ocaml
   make_findlib
-  if build_prep https://github.com/andrenth/ocaml-stdint/archive 0.3.0 tar.gz 1 Stdint-0.3.0; then
-    # Note: the setup gets the proper install path from ocamlfind, but for whatever reason it wants
-    # to create an empty folder in some folder which defaults to C:\Program Files.
-    # The --preifx overrides this. Id didn't see any files created in /tmp/extra.
-    log_1_3 ocaml setup.ml -configure --prefix /tmp/extra
-    log_1_3 ocaml setup.ml -build
-    log_1_3 ocaml setup.ml -install
-    log_1_3 ocaml setup.ml -clean
+  make_dune
+  make_gtk3
+  make_gtk_sourceview3
+  make_ocaml_cairo2
+
+  if build_prep https://github.com/garrigue/lablgtk/archive  3.0.beta5  tar.gz 1 lablgtk-3.0.beta5 ; then
+
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
+    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
+
+    # lablgtk3 includes more packages that are not relevant for Coq,
+    # such as gtkspell
+    log2 dune build -p lablgtk3
+    log2 dune install lablgtk3
+
+    log2 dune build -p lablgtk3-sourceview3
+    log2 dune install lablgtk3-sourceview3
+
+    log2 dune clean
     build_post
   fi
 }
@@ -1351,10 +1293,7 @@ function copq_coq_gtk {
     else
       COQSHARE="$PREFIXCOQ/share/"
     fi
-    if [[ ! $COQ_VERSION == 8.4* ]] ; then
-      mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-      mv "$COQSHARE"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
-    fi
+
     mkdir -p "$PREFIXCOQ/ide"
     mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
     rmdir "$PREFIXCOQ/share/coq" || true
@@ -1383,8 +1322,8 @@ function make_coq {
   make_ocaml
   make_num
   make_findlib
-  # make_camlp5
-  make_lablgtk
+  # Windows build needs tweaks for the GTK3 build
+  # make_lablgtk
   if
     case $COQ_VERSION in
       # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
@@ -1436,12 +1375,15 @@ function make_coq {
     fi
 
     log2 make install
-    log1 copy_coq_dlls
+
+    # XXX: Disabled until GTK3 support is back to the build
+    # log1 copy_coq_dlls
+    # log1 copq_coq_gtk
+
     if [ "$INSTALLOCAML" == "Y" ]; then
       copy_coq_objects
     fi
 
-    log1 copq_coq_gtk
     log1 copy_coq_license
 
     # make clean seems to be broken for 8.5pl2
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
index 2c8c46373f..2c8c46373f 100755..100644
--- a/dev/build/windows/patches_coq/VST.patch
+++ b/dev/build/windows/patches_coq/VST.patch
diff --git a/dev/build/windows/patches_coq/flexdll-0.37.patch b/dev/build/windows/patches_coq/flexdll-0.37.patch
new file mode 100644
index 0000000000..82806f9ea4
--- /dev/null
+++ b/dev/build/windows/patches_coq/flexdll-0.37.patch
@@ -0,0 +1,19 @@
+diff/patch file created on Tue, Feb 19, 2019  9:41:26 PM with:
+difftar-folder.sh tarballs/flexdll-0.37.tar.gz flexdll-0.37 1
+TARFILE= tarballs/flexdll-0.37.tar.gz
+FOLDER= flexdll-0.37
+TARSTRIP= 1
+TARPREFIX= flexdll-0.37/
+ORIGFOLDER= flexdll-0.37.orig
+--- flexdll-0.37.orig/cmdline.ml	2017-10-25 10:40:46.000000000 +0200
++++ flexdll-0.37/cmdline.ml	2019-02-19 21:41:18.157024900 +0100
+@@ -248,6 +248,9 @@
+         String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest
+     | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" ->
+         "-link" :: String.sub s 5 (String.length s - 5) :: tr rest
++    (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *)
++    | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" ->
++        "-link" :: String.sub s 4 (String.length s - 4) :: tr rest
+     | "-arg" :: x :: rest ->
+         tr (Array.to_list (Arg.read_arg x)) @ rest
+     | "-arg0" :: x :: rest ->
diff --git a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
deleted file mode 100644
index 73a098d12a..0000000000
--- a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
+++ /dev/null
@@ -1,213 +0,0 @@
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c	2015-10-27 14:58:54.422888400 +0100
-***************
-*** 80,86 ****
-  	/* If string contains prefix, check that prefix is not followed
-  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
-  	 * is not part of two-char a-with-hat symbol in string. */
-! 	return type != G_UNICODE_COMBINING_MARK &&
-  		type != G_UNICODE_ENCLOSING_MARK &&
-  		type != G_UNICODE_NON_SPACING_MARK;
-  }
---- 80,86 ----
-  	/* If string contains prefix, check that prefix is not followed
-  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
-  	 * is not part of two-char a-with-hat symbol in string. */
-! 	return type != G_UNICODE_SPACING_MARK &&
-  		type != G_UNICODE_ENCLOSING_MARK &&
-  		type != G_UNICODE_NON_SPACING_MARK;
-  }
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c	2015-10-27 14:55:30.294477600 +0100
-***************
-*** 274,280 ****
-   * containg a list of language files directories.
-   * The array is owned by @lm and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
---- 274,280 ----
-   * containg a list of language files directories.
-   * The array is owned by @lm and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
-***************
-*** 392,398 ****
-   * available languages or %NULL if no language is available. The array
-   * is owned by @lm and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
---- 392,398 ----
-   * available languages or %NULL if no language is available. The array
-   * is owned by @lm and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h	2009-11-15 00:41:33.000000000 +0100
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h	2015-10-27 14:55:30.518500000 +0100
-***************
-*** 62,74 ****
-  
-  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
-  
-  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
-  										 gchar                   **dirs);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
-  
-  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
---- 62,74 ----
-  
-  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
-  
-! const gchar* const *
-  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
-  
-  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
-  										 gchar                   **dirs);
-  
-! const gchar* const *
-  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
-  
-  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c	2015-10-27 14:55:30.545502700 +0100
-***************
-*** 310,316 ****
-   *
-   * Since: 2.0
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
---- 310,316 ----
-   *
-   * Since: 2.0
-   */
-! const gchar* const *
-  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
-***************
-*** 318,324 ****
-  	if (scheme->priv->authors == NULL)
-  		return NULL;
-  
-! 	return (G_CONST_RETURN gchar* G_CONST_RETURN *)scheme->priv->authors->pdata;
-  }
-  
-  /**
---- 318,324 ----
-  	if (scheme->priv->authors == NULL)
-  		return NULL;
-  
-! 	return (const gchar* const *)scheme->priv->authors->pdata;
-  }
-  
-  /**
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h	2010-03-29 15:02:56.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h	2015-10-27 14:55:30.565504700 +0100
-***************
-*** 61,67 ****
-  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
-  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
-  
-  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
---- 61,67 ----
-  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
-  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
-  
-  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c	2015-10-27 14:55:30.583506500 +0100
-***************
-*** 515,521 ****
-   * of string containing the search path.
-   * The array is owned by the @manager and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
---- 515,521 ----
-   * of string containing the search path.
-   * The array is owned by the @manager and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
-***************
-*** 554,560 ****
-   * of string containing the ids of the available style schemes or %NULL if no
-   * style scheme is available. The array is owned by the @manager and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
---- 554,560 ----
-   * of string containing the ids of the available style schemes or %NULL if no
-   * style scheme is available. The array is owned by the @manager and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h	2009-11-15 00:41:33.000000000 +0100
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h	2015-10-27 14:56:24.498897500 +0100
-***************
-*** 73,84 ****
-  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
-  						    				 const gchar			*path);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
-  
-  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
-  
-  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
---- 73,84 ----
-  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
-  						    				 const gchar			*path);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
-  
-  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
-  
-  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
index 23c303135d..1c6a038da9 100644
--- a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch
+++ b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
@@ -1,33 +1,12 @@
-diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with:
-difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1
-TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz
-FOLDER= lablgtk-2.18.3
+diff/patch file created on Wed, Feb 20, 2019 11:29:48 AM with:
+difftar-folder.sh tarballs/lablgtk-3.0.beta4.tar.gz lablgtk-3.0.beta4 1
+TARFILE= tarballs/lablgtk-3.0.beta4.tar.gz
+FOLDER= lablgtk-3.0.beta4
 TARSTRIP= 1
-TARPREFIX= lablgtk-2.18.3/
-ORIGFOLDER= lablgtk-2.18.3.orig
---- lablgtk-2.18.3.orig/configure	2014-10-29 08:51:05.000000000 +0100
-+++ lablgtk-2.18.3/configure	2018-04-25 10:58:54.454501600 +0200
-@@ -2667,7 +2667,7 @@
- fi
- 
- 
--if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then
-+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then
-   { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
- $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
-   OCAMLFIND=no
---- lablgtk-2.18.3.orig/src/glib.mli	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.mli	2018-04-25 10:58:54.493555500 +0200
-@@ -75,6 +75,7 @@
-   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
-   type id
-   val channel_of_descr : Unix.file_descr -> channel
-+  val channel_of_descr_socket : Unix.file_descr -> channel
-   val add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-   val remove : id -> unit
---- lablgtk-2.18.3.orig/src/glib.ml	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.ml	2018-04-25 10:58:54.479543500 +0200
+TARPREFIX= lablgtk-3.0.beta4/
+ORIGFOLDER= lablgtk-3.0.beta4.orig
+--- lablgtk-3.0.beta4.orig/src/glib.ml	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/glib.ml	2019-02-20 11:28:28.439137100 +0100
 @@ -72,6 +72,8 @@
    type id
    external channel_of_descr : Unix.file_descr -> channel
@@ -37,22 +16,18 @@ ORIGFOLDER= lablgtk-2.18.3.orig
    external remove : id -> unit = "ml_g_source_remove"
    external add_watch :
      cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
---- lablgtk-2.18.3.orig/src/Makefile	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/Makefile	2018-04-25 10:58:54.506522500 +0200
-@@ -461,9 +461,9 @@
- 	  do rm -f "$(BINDIR)"/$$f; done
- 
- lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS)
--	$(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+	$(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx)
--	$(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+	$(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS)
- 
- lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS)
---- lablgtk-2.18.3.orig/src/ml_glib.c	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/ml_glib.c	2018-04-25 10:58:54.539535600 +0200
+--- lablgtk-3.0.beta4.orig/src/glib.mli	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/glib.mli	2019-02-20 11:28:28.423592200 +0100
+@@ -75,6 +75,7 @@
+   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
+   type id
+   val channel_of_descr : Unix.file_descr -> channel
++  val channel_of_descr_socket : Unix.file_descr -> channel
+   val add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+   val remove : id -> unit
+--- lablgtk-3.0.beta4.orig/src/ml_glib.c	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/ml_glib.c	2019-02-20 11:28:28.455395900 +0100
 @@ -25,6 +25,8 @@
  #include <string.h>
  #include <locale.h>
@@ -74,7 +49,7 @@ ORIGFOLDER= lablgtk-2.18.3.orig
  #include "wrappers.h"
  #include "ml_glib.h"
  #include "glib_tags.h"
-@@ -325,14 +332,23 @@
+@@ -326,14 +333,23 @@
  
  #ifndef _WIN32
  ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
index 1afa6e7f95..1afa6e7f95 100755..100644
--- a/dev/build/windows/patches_coq/quickchick.patch
+++ b/dev/build/windows/patches_coq/quickchick.patch
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index c95bcf5573..e553cbed1b 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-11-V1"
+# CACHEKEY: "bionic_coq-V2019-03-12-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -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)
-        libgtk3.0-dev libgtksourceview3.0-dev \
+        libgtksourceview-3.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 \
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -41,7 +41,10 @@ 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="lablgtk3 conf-gtksourceview3"
+ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
+
+# Must add this to COQIDE_OPAM{,_EDGE} when we update the opam
+# packages "lablgtk3-gtksourceview3"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
@@ -53,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="lablgtk3 conf-gtksourceview3" \
+    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \
     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 5082d84c4f..e3e61609af 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 lablgtk3.sourceview3))
+ (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
 
 (rule
  (targets coqide_os_specific.ml)
diff --git a/ide/ide.mllib b/ide/ide.mllib
index a7ade71307..30ac5c9ad7 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,6 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Topfmt
 Ideutils
 Coq
 Coq_lex
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index d753687077..755a42eadd 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -15,6 +15,9 @@ class type detachable_signals =
     method detached : callback:(GObj.widget -> unit) -> unit
   end
 
+(* Cannot do a local warning in 4.05.0, fixme when we use a newer
+   OCaml to avoid the warning in the method itself. *)
+[@@@ocaml.warning "-7"]
 class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
 
   object(self)