gnu: Move coq packages from ocaml to coq.

* gnu/packages/ocaml.scm (coq, proof-general, coq-flocq, coq-gappa, coq-mathcomp)
(coq-coquelicot, coq-bignums, coq-interval): Move from here...
* gnu/packages/coq.scm: ... to here.  New file.

1 files changed, 454 insertions, 0 deletions

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
new file mode 100644
index 0000000000..3a898814c3
--- /dev/null
+++ b/gnu/packages/coq.scm
@@ -0,0 +1,454 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;;
+;;; This file is 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 (gnu packages coq)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages base)
+  #:use-module (gnu packages bison)
+  #:use-module (gnu packages boost)
+  #:use-module (gnu packages emacs)
+  #:use-module (gnu packages flex)
+  #:use-module (gnu packages multiprecision)
+  #:use-module (gnu packages ocaml)
+  #:use-module (gnu packages perl)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages texinfo)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
+  #:use-module (guix download)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix packages)
+  #:use-module (guix utils)
+  #:use-module ((srfi srfi-1) #:hide (zip)))
+
+(define-public coq
+  (package
+    (name "coq")
+    (version "8.8.2")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/coq/coq/archive/V"
+                                  version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r"))))
+    (native-search-paths
+     (list (search-path-specification
+            (variable "COQPATH")
+            (files (list "lib/coq/user-contrib")))))
+    (build-system ocaml-build-system)
+    (inputs
+     `(("lablgtk" ,lablgtk)
+       ("python" ,python-2)
+       ("camlp5" ,camlp5)
+       ("ocaml-num" ,ocaml-num)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out"))
+                    (mandir (string-append out "/share/man"))
+                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
+               (invoke "./configure"
+                       "-prefix" out
+                       "-mandir" mandir
+                       "-browser" browser
+                       "-coqide" "opt"))))
+         (replace 'build
+           (lambda _
+             (invoke "make"
+                     "-j" (number->string (parallel-job-count))
+                     "world")))
+         (delete 'check)
+         (add-after 'install 'check
+           (lambda _
+             (with-directory-excursion "test-suite"
+               ;; These two tests fail.
+               ;; This one fails because the output is not formatted as expected.
+               (delete-file-recursively "coq-makefile/timing")
+               ;; This one fails because we didn't build coqtop.byte.
+               (delete-file-recursively "coq-makefile/findlib-package")
+               (invoke "make")))))))
+    (home-page "https://coq.inria.fr")
+    (synopsis "Proof assistant for higher-order logic")
+    (description
+     "Coq is a proof assistant for higher-order logic, which allows the
+development of computer programs consistent with their formal specification.
+It is developed using Objective Caml and Camlp5.")
+    ;; The code is distributed under lgpl2.1.
+    ;; Some of the documentation is distributed under opl1.0+.
+    (license (list license:lgpl2.1 license:opl1.0+))))
+
+(define-public proof-general
+  (package
+    (name "proof-general")
+    (version "4.2")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "http://proofgeneral.inf.ed.ac.uk/releases/"
+                    "ProofGeneral-" version ".tgz"))
+              (sha256
+               (base32
+                "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("which" ,which)
+       ("emacs" ,emacs-minimal)
+       ("texinfo" ,texinfo)))
+    (inputs
+     `(("host-emacs" ,emacs)
+       ("perl" ,perl)
+       ("coq" ,coq)))
+    (arguments
+     `(#:tests? #f  ; no check target
+       #:make-flags (list (string-append "PREFIX=" %output)
+                          (string-append "DEST_PREFIX=" %output))
+       #:modules ((guix build gnu-build-system)
+                  (guix build utils)
+                  (guix build emacs-utils))
+       #:imported-modules (,@%gnu-build-system-modules
+                           (guix build emacs-utils))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure)
+         (add-after 'unpack 'disable-byte-compile-error-on-warn
+                    (lambda _
+                      (substitute* "Makefile"
+                        (("\\(setq byte-compile-error-on-warn t\\)")
+                         "(setq byte-compile-error-on-warn nil)"))
+                      #t))
+         (add-after 'unpack 'patch-hardcoded-paths
+                    (lambda* (#:key inputs outputs #:allow-other-keys)
+                      (let ((out   (assoc-ref outputs "out"))
+                            (coq   (assoc-ref inputs "coq"))
+                            (emacs (assoc-ref inputs "host-emacs")))
+                        (define (coq-prog name)
+                          (string-append coq "/bin/" name))
+                        (emacs-substitute-variables "coq/coq.el"
+                          ("coq-prog-name"           (coq-prog "coqtop"))
+                          ("coq-compiler"            (coq-prog "coqc"))
+                          ("coq-dependency-analyzer" (coq-prog "coqdep")))
+                        (substitute* "Makefile"
+                          (("/sbin/install-info") "install-info"))
+                        (substitute* "bin/proofgeneral"
+                          (("^PGHOMEDEFAULT=.*" all)
+                           (string-append all
+                                          "PGHOME=$PGHOMEDEFAULT\n"
+                                          "EMACS=" emacs "/bin/emacs")))
+                        #t)))
+         (add-after 'unpack 'clean
+                    (lambda _
+                      ;; Delete the pre-compiled elc files for Emacs 23.
+                      (zero? (system* "make" "clean"))))
+         (add-after 'install 'install-doc
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      ;; XXX FIXME avoid building/installing pdf files,
+                      ;; due to unresolved errors building them.
+                      (substitute* "Makefile"
+                        ((" [^ ]*\\.pdf") ""))
+                      (zero? (apply system* "make" "install-doc"
+                                    make-flags)))))))
+    (home-page "http://proofgeneral.inf.ed.ac.uk/")
+    (synopsis "Generic front-end for proof assistants based on Emacs")
+    (description
+     "Proof General is a major mode to turn Emacs into an interactive proof
+assistant to write formal mathematical proofs using a variety of theorem
+provers.")
+    (license license:gpl2+)))
+
+(define-public coq-flocq
+  (package
+    (name "coq-flocq")
+    (version "2.6.1")
+    (source (origin
+              (method url-fetch)
+              ;; Use the ‘Latest version’ link for a stable URI across releases.
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+                                  "file/37454/flocq-" version ".tar.gz"))
+              (sha256
+               (base32
+                "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)
+       ("coq" ,coq)))
+    (arguments
+     `(#:configure-flags
+       (list (string-append "--libdir=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib/Flocq"))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-remake
+           (lambda _
+             (substitute* "remake.cpp"
+               (("/bin/sh") (which "sh")))
+             #t))
+         (replace 'build
+           (lambda _
+             (invoke "./remake")
+             #t))
+         (replace 'check
+           (lambda _
+             (invoke "./remake" "check")
+             #t))
+             ;; TODO: requires coq-gappa and coq-interval.
+             ;(invoke "./remake" "check-more")
+         (replace 'install
+           (lambda _
+             (invoke "./remake" "install")
+             #t)))))
+    (home-page "http://flocq.gforge.inria.fr/")
+    (synopsis "Floating-point formalization for the Coq system")
+    (description "Flocq (Floats for Coq) is a floating-point formalization for
+the Coq system.  It provides a comprehensive library of theorems on a multi-radix
+multi-precision arithmetic.  It also supports efficient numerical computations
+inside Coq.")
+    (license license:lgpl3+)))
+
+(define-public coq-gappa
+  (package
+    (name "coq-gappa")
+    (version "1.3.2")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-"
+                                  version ".tar.gz"))
+              (sha256
+               (base32
+                "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)
+       ("coq" ,coq)
+       ("bison" ,bison)
+       ("flex" ,flex)))
+    (inputs
+     `(("gmp" ,gmp)
+       ("mpfr" ,mpfr)
+       ("boost" ,boost)))
+    (arguments
+     `(#:configure-flags
+       (list (string-append "--libdir=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib/Gappa"))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-remake
+           (lambda _
+             (substitute* "remake.cpp"
+               (("/bin/sh") (which "sh")))))
+         (replace 'build
+           (lambda _
+             (zero? (system* "./remake"))))
+         (replace 'check
+           (lambda _
+             (zero? (system* "./remake" "check"))))
+         (replace 'install
+           (lambda _
+             (zero? (system* "./remake" "install")))))))
+    (home-page "http://gappa.gforge.inria.fr/")
+    (synopsis "Verify and formally prove properties on numerical programs")
+    (description "Gappa is a tool intended to help verifying and formally proving
+properties on numerical programs dealing with floating-point or fixed-point
+arithmetic.  It has been used to write robust floating-point filters for CGAL
+and it is used to certify elementary functions in CRlibm.  While Gappa is
+intended to be used directly, it can also act as a backend prover for the Why3
+software verification plateform or as an automatic tactic for the Coq proof
+assistant.")
+    (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
+
+(define-public coq-mathcomp
+  (package
+    (name "coq-mathcomp")
+    (version "1.7.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
+                                  version ".tar.gz"))
+              (sha256
+               (base32
+                "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)
+       ("coq" ,coq)))
+    (arguments
+     `(#:tests? #f; No need to test formally-verified programs :)
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure)
+         (add-before 'build 'chdir
+           (lambda _
+             (chdir "mathcomp")))
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
+             (zero? (system* "make" "-f" "Makefile.coq"
+                             (string-append "COQLIB=" (assoc-ref outputs "out")
+                                            "/lib/coq/")
+                             "install")))))))
+    (home-page "https://math-comp.github.io/math-comp/")
+    (synopsis "Mathematical Components for Coq")
+    (description "Mathematical Components for Coq has its origins in the formal
+proof of the Four Colour Theorem.  Since then it has grown to cover many areas
+of mathematics and has been used for large scale projects like the formal proof
+of the Odd Order Theorem.
+
+The library is written using the Ssreflect proof language that is an integral
+part of the distribution.")
+    (license license:cecill-b)))
+
+(define-public coq-coquelicot
+  (package
+    (name "coq-coquelicot")
+    (version "3.0.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+                                  "file/37045/coquelicot-" version ".tar.gz"))
+              (sha256
+               (base32
+                "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)
+       ("coq" ,coq)))
+    (propagated-inputs
+     `(("mathcomp" ,coq-mathcomp)))
+    (arguments
+     `(#:configure-flags
+       (list (string-append "--libdir=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib/Coquelicot"))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-coq8.8
+           (lambda _
+             ; appcontext has been removed from coq 8.8
+             (substitute* "theories/AutoDerive.v"
+               (("appcontext") "context"))
+             #t))
+         (add-before 'configure 'fix-remake
+           (lambda _
+             (substitute* "remake.cpp"
+               (("/bin/sh") (which "sh")))))
+         (replace 'build
+           (lambda _
+             (zero? (system* "./remake"))))
+         (replace 'check
+           (lambda _
+             (zero? (system* "./remake" "check"))))
+         (replace 'install
+           (lambda _
+             (zero? (system* "./remake" "install")))))))
+    (home-page "http://coquelicot.saclay.inria.fr/index.html")
+    (synopsis "Coq library for Reals")
+    (description "Coquelicot is an easier way of writing formulas and theorem
+statements, achieved by relying on total functions in place of dependent types
+for limits, derivatives, integrals, power series, and so on.  To help with the
+proof process, the library comes with a comprehensive set of theorems that cover
+not only these notions, but also some extensions such as parametric integrals,
+two-dimensional differentiability, asymptotic behaviors.  It also offers some
+automations for performing differentiability proofs.  Moreover, Coquelicot is a
+conservative extension of Coq's standard library and provides correspondence
+theorems between the two libraries.")
+    (license license:lgpl3+)))
+
+(define-public coq-bignums
+  (package
+    (name "coq-bignums")
+    (version "8.8.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/coq/bignums/archive/V"
+                                  version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("coq" ,coq)))
+    (inputs
+     `(("camlp5" ,camlp5)))
+    (arguments
+     `(#:tests? #f; No test target
+       #:make-flags
+       (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib"))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))
+    (home-page "https://github.com/coq/bignums")
+    (synopsis "Coq library for arbitrary large numbers")
+    (description "Bignums is a coq library of arbitrary large numbers.  It
+provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
+    (license license:lgpl2.1+)))
+
+(define-public coq-interval
+  (package
+    (name "coq-interval")
+    (version "3.3.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+                                  "file/37077/interval-" version ".tar.gz"))
+              (sha256
+               (base32
+                "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,which)
+       ("coq" ,coq)))
+    (propagated-inputs
+     `(("flocq" ,coq-flocq)
+       ("bignums" ,coq-bignums)
+       ("coquelicot" ,coq-coquelicot)
+       ("mathcomp" ,coq-mathcomp)))
+    (arguments
+     `(#:configure-flags
+       (list (string-append "--libdir=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib/Gappa"))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-remake
+           (lambda _
+             (substitute* "remake.cpp"
+               (("/bin/sh") (which "sh")))))
+         (replace 'build
+           (lambda _
+             (zero? (system* "./remake"))))
+         (replace 'check
+           (lambda _
+             (zero? (system* "./remake" "check"))))
+         (replace 'install
+           (lambda _
+             (zero? (system* "./remake" "install")))))))
+    (home-page "http://coq-interval.gforge.inria.fr/")
+    (synopsis "Coq tactics to simplify inequality proofs")
+    (description "Interval provides vernacular files containing tactics for
+simplifying the proofs of inequalities on expressions of real numbers for the
+Coq proof assistant.")
+    (license license:cecill-c)))