89b524ab58
This patch moves Guile modules shipped as a Guix channel under the modules directory. The rationale behind this is that we are probably adding unwanted files into Guile's load path, such as the news file and possible scripts that could be added to the channel repository in the future. * guix-channel (channel): Set directory field. * nongnu/*: Move under modules/nongnu. * nonguix/*: Move under modules/nonguix.
78 lines
3.1 KiB
Scheme
78 lines
3.1 KiB
Scheme
;;; SPDX-License-Identifier: GPL-3.0-or-later
|
|
;;; Copyright © 2020 Julien Lepiller <julien@lepiller.eu>
|
|
;;; Copyright © 2021 Isaac Young <isyoung@pm.me>
|
|
;;; Copyright © 2022 Jonathan Brielmaier <jonathan.brielmaier@web.de>
|
|
|
|
(define-module (nongnu packages coq)
|
|
#:use-module (ice-9 match)
|
|
#:use-module (guix packages)
|
|
#:use-module (guix build-system gnu)
|
|
#:use-module (guix git-download)
|
|
#:use-module (gnu packages coq)
|
|
#:use-module (gnu packages ocaml)
|
|
#:use-module (nonguix licenses))
|
|
|
|
(define-public compcert
|
|
(package
|
|
(name "compcert")
|
|
(version "3.14")
|
|
(source (origin
|
|
(method git-fetch)
|
|
(uri (git-reference
|
|
(url "https://github.com/AbsInt/compcert")
|
|
(commit (string-append "v" version))))
|
|
(file-name (git-file-name name version))
|
|
(sha256
|
|
(base32
|
|
"030fsg0qr9aasmwk0ahp78sw8rbjmf6pl1w9ws5ghs61kyk4qwj1"))))
|
|
(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))
|
|
("armhf-linux" "arm-eabihf")
|
|
("i686-linux" "x86_32-linux")
|
|
(s s))))
|
|
(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))
|
|
;; MIPS is not supported.
|
|
(supported-systems (delete "mips64el-linux" %supported-systems))
|
|
(native-inputs
|
|
(list coq
|
|
ocaml
|
|
ocaml-findlib)) ; for menhir --suggest-menhirlib
|
|
(inputs
|
|
(list 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"))))
|