mirror of
https://git.in.rschanz.org/ryan77627/guix.git
synced 2024-12-24 21:38:07 -05:00
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.
This commit is contained in:
parent
912f0541a3
commit
33af92dd99
2 changed files with 454 additions and 417 deletions
454
gnu/packages/coq.scm
Normal file
454
gnu/packages/coq.scm
Normal file
|
@ -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)))
|
|
@ -636,144 +636,6 @@ (define-public ocaml-num
|
|||
the OCaml core distribution.")
|
||||
(license license:lgpl2.1+))); with linking exception
|
||||
|
||||
(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 emacs-tuareg
|
||||
(package
|
||||
(name "emacs-tuareg")
|
||||
|
@ -4715,285 +4577,6 @@ (define-public ocaml-tsdl
|
|||
cross-platform SDL C library.")
|
||||
(license license:isc)))
|
||||
|
||||
(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)))
|
||||
|
||||
(define-public dedukti
|
||||
(package
|
||||
(name "dedukti")
|
||||
|
|
Loading…
Reference in a new issue