alpine-mips-patches: 1 non-free/compcert: fix build with ocaml-4.08+ and coq-8.9.1 3 files changed, 194 insertions(+), 1 deletions(-)
Copy & paste the following snippet into your terminal to import this patchset into git:
curl -s https://lists.alpinelinux.org/~alpine/aports/patches/3125/mbox | git am -3Learn more about email & git
--- ...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