diff options
Diffstat (limited to 'gnu/packages/ocaml.scm')
| -rw-r--r-- | gnu/packages/ocaml.scm | 417 |
1 files changed, 0 insertions, 417 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 8fe8ac86f0..b71adf116f 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -636,144 +636,6 @@ arbitrary-precision integer and rational arithmetic that used to be part of 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 @@ OCaml projects that contain C stubs.") 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") |