Non-free

--------

* _compcert_: A certified C compiler

(define-public ppsimpl

  (package

    (name "ppsimpl")

    (version "8.7")

    (source (origin

              (method git-fetch)

              (uri (git-reference

                     (url "https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git")

                     (commit "86255a47568df58767d1d8e0b9e2da31cf73a5fc")))

              (file-name (string-append name "-" version))

              (sha256

               (base32

                "0h509w43j2wd2pyx04k3xfd0bsbmqscwqvhf8whzc3cxzl4j6vvq"))))

              ;(uri "https://gforge.inria.fr/frs/download.php/file/37615/ppsimpl-09-07-2018.tar.gz")

              ;(sha256

              ; (base32

              ;  "010zgskc1wd5v6wmmyxaapvwxjlgbdqqiks2dvf6llx03b07ak59"))))

    (build-system gnu-build-system)

    (arguments

     `(#:test-target "test"

       #:configure-flags

       (list "-R" (string-append (assoc-ref %build-inputs "compcert") "/lib/coq/user-contrib/compcert") "compcert")

       #:make-flags (list "COQC=coqc -R src PP -I src"

                          (string-append

                            "COQLIBINSTALL="

                            (assoc-ref %outputs "out")

                            "/lib/coq/user-contrib"))))

    (inputs

     `(("coq-bignums-8.7" ,coq-bignums-8.7)

       ("compcert" ,compcert)))

    (native-inputs

     `(("coq-8.7" ,coq-8.7)

       ("ocaml" ,ocaml)

       ("ocaml-findlib" ,ocaml-findlib)

       ("camlp4" ,camlp4)

       ("camlp5" ,camlp5)

       ("which" ,which)))

    (home-page "")

    (synopsis "")

    (description "")

    ;; No declared license -> all rights reserved

    (license #f)))

(define-public compcert

  (package

    (name "compcert")

    (version "3.5")

    (source (origin

              (method url-fetch)

              (uri (string-append "http://compcert.inria.fr/release/compcert-"

                                  version ".tgz"))

              (sha256

               (base32

                "02dmd4iw6b5i38svaycjsywlpmg0kaypc01vxi6ndyywx6giz80y"))))

    (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 "CompCert is a certified (with coq) C compiler.  Warning: this

package is not free software!")

    ;; actually the "INRIA Non-Commercial License Agreement"

    ;; a non-free license.

    (license (license:non-copyleft "file:///LICENSE"))))