From unknown Sun Jun 15 13:00:24 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#33811 <33811@debbugs.gnu.org> To: bug#33811 <33811@debbugs.gnu.org> Subject: Status: [PATCH] Opam importer improvements Reply-To: bug#33811 <33811@debbugs.gnu.org> Date: Sun, 15 Jun 2025 20:00:24 +0000 retitle 33811 [PATCH] Opam importer improvements reassign 33811 guix-patches submitter 33811 Julien Lepiller severity 33811 normal tag 33811 fixed patch thanks From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 05:41:37 2018 Received: (at submit) by debbugs.gnu.org; 20 Dec 2018 10:41:37 +0000 Received: from localhost ([127.0.0.1]:55490 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZvlp-0003eu-EF for submit@debbugs.gnu.org; Thu, 20 Dec 2018 05:41:37 -0500 Received: from eggs.gnu.org ([208.118.235.92]:44410) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZvln-0003ei-8A for submit@debbugs.gnu.org; Thu, 20 Dec 2018 05:41:35 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gZvlZ-0004n9-4q for submit@debbugs.gnu.org; Thu, 20 Dec 2018 05:41:27 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-0.5 required=5.0 tests=BAYES_05 autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:36622) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gZvlS-0004j0-EQ for submit@debbugs.gnu.org; Thu, 20 Dec 2018 05:41:15 -0500 Received: from eggs.gnu.org ([2001:4830:134:3::10]:54005) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gZvlR-0003ff-Lp for guix-patches@gnu.org; Thu, 20 Dec 2018 05:41:14 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gZvlM-0004fe-HY for guix-patches@gnu.org; Thu, 20 Dec 2018 05:41:13 -0500 Received: from lepiller.eu ([2a00:5884:8208::1]:38336) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gZvlM-0004eW-5P for guix-patches@gnu.org; Thu, 20 Dec 2018 05:41:08 -0500 Received: from webmail.lepiller.eu (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 175e3db3 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Thu, 20 Dec 2018 10:38:00 +0000 (UTC) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Date: Thu, 20 Dec 2018 11:41:00 +0100 From: Julien Lepiller To: guix-patches@gnu.org Subject: [PATCH] Opam importer improvements Message-ID: X-Sender: julien@lepiller.eu User-Agent: Roundcube Webmail/1.3.8 X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -6.0 (------) 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. From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 06:04:26 2018 Received: (at 33811) by debbugs.gnu.org; 20 Dec 2018 11:04:26 +0000 Received: from localhost ([127.0.0.1]:55502 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7p-0004Ek-Lk for submit@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:26 -0500 Received: from lepiller.eu ([89.234.186.109]:45708) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7m-0004EU-4k for 33811@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:19 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 32b707ac (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Thu, 20 Dec 2018 11:01:10 +0000 (UTC) From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: [PATCH 1/5] gnu: Move coq packages from ocaml to coq. Date: Thu, 20 Dec 2018 12:00:59 +0100 Message-Id: <20181220110103.4219-1-julien@lepiller.eu> X-Mailer: git-send-email 2.19.2 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 +;;; +;;; 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 . + +(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 From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 06:04:26 2018 Received: (at 33811) by debbugs.gnu.org; 20 Dec 2018 11:04:26 +0000 Received: from localhost ([127.0.0.1]:55506 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7u-0004F7-5C for submit@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:26 -0500 Received: from lepiller.eu ([89.234.186.109]:45708) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7o-0004EU-LC for 33811@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:21 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 02a478bc (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Thu, 20 Dec 2018 11:01:10 +0000 (UTC) From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: [PATCH 2/5] import: opam: Add recursive option. Date: Thu, 20 Dec 2018 12:01:00 +0100 Message-Id: <20181220110103.4219-2-julien@lepiller.eu> X-Mailer: git-send-email 2.19.2 In-Reply-To: <20181220110103.4219-1-julien@lepiller.eu> References: <20181220110103.4219-1-julien@lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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)) @@ -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 From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 06:04:27 2018 Received: (at 33811) by debbugs.gnu.org; 20 Dec 2018 11:04:27 +0000 Received: from localhost ([127.0.0.1]:55508 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7u-0004FF-Ki for submit@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:26 -0500 Received: from lepiller.eu ([89.234.186.109]:45708) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7p-0004EU-Dd for 33811@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:21 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 524c80a7 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Thu, 20 Dec 2018 11:01:10 +0000 (UTC) From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: [PATCH 3/5] import: opam: Add updater. Date: Thu, 20 Dec 2018 12:01:01 +0100 Message-Id: <20181220110103.4219-3-julien@lepiller.eu> X-Mailer: git-send-email 2.19.2 In-Reply-To: <20181220110103.4219-1-julien@lepiller.eu> References: <20181220110103.4219-1-julien@lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 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 From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 06:04:27 2018 Received: (at 33811) by debbugs.gnu.org; 20 Dec 2018 11:04:27 +0000 Received: from localhost ([127.0.0.1]:55510 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7u-0004FM-W9 for submit@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:27 -0500 Received: from lepiller.eu ([89.234.186.109]:45710) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7p-0004Ee-Fn for 33811@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:21 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 90f1f607 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Thu, 20 Dec 2018 11:01:10 +0000 (UTC) From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: [PATCH 4/5] gnu: ocaml-graph: Add upstream-name. Date: Thu, 20 Dec 2018 12:01:02 +0100 Message-Id: <20181220110103.4219-4-julien@lepiller.eu> X-Mailer: git-send-email 2.19.2 In-Reply-To: <20181220110103.4219-1-julien@lepiller.eu> References: <20181220110103.4219-1-julien@lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 20 06:04:27 2018 Received: (at 33811) by debbugs.gnu.org; 20 Dec 2018 11:04:27 +0000 Received: from localhost ([127.0.0.1]:55512 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7v-0004FT-CX for submit@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:27 -0500 Received: from lepiller.eu ([89.234.186.109]:45708) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZw7q-0004EU-58 for 33811@debbugs.gnu.org; Thu, 20 Dec 2018 06:04:22 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 7609c7c6 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Thu, 20 Dec 2018 11:01:10 +0000 (UTC) From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: [PATCH 5/5] import: opam: Parse comments. Date: Thu, 20 Dec 2018 12:01:03 +0100 Message-Id: <20181220110103.4219-5-julien@lepiller.eu> X-Mailer: git-send-email 2.19.2 In-Reply-To: <20181220110103.4219-1-julien@lepiller.eu> References: <20181220110103.4219-1-julien@lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 Cc: Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * 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 From debbugs-submit-bounces@debbugs.gnu.org Thu Dec 27 03:30:24 2018 Received: (at 33811) by debbugs.gnu.org; 27 Dec 2018 08:30:24 +0000 Received: from localhost ([127.0.0.1]:38150 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gcR3b-0004VK-En for submit@debbugs.gnu.org; Thu, 27 Dec 2018 03:30:23 -0500 Received: from lepiller.eu ([89.234.186.109]:45786) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gcR3V-0004V6-LM for 33811@debbugs.gnu.org; Thu, 27 Dec 2018 03:30:17 -0500 Received: from localhost (41.189.239.238 [41.189.239.238]) by lepiller.eu (OpenSMTPD) with ESMTPSA id e7f6998a (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <33811@debbugs.gnu.org>; Thu, 27 Dec 2018 08:26:53 +0000 (UTC) Date: Thu, 27 Dec 2018 09:30:03 +0100 From: Julien Lepiller To: 33811@debbugs.gnu.org Subject: Re: [bug#33811] [PATCH] Opam importer improvements Message-ID: <20181227093003.7c2c1bcf@lepiller.eu> In-Reply-To: References: X-Mailer: Claws Mail 3.17.1 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33811 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Le Thu, 20 Dec 2018 11:41:00 +0100, Julien Lepiller a =C3=A9crit : > Hi, >=20 > here are a few improvements to the opam importer. The first patch is=20 > 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! From debbugs-submit-bounces@debbugs.gnu.org Sun Feb 17 05:59:22 2019 Received: (at control) by debbugs.gnu.org; 17 Feb 2019 10:59:22 +0000 Received: from localhost ([127.0.0.1]:50759 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gvKAM-0003AO-3j for submit@debbugs.gnu.org; Sun, 17 Feb 2019 05:59:22 -0500 Received: from sender-of-o51.zoho.com ([135.84.80.216]:21011) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gvKAK-0003AG-D8 for control@debbugs.gnu.org; Sun, 17 Feb 2019 05:59:21 -0500 ARC-Seal: i=1; a=rsa-sha256; t=1550401129; cv=none; d=zoho.com; s=zohoarc; b=VjG2XV+jMTt8w97WVNN4CzC2ALWFVr+bxSa/WCtPqO9Hzg9t7ddoF647e0PO5OLIRqdoAbmIEyCJ7lgfTOHeKqduU4vZ7fDE0A7Qg1dBHFKUWWYy4Q8xfQSUQ40bqSgQPnNUQAYS4kZexnuzioqEfcWEoJ1Ze3APGfnccmmd3Fs= ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=zoho.com; s=zohoarc; t=1550401129; h=Date:From:Message-ID:Subject:To:ARC-Authentication-Results; bh=maaTGYH3scpBkVd879CHJA5aHGpx49Vx1J7yuTVyLqE=; b=N5SPrOUwRNuYbxvqNh60xBCNls4VabbHWR8+us7bAGBvHATISlwXlWpWJP1PO/3Hi3rcP5dfEE8OMRsUyhmeVoTw7Q4NMo0dyIb9hyukJBSnLEQyLSybEpOTrBQOtQ8kJSoOmIQAb+0oqfQUslzLA9HGQBGxMExkWtTMKTsVc84= ARC-Authentication-Results: i=1; mx.zoho.com; dkim=pass header.i=elephly.net; spf=pass smtp.mailfrom=rekado@elephly.net; dmarc=pass header.from= header.from= DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; t=1550401129; s=zoho; d=elephly.net; i=rekado@elephly.net; h=Date:To:From:Message-ID:Subject; l=31; bh=maaTGYH3scpBkVd879CHJA5aHGpx49Vx1J7yuTVyLqE=; b=bzhHsld6M8kHg6mlDRICgaM5cuUwSc0peZkb8UYdKlbjvSjQBFM3CjRJA5PTWCrU PsR1SZ/RID5Kll6w21KEIufkDhY2NfeGZw/ekltQcxH1kmYxrxRuUXUT6f1ec1Esghz LHhMJLe9jj8nkmIXVa9GOs+oe6+nSpZQKAnIotI4= Received: from localhost (p3E9E98D8.dip0.t-ipconnect.de [62.158.152.216]) by mx.zohomail.com with SMTPS id 1550401128476411.55094392675494; Sun, 17 Feb 2019 02:58:48 -0800 (PST) Date: Sun, 17 Feb 2019 11:58:45 +0100 To: control@debbugs.gnu.org From: Ricardo Wurmus Message-ID: <168fb1bc81e.a85897d1611664973.7714948897538901579@zoho.com> Subject: control message for bug #33811 X-ZohoMailClient: External X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: control X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) tags 33811 fixed close 33811 From unknown Sun Jun 15 13:00:24 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 17 Mar 2019 11:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator