Skip to content

Commit

Permalink
Backport PR coq#10360: Resolve coq#9885 CoqIDE does not work on Windows
Browse files Browse the repository at this point in the history
  • Loading branch information
vbgl committed Jun 13, 2019
2 parents d1bb1f3 + c333f8e commit 98b1857
Show file tree
Hide file tree
Showing 3 changed files with 163 additions and 29 deletions.
8 changes: 7 additions & 1 deletion dev/build/windows/MakeCoq_MinGW.bat
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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%" ^
Expand All @@ -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 ^
Expand Down
87 changes: 59 additions & 28 deletions dev/build/windows/makecoq_mingw.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 #####
Expand All @@ -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"
Expand Down Expand Up @@ -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
}

Expand Down Expand Up @@ -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
}

Expand Down Expand Up @@ -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
Expand Down
97 changes: 97 additions & 0 deletions dev/build/windows/patches_coq/ocaml-4.07.1.patch
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 98b1857

Please sign in to comment.