From 1892d626dd36d6b6d8553d03050afc7022e86c73 Mon Sep 17 00:00:00 2001
From: Timotej Lazar <timotej.lazar@araneo.si>
Date: Sat, 11 Apr 2020 13:16:59 +0200
Subject: [PATCH 1/2] nongnu: compcert: Fix a non-exhaustive match.

* nongnu/packages/coq.scm (compcert)[arguments]: Add default case to match so
that it can be evaluated on all systems.
[supported-systems]: Remove unsupported mips64el-linux.
---
 nongnu/packages/coq.scm | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/nongnu/packages/coq.scm b/nongnu/packages/coq.scm
index e564dc0..de067ab 100644
--- a/nongnu/packages/coq.scm
+++ b/nongnu/packages/coq.scm
@@ -43,9 +43,9 @@
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
              (let ((system ,(match (or (%current-target-system) (%current-system))
-                              ("x86_64-linux" "x86_64-linux")
+                              ("armhf-linux" "arm-linux")
                               ("i686-linux" "x86_32-linux")
-                              ("armhf-linux" "arm-linux"))))
+                              (s s))))
                (format #t "Building for ~a~%" system)
                (invoke "./configure" system "-prefix"
                        (assoc-ref outputs "out")))
@@ -62,6 +62,8 @@
                (find-files "." ".*.vo$"))
              #t)))
        #:tests? #f))
+    ;; MIPS is not supported.
+    (supported-systems (delete "mips64el-linux" %supported-systems))
     (native-inputs
      `(("ocaml" ,ocaml)
        ("ocaml-findlib" ,ocaml-findlib); for menhir --suggest-menhirlib

From 1b7a4319fa6b3f959cc925a6d713f0c111fb7c8f Mon Sep 17 00:00:00 2001
From: Timotej Lazar <timotej.lazar@araneo.si>
Date: Sat, 11 Apr 2020 20:18:39 +0200
Subject: [PATCH 2/2] nongnu: compcert: Build for arm-eabihf on arm.

* nongnu/packages/coq.scm (compcert)[arguments]: Pass arm-eabihf to configure
script to enable hard float extensions.
---
 nongnu/packages/coq.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nongnu/packages/coq.scm b/nongnu/packages/coq.scm
index de067ab..7558cd1 100644
--- a/nongnu/packages/coq.scm
+++ b/nongnu/packages/coq.scm
@@ -43,7 +43,7 @@
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
              (let ((system ,(match (or (%current-target-system) (%current-system))
-                              ("armhf-linux" "arm-linux")
+                              ("armhf-linux" "arm-eabihf")
                               ("i686-linux" "x86_32-linux")
                               (s s))))
                (format #t "Building for ~a~%" system)