aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/CODEOWNERS12
-rw-r--r--dev/build/windows/makecoq_mingw.sh25
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.3.patch44
-rw-r--r--lib/control.ml5
-rw-r--r--lib/control.mli5
5 files changed, 67 insertions, 24 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 74bbda5533..ab9725c967 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -71,6 +71,11 @@
/engine/ @ppedrot
# Secondary maintainer @aspiwack
+/engine/universes.* @SkySkimmer
+/engine/univops.* @SkySkimmer
+/engine/uState.* @SkySkimmer
+# Secondary maintainer @mattam82
+
########## Grammar macros ##########
/grammar/ @ppedrot
@@ -94,6 +99,11 @@
/kernel/byterun/ @maximedenes
# Secondary maintainer @silene
+/kernel/sorts.* @SkySkimmer
+/kernel/uGraph.* @SkySkimmer
+/kernel/univ.* @SkySkimmer
+# Secondary maintainer @mattam82
+
########## Library ##########
/library/ @silene
@@ -291,7 +301,7 @@
########## Build system ##########
/Makefile* @letouzey
-# Secondary maintainer @maximdenes
+# Secondary maintainer @gares
/configure* @letouzey
# Secondary maintainer @ejgallego
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 18f1a2f165..f4ec218b6b 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -144,24 +144,24 @@ LOGTARGET=other
# Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
log1() {
- "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
}
# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
log2() {
- "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
}
# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
log_1_3() {
- "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
}
# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
logn() {
LOGTARGETEX=$1
shift
- "$@" > "$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2> "$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
}
###################### 'UNFIX' SED #####################
@@ -954,9 +954,20 @@ function make_lablgtk {
# lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
- # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
- logn make-world-pre make world || true
- "$TARGET_ARCH-strip.exe" --strip-unneeded src/dlllablgtk2.dll
+ # 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
log2 make install
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
index 0691c1fc8f..23c303135d 100644
--- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
+++ b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
@@ -1,6 +1,12 @@
-diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
---- lablgtk-2.18.3/configure 2014-10-29 08:51:05.000000000 +0100
-+++ lablgtk-2.18.3.patched/configure 2015-10-29 08:58:08.543985500 +0100
+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
+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
@@ -10,10 +16,8 @@ diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
$as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
OCAMLFIND=no
-
-diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
---- lablgtk-2.18.3/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/glib.mli 2016-01-25 09:50:59.884715200 +0100
+--- 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
@@ -22,10 +26,8 @@ diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
val add_watch :
cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
val remove : id -> unit
-
-diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
---- lablgtk-2.18.3/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/glib.ml 2016-01-25 09:50:59.891715900 +0100
+--- 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
@@ -72,6 +72,8 @@
type id
external channel_of_descr : Unix.file_descr -> channel
@@ -35,10 +37,22 @@ diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
external remove : id -> unit = "ml_g_source_remove"
external add_watch :
cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-
-diff -u -r lablgtk-2.18.3/src/ml_glib.c lablgtk-2.18.3.patched/src/ml_glib.c
---- lablgtk-2.18.3/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/ml_glib.c 2016-01-25 09:50:59.898716600 +0100
+--- 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
@@ -25,6 +25,8 @@
#include <string.h>
#include <locale.h>
diff --git a/lib/control.ml b/lib/control.ml
index e67cd8b38d..3fbeb168c4 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with
| "Unix" | "Cygwin" -> { timeout = unix_timeout }
| _ -> { timeout = windows_timeout }
-let timeout n f e = timeout_fun.timeout n f e
+let timeout_fun_ref = ref timeout_fun
+let set_timeout f = timeout_fun_ref := f
+
+let timeout n f e = !timeout_fun_ref.timeout n f e
diff --git a/lib/control.mli b/lib/control.mli
index 415e054625..59e2a15158 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit
val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b
(** [timeout n f x e] tries to compute [f x], and if it fails to do so
before [n] seconds, it raises [e] instead. *)
+
+(** Set a particular timeout function; warning, this is an internal
+ API and it is scheduled to go away. *)
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
+val set_timeout : timeout -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:24:03 +0000