Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2020-03-30 23:02:48 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.3160 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Mar 30 23:02:48 2020 rev:3 rq:789593 version:8.11.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2020-02-15 22:26:17.867338191 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.3160/coq.changes 2020-03-30 23:02:52.176158271 +0200 @@ -1,0 +2,6 @@ +Sun Mar 29 21:42:13 UTC 2020 - Aaron Puchert <[email protected]> + +- The num library is required for OCaml 4.06 or later. +- Add ocaml-410-build.patch: fix build with OCaml 4.10. + +------------------------------------------------------------------- New: ---- ocaml-410-build.patch ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.raEcIq/_old 2020-03-30 23:02:53.984159301 +0200 +++ /var/tmp/diff_new_pack.raEcIq/_new 2020-03-30 23:02:53.992159306 +0200 @@ -1,7 +1,7 @@ # # spec file for package coq # -# Copyright (c) 2019 SUSE LLC +# Copyright (c) 2020 SUSE LLC # Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de # # All modifications and additions to the file contributed by third parties @@ -28,6 +28,8 @@ Source1: coq.desktop Source2: coq.xml Source100: %{name}-rpmlintrc +# https://github.com/ppedrot/coq/commit/ae000c9efc256675ce1d56ba27ed7f99e0540ff3 +Patch1: ocaml-410-build.patch BuildRequires: desktop-file-utils BuildRequires: memory-constraints # Required for standard coq: @@ -43,6 +45,7 @@ BuildRequires: update-desktop-files BuildRequires: ocamlfind(findlib) BuildRequires: ocamlfind(lablgtk3) +BuildRequires: ocamlfind(num) BuildRequires: pkgconfig(gdk-3.0) BuildRequires: pkgconfig(gtk+-3.0) BuildRequires: pkgconfig(gtksourceview-3.0) @@ -76,6 +79,7 @@ %prep %setup -q +%patch1 -p1 %build export CFLAGS='%{optflags}' ++++++ ocaml-410-build.patch ++++++ >From 31ad892b8c9697704af70644b66ce01dd052f12e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <[email protected]> Date: Tue, 12 Nov 2019 10:57:23 +0100 Subject: [PATCH 1/2] Use the Alloc_small macro from the OCaml runtime rather than our own. We cannot use caml_alloc_small because the macros Setup_for_gc and Restore_after_gc are still relevant (and critical). This means defining the CAML_INTERNALS macro, but it is a legit use and actually documented in the OCaml manual. This will help with forward compatibility with OCaml compilers, e.g., issue #10603. Unfortunately, it also means that we can no longer use #9914 to prevent memory corruption. The old macro is still used for OCaml versions prior to 4.10, as the upstream macro might process Ctrl+C when it is called. (cherry picked from commit a028a97005b88a66a9d6dbaa4f0ade38859beffb) --- kernel/byterun/coq_interp.c | 22 ++++++++++++++++++++-- kernel/byterun/coq_memory.c | 7 +++++-- 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e3283931898..3efc55c6b44 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,17 +16,35 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <math.h> + +#define CAML_INTERNALS #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> -#include <math.h> -#include "coq_gc.h" + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" #include "coq_float64.h" +#if OCAML_VERSION < 41000 +#undef Alloc_small +#define Alloc_small(result, wosize, tag) do{ \ + young_ptr -= Bhsize_wosize (wosize); \ + if (young_ptr < young_limit){ \ + young_ptr += Bhsize_wosize (wosize); \ + Setup_for_gc; \ + minor_collection (); \ + Restore_after_gc; \ + young_ptr -= Bhsize_wosize (wosize); \ + } \ + Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ + (result) = Val_hp (young_ptr); \ + }while(0) +#endif + #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" #else diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index a1c49bee95b..76a24f6f2b8 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -9,10 +9,13 @@ /***********************************************************************/ #include <stdio.h> -#include <string.h> +#include <string.h> + +#define CAML_INTERNALS #include <caml/alloc.h> #include <caml/address_class.h> -#include "coq_gc.h" +#include <caml/roots.h> + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" >From fb48d0823fbb6507299ec53bc324fa3550e6d327 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <[email protected]> Date: Mon, 9 Mar 2020 15:15:44 +0100 Subject: [PATCH 2/2] Do not rely on the implicit declaration of caml_minor_collection. This commit also prefixes young_ptr and young_limit along the way, so as to not rely on OCaml's compatibility layer. This is a gratuitous change, since this code is only meant to be compiled with OCaml < 4.10 anyway. (cherry picked from commit 4666a8b9596f8cb87b63c345f6e57348f0bfda6d) --- kernel/byterun/coq_interp.c | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 3efc55c6b44..776a7c33430 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -30,18 +30,20 @@ #include "coq_float64.h" #if OCAML_VERSION < 41000 +extern void caml_minor_collection(void); + #undef Alloc_small #define Alloc_small(result, wosize, tag) do{ \ - young_ptr -= Bhsize_wosize (wosize); \ - if (young_ptr < young_limit){ \ - young_ptr += Bhsize_wosize (wosize); \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + if (caml_young_ptr < caml_young_limit) { \ + caml_young_ptr += Bhsize_wosize(wosize); \ Setup_for_gc; \ - minor_collection (); \ + caml_minor_collection(); \ Restore_after_gc; \ - young_ptr -= Bhsize_wosize (wosize); \ + caml_young_ptr -= Bhsize_wosize(wosize); \ } \ - Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ - (result) = Val_hp (young_ptr); \ + Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \ + (result) = Val_hp(caml_young_ptr); \ }while(0) #endif
