---
...3f6dbccd4b280acad395b9a2683a645a9de3.patch | 163 ++++++++++++++++++
non-free/compcert/APKBUILD | 6 +-
non-free/compcert/coq-8.9.1-support.patch | 26 +++
3 files changed, 194 insertions(+), 1 deletion(-)
create mode 100644 non-free/compcert/96383f6dbccd4b280acad395b9a2683a645a9de3.patch
create mode 100644 non-free/compcert/coq-8.9.1-support.patch
diff --git a/non-free/compcert/96383f6dbccd4b280acad395b9a2683a645a9de3.patch b/non-free/compcert/96383f6dbccd4b280acad395b9a2683a645a9de3.patch
new file mode 100644
index 0000000000..308575e868
--- /dev/null
+++ b/non-free/compcert/96383f6dbccd4b280acad395b9a2683a645a9de3.patch
@@ -0,0 +1,163 @@
+commit 96383f6dbccd4b280acad395b9a2683a645a9de3
+Author: Xavier Leroy <xavierleroy@users.noreply.github.com>
+Date: Mon Jul 8 10:48:24 2019 +0200
+
+ Compatibility with OCaml 4.08 (#302)
+
+ * Do not use `Pervasives.xxx` qualified names
+
+ Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
+ and uses of `Pervasives` cause fatal warnings.
+
+ This commit uses unqualified names instead, as no ambiguity occurs.
+
+ * Clarify "open" statements
+
+ OCaml 4.08.0 has stricter warnings concerning open statements that
+ shadow module names.
+
+ Closes: #300
+
+diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
+index 46d5c3f1..902724e0 100644
+--- a/backend/Linearizeaux.ml
++++ b/backend/Linearizeaux.ml
+@@ -106,7 +106,7 @@ let flatten_blocks blks =
+ let cmp_minpc (mpc1, _) (mpc2, _) =
+ if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1
+ in
+- List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks))
++ List.flatten (List.map snd (List.sort cmp_minpc blks))
+
+ (* Build the enumeration *)
+
+diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
+index dd428808..155f5e55 100644
+--- a/backend/PrintAsm.ml
++++ b/backend/PrintAsm.ml
+@@ -13,7 +13,6 @@
+
+ open AST
+ open Camlcoq
+-open DwarfPrinter
+ open PrintAsmaux
+ open Printf
+ open Sections
+@@ -177,7 +176,7 @@ module Printer(Target:TARGET) =
+ let address = Target.address
+ end
+
+- module DebugPrinter = DwarfPrinter (DwarfTarget)
++ module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget)
+ end
+
+ let print_program oc p =
+diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
+index f68c1267..8c255a65 100644
+--- a/backend/PrintCminor.ml
++++ b/backend/PrintCminor.ml
+@@ -16,7 +16,7 @@
+ (** Pretty-printer for Cminor *)
+
+ open Format
+-open Camlcoq
++open !Camlcoq
+ open Integers
+ open AST
+ open PrintAST
+diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
+index d0557073..1c449e74 100644
+--- a/backend/PrintLTL.ml
++++ b/backend/PrintLTL.ml
+@@ -112,7 +112,7 @@ let print_function pp id f =
+ fprintf pp "%s() {\n" (extern_atom id);
+ let instrs =
+ List.sort
+- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
++ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+ (List.rev_map
+ (fun (pc, i) -> (P.to_int pc, i))
+ (PTree.elements f.fn_code)) in
+diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
+index ba336b0a..841540b6 100644
+--- a/backend/PrintRTL.ml
++++ b/backend/PrintRTL.ml
+@@ -93,7 +93,7 @@ let print_function pp id f =
+ fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+ let instrs =
+ List.sort
+- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
++ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+ (List.rev_map
+ (fun (pc, i) -> (P.to_int pc, i))
+ (PTree.elements f.fn_code)) in
+diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
+index cc1f7d49..6432682a 100644
+--- a/backend/PrintXTL.ml
++++ b/backend/PrintXTL.ml
+@@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f =
+ fprintf pp "f() {\n";
+ let instrs =
+ List.sort
+- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
++ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+ (List.map
+ (fun (pc, i) -> (P.to_int pc, i))
+ (PTree.elements f.fn_code)) in
+diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
+index 5ff58780..7a2f4828 100644
+--- a/cparser/Cutil.ml
++++ b/cparser/Cutil.ml
+@@ -29,7 +29,7 @@ let no_loc = ("", -1)
+
+ module Ident = struct
+ type t = ident
+- let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp
++ let compare id1 id2 = compare id1.stamp id2.stamp
+ end
+
+ module IdentSet = Set.Make(Ident)
+diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
+index bbfcf311..9a24041b 100644
+--- a/debug/DwarfPrinter.ml
++++ b/debug/DwarfPrinter.ml
+@@ -268,7 +268,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
+ (* Print the debug_abbrev section using the previous computed abbreviations*)
+ let print_abbrev oc =
+ let abbrevs = Hashtbl.fold (fun s i acc -> (s,i)::acc) abbrev_mapping [] in
+- let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) abbrevs in
++ let abbrevs = List.sort (fun (_,a) (_,b) -> compare a b) abbrevs in
+ section oc Section_debug_abbrev;
+ print_label oc !abbrev_start_addr;
+ List.iter (fun (s,id) ->
+@@ -685,7 +685,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
+ print_label oc line_start;
+ list_opt s (fun () ->
+ section oc Section_debug_str;
+- let s = List.sort (fun (a,_) (b,_) -> Pervasives.compare a b) s in
++ let s = List.sort (fun (a,_) (b,_) -> compare a b) s in
+ List.iter (fun (id,s) ->
+ print_label oc (loc_to_label id);
+ fprintf oc " .asciz %S\n" s) s)
+diff --git a/driver/Interp.ml b/driver/Interp.ml
+index 6760e76c..a6841460 100644
+--- a/driver/Interp.ml
++++ b/driver/Interp.ml
+@@ -15,7 +15,7 @@
+ open Format
+ open Camlcoq
+ open AST
+-open Integers
++open !Integers
+ open Values
+ open Memory
+ open Globalenvs
+@@ -145,7 +145,7 @@ let print_state p (prog, ge, s) =
+ let compare_mem m1 m2 =
+ (* assumes nextblocks were already compared equal *)
+ (* should permissions be taken into account? *)
+- Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents
++ compare m1.Mem.mem_contents m2.Mem.mem_contents
+
+ (* Comparing continuations *)
+
diff --git a/non-free/compcert/APKBUILD b/non-free/compcert/APKBUILD
index 13faf6a3b0..1063590884 100644
--- a/non-free/compcert/APKBUILD
+++ b/non-free/compcert/APKBUILD
@@ -3,7 +3,7 @@
pkgname=compcert
_pkgname=CompCert
pkgver=3.5
-pkgrel=0
+pkgrel=1
pkgdesc="The verified C compiler"
url="https://compcert.inria.fr"
arch="armhf armv7 riscv64 x86_64"
@@ -12,6 +12,8 @@ depends="gcc"
makedepends="ocaml ocaml-compiler-libs ocaml-menhir-dev coq"
subpackages="$pkgname-doc"
source="https://compcert.inria.fr/release/$pkgname-$pkgver.tgz
+ 96383f6dbccd4b280acad395b9a2683a645a9de3.patch
+ coq-8.9.1-support.patch
fix-cprepro-options.patch
"
builddir="$srcdir/$_pkgname-$pkgver"
@@ -50,4 +52,6 @@ package() {
}
sha512sums="9c72aac0c72e7b9db68e34f469dbd02e4c7d88c54d8b001891e05ae5c5a1e4323be25bab7d53334943fec26e2b64d3a21972d38a589fc79cc8d4bf0185cec50b compcert-3.5.tgz
+dd85f75ce12b00515884eec9fb82835578717fb963659d6afe1ff7e87f4be67687c6fdeb787ad9c60707050eeea2a811a3c142aa1601b9096aeedc416deda498 96383f6dbccd4b280acad395b9a2683a645a9de3.patch
+53a35d10ff1e4c3b00015a7e19db30b7722d782c9f715dc5f69ae49a394eabb12b97c20356da48c9bd1f02659f86b7519ce236ace4390649bfa2d57786d80e35 coq-8.9.1-support.patch
5bdafee9e97c81505853ee2c5263067f98fce937af9c5eac79f51b0998ab9694811761ab5a131cac27109b3e8c84d9cbe293f11b66afce6e4910d452ce648de8 fix-cprepro-options.patch"
diff --git a/non-free/compcert/coq-8.9.1-support.patch b/non-free/compcert/coq-8.9.1-support.patch
new file mode 100644
index 0000000000..1f3362c471
--- /dev/null
+++ b/non-free/compcert/coq-8.9.1-support.patch
@@ -0,0 +1,26 @@
+diff -urN a/configure b/configure
+--- a/configure 2019-02-28 13:10:23.000000000 +0000
++++ b/configure 2019-09-02 11:48:06.703606027 +0000
+@@ -503,19 +503,19 @@
+ echo "Testing Coq... " | tr -d '\n'
+ coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
+ case "$coq_ver" in
+- 8.6.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0)
++ 8.6.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1)
+ echo "version $coq_ver -- good!";;
+ ?*)
+ echo "version $coq_ver -- UNSUPPORTED"
+ if $ignore_coq_version; then
+ echo "Warning: this version of Coq is unsupported, proceed at your own risks."
+ else
+- echo "Error: CompCert requires one of the following Coq versions: 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1"
++ echo "Error: CompCert requires one of the following Coq versions: 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1"
+ missingtools=true
+ fi;;
+ "")
+ echo "NOT FOUND"
+- echo "Error: make sure Coq version 8.9.0 is installed."
++ echo "Error: make sure Coq version 8.9.1 is installed."
+ missingtools=true;;
+ esac
+
--
2.23.0