* [bug#33811] [PATCH] Opam importer improvements
@ 2018-12-20 10:41 Julien Lepiller
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
2018-12-27 8:30 ` [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
0 siblings, 2 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 10:41 UTC (permalink / raw)
To: 33811
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.
^ permalink raw reply [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq.
2018-12-20 10:41 [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
@ 2018-12-20 11:00 ` Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 2/5] import: opam: Add recursive option Julien Lepiller
` (3 more replies)
2018-12-27 8:30 ` [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
1 sibling, 4 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 11:00 UTC (permalink / raw)
To: 33811
* 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
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
new file mode 100644
index 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.scm
index 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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH 2/5] import: opam: Add recursive option.
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
@ 2018-12-20 11:01 ` Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 3/5] import: opam: Add updater Julien Lepiller
` (2 subsequent siblings)
3 siblings, 0 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 11:01 UTC (permalink / raw)
To: 33811
* 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(-)
diff --git a/guix/import/opam.scm b/guix/import/opam.scm
index 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.scm
index 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))
\f
@@ -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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH 3/5] import: opam: Add updater.
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 2/5] import: opam: Add recursive option Julien Lepiller
@ 2018-12-20 11:01 ` Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 4/5] gnu: ocaml-graph: Add upstream-name Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 5/5] import: opam: Parse comments Julien Lepiller
3 siblings, 0 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 11:01 UTC (permalink / raw)
To: 33811
* guix/import/opam.scm (%opam-updater): New variable.
---
guix/import/opam.scm | 59 ++++++++++++++++++++++++++++++++++++++++----
1 file changed, 54 insertions(+), 5 deletions(-)
diff --git a/guix/import/opam.scm b/guix/import/opam.scm
index 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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH 4/5] gnu: ocaml-graph: Add upstream-name.
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 2/5] import: opam: Add recursive option Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 3/5] import: opam: Add updater Julien Lepiller
@ 2018-12-20 11:01 ` Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 5/5] import: opam: Parse comments Julien Lepiller
3 siblings, 0 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 11:01 UTC (permalink / raw)
To: 33811
* gnu/packages/ocaml.scm (ocaml-graph)[properties]: Add upstream-name.
---
gnu/packages/ocaml.scm | 1 +
1 file changed, 1 insertion(+)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH 5/5] import: opam: Parse comments.
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
` (2 preceding siblings ...)
2018-12-20 11:01 ` [bug#33811] [PATCH 4/5] gnu: ocaml-graph: Add upstream-name Julien Lepiller
@ 2018-12-20 11:01 ` Julien Lepiller
3 siblings, 0 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-20 11:01 UTC (permalink / raw)
To: 33811
* guix/import/opam.scm: Add comment support in parser.
---
guix/import/opam.scm | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/guix/import/opam.scm b/guix/import/opam.scm
index 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
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [bug#33811] [PATCH] Opam importer improvements
2018-12-20 10:41 [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
@ 2018-12-27 8:30 ` Julien Lepiller
1 sibling, 0 replies; 7+ messages in thread
From: Julien Lepiller @ 2018-12-27 8:30 UTC (permalink / raw)
To: 33811
Le Thu, 20 Dec 2018 11:41:00 +0100,
Julien Lepiller <julien@lepiller.eu> a écrit :
> 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 anyone
wants to make a review of course. Thank you!
^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2018-12-27 8:31 UTC | newest]
Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-12-20 10:41 [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
2018-12-20 11:00 ` [bug#33811] [PATCH 1/5] gnu: Move coq packages from ocaml to coq Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 2/5] import: opam: Add recursive option Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 3/5] import: opam: Add updater Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 4/5] gnu: ocaml-graph: Add upstream-name Julien Lepiller
2018-12-20 11:01 ` [bug#33811] [PATCH 5/5] import: opam: Parse comments Julien Lepiller
2018-12-27 8:30 ` [bug#33811] [PATCH] Opam importer improvements Julien Lepiller
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.