[PATCH] Opam importer improvements

DoneSubmitted by Julien Lepiller.
Details
2 participants
  • Julien Lepiller
  • Ricardo Wurmus
Owner
unassigned
Severity
normal
J
J
Julien Lepiller wrote on 20 Dec 2018 11:41
(address . guix-patches@gnu.org)
e7e2404c6d4033d3988b7e7ef28882e4@lepiller.eu
Hi,
here are a few improvements to the opam importer. The first patch is somewhat unrelated and moves coq and coq packages away from ocaml.scm to a new coq.scm file. The second and third patches add a recursive option and an updater for opam, while the fourth and fith patches make sure it works for ocaml-graph: I found that the importer didn't support comments that are present in the opam file for ocamlgraph.
J
J
Julien Lepiller wrote on 20 Dec 2018 12:00
[PATCH 1/5] gnu: Move coq packages from ocaml to coq.
(address . 33811@debbugs.gnu.org)(name . Julien Lepiller)(address . julien@lepiller.eu)
20181220110103.4219-1-julien@lepiller.eu
* 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.--- gnu/packages/coq.scm | 454 +++++++++++++++++++++++++++++++++++++++++ gnu/packages/ocaml.scm | 417 ------------------------------------- 2 files changed, 454 insertions(+), 417 deletions(-) create mode 100644 gnu/packages/coq.scm
Toggle diff (894 lines)diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scmnew file mode 100644index 000000000..3a898814c--- /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)))diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scmindex 3b1ddcb5b..503e42297 100644--- a/gnu/packages/ocaml.scm+++ b/gnu/packages/ocaml.scm@@ -632,144 +632,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")@@ -4710,282 +4572,3 @@ OCaml projects that contain C stubs.") (description "Tsdl is an OCaml library providing thin bindings to the 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)))-- 2.19.2
J
J
Julien Lepiller wrote on 20 Dec 2018 12:01
[PATCH 2/5] import: opam: Add recursive option.
(address . 33811@debbugs.gnu.org)(name . Julien Lepiller)(address . julien@lepiller.eu)
20181220110103.4219-2-julien@lepiller.eu
* guix/script/import/opam.scm: Add recursive option.* guix/import/opam.scm (opam->guix-package): return two values.(opam-recursive-import): New variable.--- guix/import/opam.scm | 70 ++++++++++++++++++++++++------------ guix/scripts/import/opam.scm | 27 +++++++++++--- 2 files changed, 69 insertions(+), 28 deletions(-)
Toggle diff (168 lines)diff --git a/guix/import/opam.scm b/guix/import/opam.scmindex c42a5d767..cdf05e7d2 100644--- a/guix/import/opam.scm+++ b/guix/import/opam.scm@@ -33,7 +33,8 @@ #:use-module (guix utils) #:use-module (guix import utils) #:use-module ((guix licenses) #:prefix license:)- #:export (opam->guix-package))+ #:export (opam->guix-package+ opam-recursive-import)) ;; Define a PEG parser for the opam format (define-peg-pattern SP none (or " " "\n"))@@ -128,7 +129,6 @@ path to the repository." (else (string-append "ocaml-" name)))) (define (metadata-ref file lookup)- (pk 'file file 'lookup lookup) (fold (lambda (record acc) (match record ((record key val)@@ -166,6 +166,21 @@ path to the repository." (('conditional-value val condition) (if (native? condition) (dependency->input val) "")))) +(define (dependency->name dependency)+ (match dependency+ (('string-pat str) str)+ (('conditional-value val condition)+ (dependency->name val))))++(define (dependency-list->names lst)+ (filter+ (lambda (name)+ (not (or+ (string-prefix? "conf-" name)+ (equal? name "ocaml")+ (equal? name "findlib"))))+ (map dependency->name lst)))+ (define (ocaml-names->guix-names names) (map ocaml-name->guix-name (remove (lambda (name)@@ -193,32 +208,41 @@ path to the repository." (define (opam->guix-package name) (and-let* ((repository (get-opam-repository)) (version (find-latest-version name repository))- (file (string-append repository "/packages/" name "/" name "." (pk 'version version) "/opam"))+ (file (string-append repository "/packages/" name "/" name "." version "/opam")) (opam-content (get-metadata file))- (url-dict (metadata-ref (pk 'metadata opam-content) "url"))+ (url-dict (metadata-ref opam-content "url")) (source-url (metadata-ref url-dict "src")) (requirements (metadata-ref opam-content "depends"))+ (dependencies (dependency-list->names requirements)) (inputs (dependency-list->inputs (depends->inputs requirements))) (native-inputs (dependency-list->inputs (depends->native-inputs requirements)))) (call-with-temporary-output-file (lambda (temp port) (and (url-fetch source-url temp)- `(package- (name ,(ocaml-name->guix-name name))- (version ,(metadata-ref opam-content "version"))- (source- (origin- (method url-fetch)- (uri ,source-url)- (sha256 (base32 ,(guix-hash-url temp)))))- (build-system ocaml-build-system)- ,@(if (null? inputs)- '()- `((inputs ,(list 'quasiquote inputs))))- ,@(if (null? native-inputs)- '()- `((native-inputs ,(list 'quasiquote native-inputs))))- (home-page ,(metadata-ref opam-content "homepage"))- (synopsis ,(metadata-ref opam-content "synopsis"))- (description ,(metadata-ref opam-content "description"))- (license #f)))))))+ (values+ `(package+ (name ,(ocaml-name->guix-name name))+ (version ,(metadata-ref opam-content "version"))+ (source+ (origin+ (method url-fetch)+ (uri ,source-url)+ (sha256 (base32 ,(guix-hash-url temp)))))+ (build-system ocaml-build-system)+ ,@(if (null? inputs)+ '()+ `((inputs ,(list 'quasiquote inputs))))+ ,@(if (null? native-inputs)+ '()+ `((native-inputs ,(list 'quasiquote native-inputs))))+ (home-page ,(metadata-ref opam-content "homepage"))+ (synopsis ,(metadata-ref opam-content "synopsis"))+ (description ,(metadata-ref opam-content "description"))+ (license #f))+ dependencies))))))++(define (opam-recursive-import package-name)+ (recursive-import package-name #f+ #:repo->guix-package (lambda (name repo)+ (opam->guix-package name))+ #:guix-name ocaml-name->guix-name))diff --git a/guix/scripts/import/opam.scm b/guix/scripts/import/opam.scmindex b54987874..2d249a213 100644--- a/guix/scripts/import/opam.scm+++ b/guix/scripts/import/opam.scm@@ -25,6 +25,7 @@ #:use-module (srfi srfi-1) #:use-module (srfi srfi-11) #:use-module (srfi srfi-37)+ #:use-module (srfi srfi-41) #:use-module (ice-9 match) #:use-module (ice-9 format) #:export (guix-import-opam))@@ -43,6 +44,8 @@ Import and convert the opam package for PACKAGE-NAME.\n")) (display (G_ " -h, --help display this help and exit")) (display (G_ "+ -r, --recursive import packages recursively"))+ (display (G_ " -V, --version display version information and exit")) (newline) (show-bug-report-information))@@ -56,6 +59,9 @@ Import and convert the opam package for PACKAGE-NAME.\n")) (option '(#\V "version") #f #f (lambda args (show-version-and-exit "guix import opam")))+ (option '(#\r "recursive") #f #f+ (lambda (opt name arg result)+ (alist-cons 'recursive #t result))) %standard-import-options)) @@ -81,11 +87,22 @@ Import and convert the opam package for PACKAGE-NAME.\n")) (reverse opts)))) (match args ((package-name)- (let ((sexp (opam->guix-package package-name)))- (unless sexp- (leave (G_ "failed to download meta-data for package '~a'~%")- package-name))- sexp))+ (if (assoc-ref opts 'recursive)+ ;; Recursive import+ (map (match-lambda+ ((and ('package ('name name) . rest) pkg)+ `(define-public ,(string->symbol name)+ ,pkg))+ (_ #f))+ (reverse+ (stream->list+ (opam-recursive-import package-name))))+ ;; Single import+ (let ((sexp (opam->guix-package package-name)))+ (unless sexp+ (leave (G_ "failed to download meta-data for package '~a'~%")+ package-name))+ sexp))) (() (leave (G_ "too few arguments~%"))) ((many ...)-- 2.19.2
J
J
Julien Lepiller wrote on 20 Dec 2018 12:01
[PATCH 3/5] import: opam: Add updater.
(address . 33811@debbugs.gnu.org)(name . Julien Lepiller)(address . julien@lepiller.eu)
20181220110103.4219-3-julien@lepiller.eu
* guix/import/opam.scm (%opam-updater): New variable.--- guix/import/opam.scm | 59 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 54 insertions(+), 5 deletions(-)
Toggle diff (99 lines)diff --git a/guix/import/opam.scm b/guix/import/opam.scmindex cdf05e7d2..b30d28561 100644--- a/guix/import/opam.scm+++ b/guix/import/opam.scm@@ -27,14 +27,19 @@ #:use-module (srfi srfi-1) #:use-module (srfi srfi-2) #:use-module (web uri)+ #:use-module (guix build-system)+ #:use-module (guix build-system ocaml) #:use-module (guix http-client) #:use-module (guix git) #:use-module (guix ui)+ #:use-module (guix packages)+ #:use-module (guix upstream) #:use-module (guix utils) #:use-module (guix import utils) #:use-module ((guix licenses) #:prefix license:) #:export (opam->guix-package- opam-recursive-import))+ opam-recursive-import+ %opam-updater)) ;; Define a PEG parser for the opam format (define-peg-pattern SP none (or " " "\n"))@@ -205,11 +210,17 @@ path to the repository." (list dependency (list 'unquote (string->symbol dependency)))) (ocaml-names->guix-names lst))) -(define (opam->guix-package name)+(define (opam-fetch name) (and-let* ((repository (get-opam-repository)) (version (find-latest-version name repository))- (file (string-append repository "/packages/" name "/" name "." version "/opam"))- (opam-content (get-metadata file))+ (file (string-append repository "/packages/" name "/" name "." version "/opam")))+ `(("metadata" ,@(get-metadata file))+ ("version" . ,version))))++(define (opam->guix-package name)+ (and-let* ((opam-file (opam-fetch name))+ (version (assoc-ref opam-file "version"))+ (opam-content (assoc-ref opam-file "metadata")) (url-dict (metadata-ref opam-content "url")) (source-url (metadata-ref url-dict "src")) (requirements (metadata-ref opam-content "depends"))@@ -222,7 +233,7 @@ path to the repository." (values `(package (name ,(ocaml-name->guix-name name))- (version ,(metadata-ref opam-content "version"))+ (version ,version) (source (origin (method url-fetch)@@ -246,3 +257,41 @@ path to the repository." #:repo->guix-package (lambda (name repo) (opam->guix-package name)) #:guix-name ocaml-name->guix-name))++(define (guix-package->opam-name package)+ "Given an OCaml PACKAGE built from OPAM, return the name of the+package in OPAM."+ (let ((upstream-name (assoc-ref+ (package-properties package)+ 'upstream-name))+ (name (package-name package)))+ (cond+ (upstream-name upstream-name)+ ((string-prefix? "ocaml-" name) (substring name 6))+ (else name))))++(define (opam-package? package)+ "Return true if PACKAGE is an OCaml package from OPAM"+ (and+ (equal? (build-system-name (package-build-system package)) 'ocaml)+ (not (string-prefix? "ocaml4" (package-name package)))))++(define (latest-release package)+ "Return an <upstream-source> for the latest release of PACKAGE."+ (and-let* ((opam-name (guix-package->opam-name package))+ (opam-file (opam-fetch opam-name))+ (version (assoc-ref opam-file "version"))+ (opam-content (assoc-ref opam-file "metadata"))+ (url-dict (metadata-ref opam-content "url"))+ (source-url (metadata-ref url-dict "src")))+ (upstream-source+ (package (package-name package))+ (version version)+ (urls (list source-url)))))++(define %opam-updater+ (upstream-updater+ (name 'opam)+ (description "Updater for OPAM packages")+ (pred opam-package?)+ (latest latest-release)))-- 2.19.2
J
J
Julien Lepiller wrote on 20 Dec 2018 12:01
[PATCH 4/5] gnu: ocaml-graph: Add upstream-name.
(address . 33811@debbugs.gnu.org)(name . Julien Lepiller)(address . julien@lepiller.eu)
20181220110103.4219-4-julien@lepiller.eu
* gnu/packages/ocaml.scm (ocaml-graph)[properties]: Add upstream-name.--- gnu/packages/ocaml.scm | 1 + 1 file changed, 1 insertion(+)
Toggle diff (14 lines)diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scmindex 503e42297..a0d2eac95 100644--- a/gnu/packages/ocaml.scm+++ b/gnu/packages/ocaml.scm@@ -4134,6 +4134,7 @@ and 4 (random based) according to RFC 4122.") (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") "/bin/sh"))))))) (inputs `(("lablgtk" ,lablgtk)))+ (properties `((upstream-name . "ocamlgraph"))) (home-page "http://ocamlgraph.lri.fr/") (synopsis "Graph library for OCaml") (description "OCamlgraph is a generic graph library for OCaml.")-- 2.19.2
J
J
Julien Lepiller wrote on 20 Dec 2018 12:01
[PATCH 5/5] import: opam: Parse comments.
(address . 33811@debbugs.gnu.org)(name . Julien Lepiller)(address . julien@lepiller.eu)
20181220110103.4219-5-julien@lepiller.eu
* guix/import/opam.scm: Add comment support in parser.--- guix/import/opam.scm | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-)
Toggle diff (16 lines)diff --git a/guix/import/opam.scm b/guix/import/opam.scmindex b30d28561..c254db5f2 100644--- a/guix/import/opam.scm+++ b/guix/import/opam.scm@@ -42,7 +42,8 @@ %opam-updater)) ;; Define a PEG parser for the opam format-(define-peg-pattern SP none (or " " "\n"))+(define-peg-pattern comment none (and "#" (* STRCHR) "\n"))+(define-peg-pattern SP none (or " " "\n" comment)) (define-peg-pattern SP2 body (or " " "\n")) (define-peg-pattern QUOTE none "\"") (define-peg-pattern QUOTE2 body "\"")-- 2.19.2
J
J
Julien Lepiller wrote on 27 Dec 2018 09:30
Re: [bug#33811] [PATCH] Opam importer improvements
(address . 33811@debbugs.gnu.org)
20181227093003.7c2c1bcf@lepiller.eu
Le Thu, 20 Dec 2018 11:41:00 +0100,Julien Lepiller <julien@lepiller.eu> a écrit :
Toggle quote (9 lines)> Hi,> > here are a few improvements to the opam importer. The first patch is > somewhat unrelated and moves coq and coq packages away from ocaml.scm> to a new coq.scm file. The second and third patches add a recursive> option and an updater for opam, while the fourth and fith patches> make sure it works for ocaml-graph: I found that the importer didn't> support comments that are present in the opam file for ocamlgraph.
Hi,
I'd like to push this series soonish. I can wait a bit more if anyonewants to make a review of course. Thank you!
R
R
Ricardo Wurmus wrote on 17 Feb 2019 11:58
control message for bug #33811
(address . control@debbugs.gnu.org)
168fb1bc81e.a85897d1611664973.7714948897538901579@zoho.com
tags 33811 fixedclose 33811
?
Your comment

This issue is archived.

To comment on this conversation send email to 33811@debbugs.gnu.org