From 048de09ad8029b0ca31dfc59e600b691f5bd5c94 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Sat, 4 Apr 2020 18:53:30 +0200
Subject: [PATCH] nongnu: Add compcert.

* nongnu/packages/coq.scm: New file.
---
 nongnu/packages/coq.scm | 86 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 nongnu/packages/coq.scm

diff --git a/nongnu/packages/coq.scm b/nongnu/packages/coq.scm
new file mode 100644
index 0000000..e564dc0
--- /dev/null
+++ b/nongnu/packages/coq.scm
@@ -0,0 +1,86 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2020 Julien Lepiller <julien@lepiller.eu>
+;;;
+;;; This file is not part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (nongnu packages coq)
+  #:use-module (ice-9 match)
+  #:use-module (guix packages)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix download)
+  #:use-module (gnu packages coq)
+  #:use-module (gnu packages ocaml)
+  #:use-module (nonguix licenses))
+
+(define-public compcert
+  (package
+    (name "compcert")
+    (version "3.7")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://compcert.inria.fr/release/compcert-"
+                                  version ".tgz"))
+              (sha256
+               (base32
+                "1c3yp3ns830vg3q8b0y61xffd1fgkmkg585pdsv6qmy2sqp1pvnf"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((system ,(match (or (%current-target-system) (%current-system))
+                              ("x86_64-linux" "x86_64-linux")
+                              ("i686-linux" "x86_32-linux")
+                              ("armhf-linux" "arm-linux"))))
+               (format #t "Building for ~a~%" system)
+               (invoke "./configure" system "-prefix"
+                       (assoc-ref outputs "out")))
+             #t))
+         (add-after 'install 'install-lib
+           (lambda* (#:key outputs #:allow-other-keys)
+             (for-each
+               (lambda (file)
+                 (install-file
+                   file
+                   (string-append
+                     (assoc-ref outputs "out")
+                     "/lib/coq/user-contrib/compcert/" (dirname file))))
+               (find-files "." ".*.vo$"))
+             #t)))
+       #:tests? #f))
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("ocaml-findlib" ,ocaml-findlib); for menhir --suggest-menhirlib
+       ("coq" ,coq)))
+    (inputs
+     `(("menhir" ,ocaml-menhir)))
+    (home-page "http://compcert.inria.fr")
+    (synopsis "Certified C compiler")
+    (description "The CompCert project investigates the formal verification of
+realistic compilers usable for critical embedded software.  Such verified
+compilers come with a mathematical, machine-checked proof that the generated
+executable code behaves exactly as prescribed by the semantics of the source
+program. By ruling out the possibility of compiler-introduced bugs, verified
+compilers strengthen the guarantees that can be obtained by applying formal
+methods to source programs.
+
+The main result of the project is the CompCert C verified compiler, a
+high-assurance compiler for almost all of the C language (ISO C99), generating
+efficient code for the PowerPC, ARM, RISC-V and x86 processors.")
+    ;; actually the "INRIA Non-Commercial License Agreement"
+    ;; a non-free license.
+    (license (nonfree "file:///LICENSE"))))