summaryrefslogtreecommitdiff
path: root/nongnu/packages/coq.scm
diff options
context:
space:
mode:
authorJulien Lepiller <julien@lepiller.eu>2020-04-04 18:53:30 +0200
committerJulien Lepiller <julien@lepiller.eu>2020-04-04 18:54:06 +0200
commit048de09ad8029b0ca31dfc59e600b691f5bd5c94 (patch)
treec8ab8755c178e73cae7677b8543cd869c5a4bfe7 /nongnu/packages/coq.scm
parent8d2c3b5bb38ec98420f7dd6518850cde8cf50e2f (diff)
nongnu: Add compcert.
* nongnu/packages/coq.scm: New file.
Diffstat (limited to 'nongnu/packages/coq.scm')
-rw-r--r--nongnu/packages/coq.scm86
1 files changed, 86 insertions, 0 deletions
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"))))