coq · ejgallego · Jun 13, 2019 · Jun 9, 2019
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
@@ -331,7 +331,9 @@ IF "%CYGWIN_QUIET%" == "Y" (
 )
 
 IF "%GTK_FROM_SOURCES%"=="N" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-libxml2
+  REM gtksourceview3 is always built from sources until the bug in DLLMain is fixed in cygwin
+  REM SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtksourceview3.0
 )
 
 REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
@@ -362,6 +364,9 @@ IF NOT "%APPVEYOR%" == "True" (
 
 ECHO "========== INSTALL CYGWIN =========="
 
+REM If you need to add packages, see https://cygwin.com/packages/package_list.html for package names
+REM In the description of each package you also find the file list and maintainer there
+
 IF "%RUNSETUP%"=="Y" (
   %SETUP% ^
     --proxy "%PROXY%" ^
@@ -376,6 +381,7 @@ IF "%RUNSETUP%"=="Y" (
     -P pkg-config ^
     -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
     -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+    -P adwaita-icon-theme ^
     -P libiconv-devel,libunistring-devel,libncurses-devel ^
     -P gettext-devel,libgettextpo-devel ^
     -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
@@ -104,7 +104,8 @@ cd /build
 mkdir -p "$SOURCE_LOCAL_CACHE_CFMT"
 
 # sysroot prefix for the above /build/host/target combination
-PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
+# This must be in MFMT (C:/.../) because the OCaml library path is based on it and OCaml is a MinGW application.
+PREFIXMINGW=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
 
 # Install / Prefix folder for COQ
 PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
@@ -113,10 +114,10 @@ PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
 if [ "$INSTALLOCAML" == "Y" ]; then
   PREFIXOCAML=$PREFIXCOQ
 else
-  PREFIXOCAML=$PREFIX
+  PREFIXOCAML=$PREFIXMINGW
 fi
 
-mkdir -p "$PREFIX/bin"
+mkdir -p "$PREFIXMINGW/bin"
 mkdir -p "$PREFIXCOQ/bin"
 mkdir -p "$PREFIXOCAML/bin"
 
@@ -487,7 +488,7 @@ function build_post {
 function build_conf_make_inst {
   if build_prep "$1" "$2" "$3" ; then
     $4
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" "${@:5}"
+    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" "${@:5}"
     # shellcheck disable=SC2086
     log1 make $MAKE_OPT
     log2 make install
@@ -895,9 +896,9 @@ function make_libxml2 {
   # Note: latest release version 2.9.2 fails during configuring lzma, so using 2.9.1
   # Note: python binding requires <sys/select.h> which doesn't exist on cygwin
   if build_prep https://git.gnome.org/browse/libxml2/snapshot  libxml2-2.9.1  tar.xz ; then
-    # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --disable-shared --without-python
+    # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXMINGW" --disable-shared --without-python
     # shared library required by gtksourceview
-    ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" --without-python
+    ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" --without-python
     # shellcheck disable=SC2086
     log1 make $MAKE_OPT all
     log2 make install
@@ -910,14 +911,13 @@ function make_libxml2 {
 
 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
+  # Note: this is always built from sources cause of a bug in the cygwin delivery.
+  # Just dependencies are only built if we build from sources
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
     make_gtk3
     make_libxml2
-    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.9  tar.bz2  true
   fi
+  build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.11  tar.xz  make_arch_pkg_config
 }
 
 ##### FLEXDLL FLEXLINK #####
@@ -930,7 +930,7 @@ function make_gtk_sourceview3 {
 # Install flexdll objects
 
 function install_flexdll {
-  cp flexdll.h "/usr/$TARGET_ARCH/sys-root/mingw/include"
+  cp flexdll.h "$PREFIXMINGW/include"
   if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
     cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
     cp flexdll*_mingw.o "$PREFIXOCAML/bin"
@@ -1202,7 +1202,7 @@ function make_lablgtk {
 
 function copy_coq_dll {
   if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    cp "/usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1" "$PREFIXCOQ/bin/$1"
+    cp "$PREFIXMINGW/bin/$1" "$PREFIXCOQ/bin/$1"
   fi
 }
 
@@ -1282,27 +1282,58 @@ function copy_coq_objects {
 }
 
 # Copy required GTK config and support files
+# This must be called from inside the coq build folder!
 
 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"
+
+  glib-compile-schemas $PREFIXMINGW/share/glib-2.0/schemas/
+  echo 'gtk-theme-name = "Default"'     >  "$PREFIXMINGW/etc/gtk-3.0/gtkrc"
 
   if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    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"
+    install_glob  "$PREFIXMINGW/etc/gtk-3.0" '*'                                 "$PREFIXCOQ/gtk-3.0"
+    install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled"        "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
+
+    install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*'      "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
+    install -D -T "ide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+    install -D -T "ide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+
+    install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*'              "$PREFIXCOQ/share/gtksourceview-3.0/styles"
+    install -D -T "ide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+
+    install_rec   "$PREFIXMINGW/share/themes" '*'                                "$PREFIXCOQ/share/themes"
+
+    FOLDERS=""
+    # The sizes include all default sizes given in index.theme
+    # The types used haven been recorded with ProcMon in an installation with all icons present
+    for SIZE in 16x16 22x22 32x32 48x48; do
+      for TYPE in \
+        actions/bookmark actions/document devices/drive actions/format-text actions/go actions/list \
+        actions/media actions/pan actions/process actions/system actions/window \
+        mimetypes/text places/folder places/user status/dialog
+      do
+        CLASS=$(dirname $TYPE)
+        ICON=$(basename $TYPE)
+        if [[ ! "$FOLDERS" =~ "$SIZE/$CLASS" ]] ;then
+          FOLDERS="$FOLDERS$SIZE/$CLASS,"
+        fi
+        install_rec "/usr/share/icons/Adwaita/$SIZE/$CLASS" "$ICON*"  "$PREFIXCOQ/share/icons/Adwaita/$SIZE/$CLASS"
+      done
+    done
+    echo Folders=$FOLDERS
+    install -D -T "/usr/share/icons/Adwaita/index.theme" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
+    sed -i "s|^Directories=.*|Directories=$FOLDERS|" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
+    gtk-update-icon-cache -f "$PREFIXCOQ/share/icons/Adwaita/"
 
     # This below item look like a bug in make install
-    if [ -d "$PREFIXCOQ/share/coq/" ] ; then
-      COQSHARE="$PREFIXCOQ/share/coq/"
-    else
-      COQSHARE="$PREFIXCOQ/share/"
-    fi
-
-    mkdir -p "$PREFIXCOQ/ide"
-    mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
-    rmdir "$PREFIXCOQ/share/coq" || true
+    # if [ -d "$PREFIXCOQ/share/coq/" ] ; then
+    #   COQSHARE="$PREFIXCOQ/share/coq/"
+    # else
+    #   COQSHARE="$PREFIXCOQ/share/"
+    # fi
+
+    # mkdir -p "$PREFIXCOQ/ide"
+    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    # rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
 
@@ -1454,7 +1485,7 @@ function make_gcc {
         --enable-languages=c --disable-nls \
         --disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
         # --disable-decimal-float seems to be required
-        # --with-sysroot="$PREFIX"  results in configure error that this is not an absolute path
+        # --with-sysroot="$PREFIXMINGW"  results in configure error that this is not an absolute path
     # shellcheck disable=SC2086
     log1 make $MAKE_OPT
     log2 make install

diff --git a/dev/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
@@ -0,0 +1,97 @@
+diff/patch file created on Tue, Jun 11, 2019 10:15:38 AM with:
+difftar-folder.sh tarballs/ocaml-4.07.1.tar.gz ocaml-4.07.1 1
+TARFILE= tarballs/ocaml-4.07.1.tar.gz
+FOLDER= ocaml-4.07.1/
+TARSTRIP= 1
+TARPREFIX= ocaml-4.07.1/
+ORIGFOLDER= ocaml-4.07.1.orig
+--- ocaml-4.07.1.orig/byterun/caml/osdeps.h	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/caml/osdeps.h	2019-06-11 10:13:50.766997600 +0200
+@@ -98,6 +98,11 @@
+ */
+ extern char_os *caml_secure_getenv(char_os const *var);
+
++/* Modify or delete environment variable.
++   Returns 0 on success or an error code.
++*/
++extern int caml_putenv(char_os const *var, char_os const *value);
++
+ /* If [fd] refers to a terminal or console, return the number of rows
+    (lines) that it displays.  Otherwise, or if the number of rows
+    cannot be determined, return -1. */
+--- ocaml-4.07.1.orig/byterun/debugger.c	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/debugger.c	2019-06-11 10:14:02.706013700 +0200
+@@ -180,6 +180,7 @@
+   if (address == NULL) return;
+   if (dbg_addr != NULL) caml_stat_free(dbg_addr);
+   dbg_addr = address;
++  caml_putenv(_T("CAML_DEBUG_SOCKET"),_T(""));
+
+ #ifdef _WIN32
+   winsock_startup();
+--- ocaml-4.07.1.orig/byterun/unix.c	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/unix.c	2019-06-11 10:14:11.252438800 +0200
+@@ -430,6 +430,19 @@
+ #endif
+ }
+
++int caml_putenv(char_os const *var, char_os const *value)
++{
++  char_os * s;
++  int ret;
++
++  s = caml_stat_strconcat_os(3, var, _T("="), value);
++  ret = putenv_os(s);
++  if (ret == -1) {
++    caml_stat_free(s);
++  }
++  return ret;
++}
++
+ int caml_num_rows_fd(int fd)
+ {
+ #ifdef TIOCGWINSZ
+--- ocaml-4.07.1.orig/byterun/win32.c	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/win32.c	2019-06-11 10:14:19.485640700 +0200
+@@ -727,6 +727,19 @@
+   return _wgetenv(var);
+ }
+
++int caml_putenv(char_os const *var, char_os const *value)
++{
++  char_os * s;
++  int ret;
++
++  s = caml_stat_strconcat_os(3, var, _T("="), value);
++  ret = putenv_os(s);
++  if (ret == -1) {
++    caml_stat_free(s);
++  }
++  return ret;
++}
++
+ /* caml_win32_getenv is used to implement Sys.getenv and Unix.getenv in such a
+    way that they get direct access to the Win32 environment rather than to the
+    copy that is cached by the C runtime system. The result of caml_win32_getenv
+--- ocaml-4.07.1.orig/config/Makefile.mingw	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1//config/Makefile.mingw	2019-06-11 10:14:44.492969800 +0200
+@@ -89,7 +89,7 @@
+ NATDYNLINK=true
+ NATDYNLINKOPTS=
+ CMXS=cmxs
+-RUNTIMED=false
++RUNTIMED=true
+ ASM_CFI_SUPPORTED=false
+ WITH_FRAME_POINTERS=false
+ UNIX_OR_WIN32=win32
+--- ocaml-4.07.1.orig/config/Makefile.mingw64	2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1//config/Makefile.mingw64	2019-06-11 10:14:53.664784900 +0200
+@@ -89,7 +89,7 @@
+ NATDYNLINK=true
+ NATDYNLINKOPTS=
+ CMXS=cmxs
+-RUNTIMED=false
++RUNTIMED=true
+ ASM_CFI_SUPPORTED=false
+ WITH_FRAME_POINTERS=false
+ UNIX_OR_WIN32=win32