Merge PR #9279: CoqIDE on lablgtk3

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

9 files changed, 179 insertions, 421 deletions

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..4c5bd29236 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
 }
 
@@ -977,7 +965,7 @@ function get_flex_dll_link_bin {
 # Build flexdll and flexlink from sources after building OCaml
 
 function make_flex_dll_link {
-  if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then
+  if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then
     if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
       # shellcheck disable=SC2086
       log1 make $MAKE_OPT build_mingw flexlink.exe
@@ -1014,11 +1002,21 @@ function make_ln {
   fi
 }
 
+##### ARCH-pkg-config replacement #####
+
+# cygwin replaced ARCH-pkg-config with a shell script, which doesn't work e.g. for dune on Windows.
+# This builds a binary replacement for the shell script and puts it into the bin_special folder.
+# There is no global installation since it is module specific what pkg-config is needed under what name.
+
+function make_arch_pkg_config {
+  gcc -DARCH="$TARGET_ARCH" -o bin_special/pkg-config.exe $PATCHES/pkg-config.c
+}
+
 ##### OCAML #####
 
 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 +1071,6 @@ function make_ocaml {
 
 function make_ocaml_tools {
   make_findlib
-  # make_camlp5
 }
 
 ##### OCAML EXTRA LIBRARIES #####
@@ -1082,7 +1079,6 @@ function make_ocaml_libs {
   make_num
   make_findlib
   make_lablgtk
-  # make_stdint
 }
 
 ##### Ocaml num library #####
@@ -1130,6 +1126,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 dune-1.6.3 ; then
+
+    log2 make release
+    log2 make install
+
+    build_post
+  fi
+}
+
 ##### MENHIR Ocaml Parser Generator #####
 
 function make_menhir {
@@ -1144,108 +1154,44 @@ 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
-
-    # 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
-
-    # 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
-
-    # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
-    sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+function make_ocaml_cairo2 {
+  if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then
+    make_arch_pkg_config
 
-    log2 make install
-    log2 make clean
+    log2 dune build cairo2.install
+    log2 dune install cairo2
+    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
+    make_arch_pkg_config
+
+    # 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
 }
@@ -1270,42 +1216,44 @@ function copy_coq_dlls {
   # Select all missing DLLs from the module list, right click "copy filenames"
   # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line)
   # Do this recursively until there are no further missing DLLs (File close + reopen)
-  # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script.
+  # For running this quickly, just do "cd coq-<ver> ; copy_coq_dlls ; cd .." at the end of this script.
   # Do the same for coqc and ocamlc (usually doesn't result in additional files)
 
-  copy_coq_dll LIBATK-1.0-0.DLL
   copy_coq_dll LIBCAIRO-2.DLL
-  copy_coq_dll LIBEXPAT-1.DLL
-  copy_coq_dll LIBFFI-6.DLL
   copy_coq_dll LIBFONTCONFIG-1.DLL
   copy_coq_dll LIBFREETYPE-6.DLL
-  copy_coq_dll LIBGDK-WIN32-2.0-0.DLL
+  copy_coq_dll LIBGDK-3-0.DLL
   copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL
-  copy_coq_dll LIBGIO-2.0-0.DLL
   copy_coq_dll LIBGLIB-2.0-0.DLL
-  copy_coq_dll LIBGMODULE-2.0-0.DLL
   copy_coq_dll LIBGOBJECT-2.0-0.DLL
-  copy_coq_dll LIBGTK-WIN32-2.0-0.DLL
-  copy_coq_dll LIBINTL-8.DLL
+  copy_coq_dll LIBGTK-3-0.DLL
+  copy_coq_dll LIBGTKSOURCEVIEW-3.0-1.DLL
   copy_coq_dll LIBPANGO-1.0-0.DLL
+  copy_coq_dll LIBATK-1.0-0.DLL
+  copy_coq_dll LIBBZ2-1.DLL
+  copy_coq_dll LIBCAIRO-GOBJECT-2.DLL
+  copy_coq_dll LIBEPOXY-0.DLL
+  copy_coq_dll LIBEXPAT-1.DLL
+  copy_coq_dll LIBFFI-6.DLL
+  copy_coq_dll LIBGIO-2.0-0.DLL
+  copy_coq_dll LIBGMODULE-2.0-0.DLL
+  copy_coq_dll LIBINTL-8.DLL
   copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL
   copy_coq_dll LIBPANGOWIN32-1.0-0.DLL
-  copy_coq_dll libpcre-1.dll
+  copy_coq_dll LIBPCRE-1.DLL
   copy_coq_dll LIBPIXMAN-1-0.DLL
   copy_coq_dll LIBPNG16-16.DLL
   copy_coq_dll LIBXML2-2.DLL
   copy_coq_dll ZLIB1.DLL
+  copy_coq_dll ICONV.DLL
+  copy_coq_dll LIBLZMA-5.DLL
+  copy_coq_dll LIBPANGOFT2-1.0-0.DLL
+  copy_coq_dll LIBHARFBUZZ-0.DLL
 
   # Depends on if GTK is built from sources
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    copy_coq_dll libiconv-2.dll
-  else
-    copy_coq_dll ICONV.DLL
-    copy_coq_dll LIBBZ2-1.DLL
-    copy_coq_dll LIBGTKSOURCEVIEW-2.0-0.DLL
-    copy_coq_dll LIBHARFBUZZ-0.DLL
-    copy_coq_dll LIBLZMA-5.DLL
-    copy_coq_dll LIBPANGOFT2-1.0-0.DLL
+    echo "Building GTK from sources is currently not supported"
+    exit 1
   fi;
 
   # Architecture dependent files
@@ -1335,14 +1283,14 @@ function copy_coq_objects {
 
 # Copy required GTK config and suport files
 
-function copq_coq_gtk {
-  echo 'gtk-theme-name = "MS-Windows"'     >  "$PREFIX/etc/gtk-2.0/gtkrc"
-  echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-2.0/gtkrc"
+function copy_coq_gtk {
+  echo 'gtk-theme-name = "Default"'     >  "$PREFIX/etc/gtk-3.0/gtkrc"
+  echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-3.0/gtkrc"
 
   if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    install_glob "$PREFIX/etc/gtk-2.0" '*'                            "$PREFIXCOQ/gtk-2.0"
-    install_glob "$PREFIX/share/gtksourceview-2.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-    install_glob "$PREFIX/share/gtksourceview-2.0/styles" '*'         "$PREFIXCOQ/share/gtksourceview-2.0/styles"
+    install_glob "$PREFIX/etc/gtk-3.0" '*'                            "$PREFIXCOQ/gtk-3.0"
+    install_glob "$PREFIX/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
+    install_glob "$PREFIX/share/gtksourceview-3.0/styles" '*'         "$PREFIXCOQ/share/gtksourceview-3.0/styles"
     install_rec  "$PREFIX/share/themes" '*'                           "$PREFIXCOQ/share/themes"
 
     # This below item look like a bug in make install
@@ -1351,10 +1299,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,7 +1328,6 @@ function make_coq {
   make_ocaml
   make_num
   make_findlib
-  # make_camlp5
   make_lablgtk
   if
     case $COQ_VERSION in
@@ -1437,11 +1381,12 @@ function make_coq {
 
     log2 make install
     log1 copy_coq_dlls
+    log1 copy_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/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c
new file mode 100755
index 0000000000..e4fdcd4d7d
--- /dev/null
+++ b/dev/build/windows/patches_coq/pkg-config.c
@@ -0,0 +1,29 @@
+// MinGW personality wrapper for pkgconf
+// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config
+// Compile with e.g.
+// gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe
+// gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe
+// ATTENTION: Do not compile with MinGW-gcc, compile with cygwin gcc!
+//
+// To test it execute e.g.
+// $ ./pkg-config --path zlib
+// /usr/x86_64-w64-mingw32/sys-root/mingw/lib/pkgconfig/zlib.pc
+
+#include <unistd.h>
+
+#define STRINGIFY1(arg) #arg
+#define STRINGIFY(arg) STRINGIFY1(arg)
+
+int main(int argc, char *argv[])
+{
+    // +1 for extra argument, +1 for trailing NULL
+    char * argvnew[argc+2];
+    int id=0, is=0;
+
+    argvnew[id++] = argv[is++];
+    argvnew[id++] = "--personality="STRINGIFY(ARCH);
+    while( is<argc ) argvnew[id++] = argv[is++];
+    argvnew[id++] = 0;
+
+    return execv("/usr/bin/pkgconf", argvnew);
+}
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 ac763547b6..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)
-        libgtk2.0-dev libgtksourceview2.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="lablgtk.2.18.5 conf-gtksourceview.2"
+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="lablgtk.2.18.6 conf-gtksourceview.2" \
+    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