aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--Makefile.ide21
-rw-r--r--configure.ml93
-rw-r--r--coqide.opam6
-rw-r--r--default.nix5
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat2
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh204
-rw-r--r--[-rwxr-xr-x]dev/build/windows/patches_coq/VST.patch0
-rw-r--r--dev/build/windows/patches_coq/flexdll-0.37.patch19
-rw-r--r--dev/build/windows/patches_coq/gtksourceview-2.11.2.patch213
-rw-r--r--dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch (renamed from dev/build/windows/patches_coq/lablgtk-2.18.6.patch)67
-rw-r--r--[-rwxr-xr-x]dev/build/windows/patches_coq/quickchick.patch0
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile13
-rw-r--r--ide/dune2
-rw-r--r--ide/ide.mllib1
-rw-r--r--ide/wg_Detachable.ml3
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:03:53 +0000