Add non free compcert.

Julien LepillerTue May 02 14:01:35+0200 2017

8f3024d

Add non free compcert.

README.md

4444 
* _antlr3_: A parser generator
4545 
* _josm_: An openstreetmap editor
4646 
47+
Non-free
48+
--------
49+
50+
* _compcert_: A certified C compiler
51+
4752 
Current work
4853 
============
4954 
more/packages/ocaml.scm
11331133 
assistant to write formal mathematical proofs using a variety of theorem
11341134 
provers.")
11351135 
    (license license:gpl2+)))
1136+
1137+
(define-public compcert
1138+
  (package
1139+
    (name "compcert")
1140+
    (version "3.0")
1141+
    (source (origin
1142+
              (method url-fetch)
1143+
              (uri (string-append "http://compcert.inria.fr/release/compcert-"
1144+
                                  version ".tgz"))
1145+
              (sha256
1146+
               (base32
1147+
                "03fxf01acvy0akzb1czk33jsfmv2rka0m0jc1a2gmzs9i192rr7m"))))
1148+
    (build-system gnu-build-system)
1149+
    (arguments
1150+
     `(#:phases
1151+
       (modify-phases %standard-phases
1152+
         (replace 'configure
1153+
           (lambda* (#:key outputs #:allow-other-keys)
1154+
             (zero? (system* "./configure" "x86_64-linux" "-prefix"
1155+
                             (assoc-ref outputs "out"))))))
1156+
       #:tests? #f))
1157+
    (native-inputs
1158+
     `(("ocaml" ,ocaml)
1159+
       ("coq" ,coq)))
1160+
    (inputs
1161+
     `(("menhir" ,ocaml-menhir)))
1162+
    (home-page "http://compcert.inria.fr")
1163+
    (synopsis "Certified C compiler")
1164+
    (description "CompCert is a certified (with coq) C compiler.  Warning: this
1165+
package is not free software!")
1166+
    ;; actually the "INRIA Non-Commercial License Agreement"
1167+
    ;; a non-free license.
1168+
    (license (license:non-copyleft "file:///LICENSE"))))