Subject: [PATCH 6 of 6] non-free/compcert: fix build with ocaml-4.08+ and coq-8.9.1

From: alpine-mips-patches <[email-masked]>
Date: Thu, 7 Nov 2019 12:11:30 +0000

---
 ...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 <[email-masked]>
+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