diff options
author | Alex Griffin <a@ajgrf.com> | 2020-04-07 16:42:17 +0000 |
---|---|---|
committer | Alex Griffin <a@ajgrf.com> | 2020-04-07 16:42:17 +0000 |
commit | a66e21377de9131ef5d261c4754010e7206679ab (patch) | |
tree | d90e7639f0c08a998300747283b34e669e6704b8 /nongnu | |
parent | 2a939c8d8b813d9941649691dddfcda3a751ca0d (diff) | |
parent | 048de09ad8029b0ca31dfc59e600b691f5bd5c94 (diff) |
Merge branch 'compcert' into 'master'
nongnu: Add compcert.
See merge request nonguix/nonguix!21
Diffstat (limited to 'nongnu')
-rw-r--r-- | nongnu/packages/coq.scm | 86 |
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")))) |