diff options
| author | Julien Lepiller <julien@lepiller.eu> | 2017-06-21 21:41:36 +0200 |
|---|---|---|
| committer | Julien Lepiller <julien@lepiller.eu> | 2017-07-29 15:19:07 +0200 |
| commit | 303690c405446d1eea231044f0bcb48b88b6508d (patch) | |
| tree | ed3fa98a9a76f2402ff209512fc375d17bf0cf64 /gnu/packages | |
| parent | b09c4244f7c77b11e039cd5348270b2d1da77577 (diff) | |
gnu: Add coq-interval.
* gnu/packages/ocaml.scm (coq-interval): New variable.
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/ocaml.scm | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 86af187aa0..43bbdcd6e2 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3345,3 +3345,49 @@ 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-interval + (package + (name "coq-interval") + (version "3.2.0") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/" + "file/36538/interval-" version ".tar.gz")) + (sha256 + (base32 + "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (propagated-inputs + `(("flocq" ,coq-flocq) + ("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))) |