From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id 8LVtANzMcGM5rwAAbAwnHQ (envelope-from ) for ; Sun, 13 Nov 2022 11:54:20 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id AEGHANzMcGO3DQEA9RJhRA (envelope-from ) for ; Sun, 13 Nov 2022 11:54:20 +0100 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 3BA6E3E50F for ; Sun, 13 Nov 2022 11:54:19 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ouAcm-0000b8-Rv; Sun, 13 Nov 2022 05:54:04 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ouAck-0000az-QM for guix-patches@gnu.org; Sun, 13 Nov 2022 05:54:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ouAck-0003TR-IP for guix-patches@gnu.org; Sun, 13 Nov 2022 05:54:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ouAck-0006Eg-7D for guix-patches@gnu.org; Sun, 13 Nov 2022 05:54:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#58310] Manifest for coq-mathcomp-analysis Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 13 Nov 2022 10:54:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 58310 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Garek Dyszel , zimoun , 58310@debbugs.gnu.org Cc: pukkamustard Received: via spool by 58310-submit@debbugs.gnu.org id=B58310.166833679323910 (code B ref 58310); Sun, 13 Nov 2022 10:54:02 +0000 Received: (at 58310) by debbugs.gnu.org; 13 Nov 2022 10:53:13 +0000 Received: from localhost ([127.0.0.1]:50143 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ouAbv-0006DY-DA for submit@debbugs.gnu.org; Sun, 13 Nov 2022 05:53:13 -0500 Received: from lepiller.eu ([89.234.186.109]:52356) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ouAbr-0006DN-Fx for 58310@debbugs.gnu.org; Sun, 13 Nov 2022 05:53:09 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 8e22513e; Sun, 13 Nov 2022 10:53:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:message-id:in-reply-to:references:mime-version :content-type; s=dkim; bh=zNKTkLYwymzgcLGWfjpkKqJWP/+TGKKLnP4bLQ OR2uA=; b=IMBfajCtl4MttgLcgjZ18wR4y6Bgza9JY51X2hfxvB2hdgxRL84axw kWdcoGYe2x6joveUsvVDOi2go7POC23PobQl5oiXD3Yavozj9oyoKCIBTBJ2qzv5 vJPW7vOH/Eml83CBuktTMU4SI0U4zgox40qhyRvpB0dJ8syP8NE/yb4W6ZsnJPOQ iT/aP5Jg2ympvHv+oCuxD4+TwRyw5v/vfkdYYKDYajQ2Ze0/H42h7f4PCjOTXM0m 5fn3uSrB4Gx1gsDYZNmld15cK7TkFL3le/Rui91X2yA5ADkyAniiTJxMgzoas6iQ 2OWhzhlNIpn/rEqDzDhrS6kfyO9pmO5Q== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 0f3d1e8f (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Sun, 13 Nov 2022 10:53:04 +0000 (UTC) Date: Sun, 13 Nov 2022 11:53:03 +0100 From: Julien Lepiller Message-ID: <20221113115303.66ccb071@sybil.lepiller.eu> In-Reply-To: References: <87h70iqji2.fsf@disroot.org> <87v8njspi5.fsf@disroot.org> X-Mailer: Claws Mail 4.1.1 (GTK 3.24.30; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/uvRhSCMl/XdMwbzM4kqo_=n" X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1668336859; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post: dkim-signature; bh=hON/pSZ2Zx5PpQt1nN8HHz3rh8RYoxerBe0TGU5HyO0=; b=W3f2D42pKess+m54KYs8bEaDe0tTKi5ziU8f+YZHE4Wp30UGnh1mZNqku6sXVnbIgsiMdY c/Ipm5V2WdyTs7ELEQMZ2DLoCJLi6aHqN9BvYeqN31FInurx6B0NZlIzusM4Y7QMx1thP4 iDlgHu666PkS7+YNWeUbOX/eQFSmgkb8gJpp/qIVVIxzHxOW6d3blo67W0ItfW5GJW5yY8 AgV7n/dxz5Jwr4uwPFcoea+qJJR4wB2nZc2hyTM6HeDW3Ek0g6sjhY8s/5LwlP4+mOAcRP AvNrkvSu86X+31nIPBKKuEtqiyfyDcExa1k+tlQ/4iRVqr50TUfEJDW1dnFxYw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1668336859; a=rsa-sha256; cv=none; b=ezcDZrxdVqgq8VV+YMwerGSD5ni7po7MhylDigp6+Bhv+yIJ4LDUbAkJKDJOjtakNmjsEm 07ud8xUbBYFbXJf6ceXbfPZzUwYJ02bYmhCbtq5ZKHcns3P7tZmPQb3QOdy6JKlviw+exY xfpa5dvYBKcmoxWse5u0z+U76XPypqU6T/LDGMEMjNQjCu56e7bQMr6JsymE/8mND5+vpD CyIquFHzUSdPjsLSTltw60/llrPcmtFItjyMtv1TwSJ2dVfBOLZ40BNxQDQYt7wUDyV/iQ +DBv1XJvfBgxYaohC4Wsrmf/Ts55HlzFcGvd+dgS1N9j4L3G3hM2OP0oDhSstw== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=IMBfajCt; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: 8.95 X-Spam: Yes Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=IMBfajCt; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 3BA6E3E50F X-Spam-Score: 8.95 X-Migadu-Spam: Yes X-Migadu-Scanner: scn1.migadu.com X-TUID: yilYW13A+XWc --MP_/uvRhSCMl/XdMwbzM4kqo_=n Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline So, I've had a further look at the sources for the failing packages and figured that some variables were missing in the make-flags. Attached is the fixed version of your file that builds coq-mathcomp-analysis. Note that the build of mathcomp-analysis is very quiet and takes a long time, but it works eventually. Le Sun, 13 Nov 2022 10:17:07 +0100, Julien Lepiller a =C3=A9crit : > Hi! >=20 > I tried building your file (it's technically not a manifest) and > indeed it's failing in the chack-findlib-path. >=20 > Why do you want to run it? There's no way it could work at this > point, right after the check phase, since the package is not even > installed yet. Also, the OCAMLPATH that would allow findlib to find > it is not set to the outputs, only to the inputs. >=20 > Le 13 novembre 2022 00:48:50 GMT+01:00, Garek Dyszel > a =C3=A9crit=C2=A0: > >Hi, > > > >CC: ocaml team > > > >I am including a manifest file instead of sending patches for now. It > >seems like a good idea to stick with that until these packages are > >ready to be put into the Guix source tree. I'm refactoring them too > >often. > > > >After opening an issue on Github [1] [2], it seems that coq-elpi is > >the package that is not building properly. It is clear that > >ocamlfind (from ocaml-findlib) can't find coq-elpi after coq-elpi's > >install phase. [1]: > >https://github.com/math-comp/hierarchy-builder/issues/320 [2]: > >https://github.com/LPCIC/coq-elpi/issues/384 > > > >It looks like the META file is not being installed by coq-elpi > >either. I'm not sure whether that's relevant, since ocamlfind > >couldn't find coq-elpi even when META was present (in a much older > >revision of this manifest; I can dig for it but just today don't > >have time). > > > >The problem seems to be something in the build process itself; if the > >extra phase 'check-findlib-path' is omitted then coq-elpi's build is > >reported as a success. > > > >The later package coq-mathcomp-hierarchy-builder runs ocamlfind to > >find coq-elpi, too. > > > >What would be a way to ensure that coq-elpi is found by ocamlfind?=20 > > > >Thanks! > >Garek > > > >(Manifest attached with an ocaml-elpi patch. You will need to change > >the path for the ocaml-elpi (patches) field to match your directory > >structure, but otherwise this manifest should work.) > > =20 --MP_/uvRhSCMl/XdMwbzM4kqo_=n Content-Type: text/x-scheme Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=coq-mathcomp-analysis.scm ;; -*- mode: scheme; mode: guix-devel -*- ;;; Local Variables: ;;; sentence-end-double-space: t ;;; End: ;;; This module extends GNU=C2=A0Guix and is licensed under the same terms,= those ;;; of the GNU GPL version 3 or (at your option) any later version. ;;; ;;; Copyright =C2=A9 2022 Garek Dyszel ;; To build directly from this file, use the following command. ;; guix build --with-patch=3Docaml-elpi=3Dpatches/ocaml-elpi-fix-yojson.pat= ch -Kf coq-mathcomp-analysis.scm (define-module (coq-mathcomp-analysis) #:use-module (guix) #:use-module (guix git-download) #:use-module (guix download) #:use-module (guix packages) #:use-module (guix build-system gnu) #:use-module (guix build gnu-build-system) #:use-module (guix build-system dune) #:use-module (guix build-system ocaml) #:use-module (guix build-system pyproject) ;; #:use-module ((guix build utils) #:prefix utils:) #:use-module ((guix licenses) #:prefix license:) #:use-module ((gnu packages base) #:prefix base:) #:use-module (guix build utils) #:use-module (guix utils) #:use-module (guix profiles) #:use-module (gnu packages) #:use-module (gnu packages coq) #:use-module (gnu packages base) #:use-module (gnu packages ocaml) #:use-module (gnu packages time) #:use-module (gnu packages python) #:use-module (gnu packages python-xyz) #:use-module (gnu packages python-build) #:use-module (gnu packages python-web) #:use-module (gnu packages python-crypto) #:use-module (gnu packages xdisorg) #:use-module (guix build-system python) #:use-module (gnu packages python-check) #:use-module (gnu packages check) #:use-module (gnu packages java) #:use-module (gnu packages python-compression) #:use-module (gnu packages lua) #:use-module (gnu packages version-control)) ;;; Python (define-public python-pprintpp ;; Git version tags are inaccurate for this package; use the ;; bare commit. (let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0") (revision "1")) (package (name "python-pprintpp") (version (git-version "0.3.0" revision commit)) (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/wolever/pprintpp") (commit commit))) (file-name (git-file-name name version)) (sha256 (base32 "0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li")))) (inputs (list python-pypa-build python-hypothesis python-wheel python-parameterized)) (native-inputs (list python-pytest python-nose)) (build-system pyproject-build-system) (arguments (list #:phases #~(modify-phases %standard-phases (replace 'build (lambda _ (setenv "SOURCE_DATE_EPOCH" "315532800") (invoke "python" "-m" "build" "--wheel" "--no-isolation" "."))) (replace 'install (lambda* (#:key outputs #:allow-other-keys) (let ((whl (car (find-files "dist" "\\.whl$")= ))) (invoke "pip" "--no-cache-dir" "--no-input" "install" "--no-deps" "--prefix" #$output whl)))) (replace 'check (lambda* (#:key tests? #:allow-other-keys) (when tests? (invoke "python" "test.py"))))))) (home-page "https://github.com/wolever/pprintpp") (synopsis "Python pretty-printer") (description "This package is a printer for Python which pretty-prints structures. It also attempts to print Unicode characters without escaping them.") (license license:bsd-3)))) (define-public python-pluggy-1.0 (package (inherit python-pluggy) (name "python-pluggy") (version "1.0.0") (source (origin (method url-fetch) (uri (pypi-uri "pluggy" version)) (sha256 (base32 "0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922")))) (inputs (list python-pypa-build python-wheel)) (native-inputs (list python-pytest python-setuptools-scm)))) (define-public python-setuptools-scm-7 (package (inherit python-setuptools-scm) (version "7.0.5") (source (origin (method url-fetch) (uri (pypi-uri "setuptools_scm" version)) (sha256 (base32 "0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3")))) (build-system pyproject-build-system) (arguments `( ;Disabled tests to avoid extra dependencies. #:tests? #f #:phases (modify-phases %standard-phases ;; Disabled sanity check to avoid extra dependencies. (delete 'sanity-check)))) (propagated-inputs (list python-packaging-bootstrap python-tomli)))) (define-public python-pathspec-0.10.1 (package (name "python-pathspec") (version "0.10.1") (source ;; (origin ;; (method url-fetch) ;; (uri (pypi-uri "pathspec" version)) ;; (sha256 ;; (base32 ;; "0g9jhhhf3zmrnvzvjjd2yhizsb6i93hmlszb09wixlr1nrhn3kks"))) (origin (method git-fetch) (uri (git-reference (url "https://github.com/cpburnz/python-pathspec") (commit (string-append "v" version)))) (sha256 (base32 "0sgzh7ad1x098d0rln01f0qabpa7mnp26863isncbiyqsxh1gaxp")))) (build-system pyproject-build-system) (home-page "https://github.com/cpburnz/python-pathspec") (synopsis "Utility library for gitignore style pattern matching of file paths.") (description "Utility library for gitignore style pattern matching of file paths.") (license license:mpl2.0))) ;; This depends on packages in python-xyz.scm: ;; python-version, python-importlib-metadata, python-pathspec, ;; python-pluggy-1.0, and python-platformdirs. (define-public python-hatchling (package (name "python-hatchling") (version "1.10.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/pypa/hatch") (commit (string-append "hatchling-v" version)))) (file-name (git-file-name name version)) (sha256 (base32 "0ahx62w711a2vnb91ahqxrw8yi0gq0kfch3fk6akzngd13376czj")))) ;; python-pypa-build needed for bootstrapping. ;; Otherwise we get a circular reference: ;; python-hatchling trying to build itself, without ;; first having hatchling installed. (inputs (list python-editables python-packaging-bootstrap ;; Below from python-xyz.scm, can be moved to python-buil= d.scm python-pathspec-0.10.1 ;; Below from python-xyz.scm, can be moved to python-buil= d.scm python-pluggy-1.0 python-tomli)) (build-system pyproject-build-system) (arguments `( ;Tests depend on module python-hatch, which would result in circula= r references #:tests? #f #:phases (modify-phases %standard-phases (replace 'build (lambda _ (chdir "backend") ;; ZIP does not support timestamps before 1980. (setenv "SOURCE_DATE_EPOCH" "315532800") (invoke "python" "-m" "build" "--wheel" "--no-isolation" "."))) (replace 'install (lambda* (#:key outputs #:allow-other-keys) (let ((whl (car (find-files "dist" "\\.whl$")))) (invoke "pip" "--no-cache-dir" "--no-input" "install" "--no-deps" "--prefix" (assoc-ref %outputs "out") whl))))))) (home-page "https://ofek.dev/projects/hatch/") (synopsis "Bootstrap binaries to build @code{python-hatch}") (description "Bootstrap binaries to build @code{python-hatch}") ;; MIT License (license license:expat))) ;; (define-public python-hatchling ;; (package ;; (name "python-hatchling") ;; (version "1.10.0") ;; (source (origin ;; (method git-fetch) ;; (uri (git-reference ;; (url "https://github.com/pypa/hatch") ;; (commit (string-append "hatchling-v" version)))) ;; (file-name (git-file-name name version)) ;; (sha256 ;; (base32 ;; "0ahx62w711a2vnb91ahqxrw8yi0gq0kfch3fk6akzngd13376czj"))= )) ;; (inputs (list python-editables ;; python-packaging-bootstrap ;; ;; Below from python-xyz.scm, can be moved to python-b= uild.scm ;; python-pathspec-0.10.1 ;; ;; Below from python-xyz.scm, can be moved to python-b= uild.scm ;; python-pluggy-1.0 ;; python-tomli ;; python-hatchling-bootstrap)) ;; (build-system pyproject-build-system) ;; (arguments ;; `( ;Tests depend on module python-hatch, which this ;; ;; is bootstrapping. ;; #:tests? #f ;; #:phases (modify-phases %standard-phases ;; (replace 'build ;; (lambda _ ;; (chdir "backend") ;; ;; ZIP does not support timestamps before 1980. ;; (setenv "SOURCE_DATE_EPOCH" "315532800") ;; (invoke "python" ;; "-m" ;; "build" ;; "--wheel" ;; "--no-isolation" ;; "."))) ;; (replace 'install ;; (lambda* (#:key outputs #:allow-other-keys) ;; (let ((whl (car (find-files "dist" "\\.whl$")))) ;; (invoke "pip" ;; "--no-cache-dir" ;; "--no-input" ;; "install" ;; "--no-deps" ;; "--prefix" ;; (assoc-ref %outputs "out") ;; whl))))))) ;; (home-page "https://ofek.dev/projects/hatch/") ;; (synopsis "Bootstrap binaries to build @code{python-hatch}") ;; (description "Bootstrap binaries to build @code{python-hatch}") ;; ;; MIT License ;; (license license:expat))) (define-public python-hatch (package (name "python-hatch") (version "1.6.2") ;; at minimum 1.5.0 (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/pypa/hatch") (commit (string-append "hatch-v" version)))) (file-name (git-file-name name version)) (sha256 (base32 "0if5ssp6vlfvna1jcvap40r0f7pm45h7kbia78h5ivm17vb8p08b" ;;"030yi9hw50mn899pq073lw2a55r57skl2g9agjp3b4l95f3nay30" )))) (inputs (list python-pypa-build python-editables python-importlib-metadata python-version python-packaging-next python-pathspec python-pluggy-1.0 ;TODO: Not detected by pytest? python-hatchling python-tomli python-platformdirs python-rich python-tomli-w)) (build-system pyproject-build-system) (arguments `( ;Tests appear to be written such that the input python-pluggy-1.0 is ;; not detected. #:tests? #f #:phases (modify-phases %standard-phases (replace 'build (lambda _ ;; ZIP does not support timestamps before 1980. (setenv "SOURCE_DATE_EPOCH" "315532800") (invoke "hatchling" "build"))) (replace 'install (lambda* (#:key outputs #:allow-other-keys) (let ((whl (car (find-files "dist" "\\.whl$")))) (invoke "pip" "--no-cache-dir" "--no-input" "install" "--no-deps" "--prefix" (assoc-ref %outputs "out") whl)))) (replace 'check (lambda* (#:key tests? #:allow-other-keys) (when tests? (chdir "tests") (invoke "pytest" "-vv")))) ;; Can't have hatch as a requirement of itself. (delete 'sanity-check)))) (home-page "https://ofek.dev/projects/hatch/") (synopsis "Python build system with project generation") (description "Python build system with project generation. It also defines a speci= fic syntax in @code{toml} files to check for dependencies.") ;; MIT License (license license:expat))) (define-public python-hatch-vcs ;; Tags are not accurate; just use the commit itself. (let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2") (revision "1")) (package (name "python-hatch-vcs") (version (git-version "0.2.0" revision commit)) (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/ofek/hatch-vcs") (commit commit))) (file-name (git-file-name name version)) (sha256 (base32 "0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05")))) (build-system pyproject-build-system) (inputs (list python-pypa-build python-pathspec-0.10.1 python-pluggy-1.0 python-editables git python-hatchling ;; python-hatch python-typing-extensions)) (native-inputs (list python-pytest ;; python-setuptools-scm-6.4 minimum python-setuptools-scm-7)) ;; (arguments ;; (list #:phases #~(modify-phases %standard-phases ;; (replace 'build ;; (lambda _ ;; (setenv "SOURCE_DATE_EPOCH" "315532800") ;; (invoke "python" ;; "-m" ;; "build" ;; "--wheel" ;; "--no-isolation" ;; "."))) ;; (replace 'install ;; (lambda* (#:key outputs #:allow-other-keys) ;; (let ((whl (car (find-files "dist" "\\.whl= $")))) ;; (invoke "pip" ;; "--no-cache-dir" ;; "--no-input" ;; "install" ;; "--no-deps" ;; "--prefix" ;; #$output ;; whl)))) ;; (replace 'check ;; (lambda* (#:key tests? #:allow-other-keys) ;; (when tests? ;; (invoke "pytest" "-vvv"))))))) ;) (arguments `( ;Tests depend on module python-hatch, which this ;; is bootstrapping. #:tests? #f #:phases (modify-phases %standard-phases (replace 'build (lambda _ ;;(chdir "backend") ;; ZIP does not support timestamps before 1980. (setenv "SOURCE_DATE_EPOCH" "315532800") (invoke "python" "-m" "build" "--wheel" "--no-isolation" "."))) (replace 'install (lambda* (#:key outputs #:allow-other-keys) (let ((whl (car (find-files "dist" "\\.whl$")))) (invoke "pip" "--no-cache-dir" "--no-input" "install" "--no-deps" "--prefix" (assoc-ref %outputs "out") whl))))))) (home-page "https://ofek.dev/projects/hatch/") (synopsis "Plugin for @code{python-hatch} to include versions") (description "This plugin defines a version-control syntax for use with @code{toml} files intended for use with @code{python-hatch}.") ;; MIT License (license license:expat)))) (define-public python-pytest-icdiff (package (name "python-pytest-icdiff") (version "0.6") (source (origin (method url-fetch) (uri (pypi-uri "pytest-icdiff" version)) (sha256 (base32 "1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8")))) (build-system pyproject-build-system) (propagated-inputs (list python-pypa-build python-icdiff python-pprintpp python-pluggy-1.0)) (native-inputs (list python-pytest)) (arguments `(;; Tests fail with "collecting ... collected 0 items" #:tests? #f)) ;; (arguments ;; `(#:phases ;; (modify-phases %standard-phases ;; (add-before 'check 'chdir-to-test-dir ;; (chdir "tests"))))) (home-page "https://github.com/hjwp/pytest-icdiff") (synopsis "Colored diffs using @code{python-icdiff} for pytest output") (description "This package uses @code{python-icdiff} to add color to the output of pytest assertions.") (license (license:non-copyleft "LICENSE")))) (define-public python-hatch-fancy-pypi-readme (package (name "python-hatch-fancy-pypi-readme") (version "22.8.0") (source (origin (method url-fetch) (uri (pypi-uri "hatch_fancy_pypi_readme" version)) (sha256 (base32 ;; PyPI hash problem ;;"1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx" "0sn2wsfbpsbf2mqhjvw62h1cfy5mz3d7iqyqvs5c20cnl0n2i4fs")))) (build-system pyproject-build-system) (propagated-inputs (list python-tomli python-typing-extensions)) (native-inputs (list python-pypa-build python-pathspec-0.10.1 python-pluggy-1.0 python-editables python-hatchling python-wheel python-pytest python-pytest-icdiff)) (arguments `(#:phases (modify-phases %standard-phases (add-before 'build 'disable-broken-tests (lambda _ ;; Skip the tests for "building". Guix already does t= his, ;; so we don't need to test it for this package. (chdir "tests") (invoke "sed" "-i" "11ipytest.skip('No need to test\ building; guix does this already', allow_module_level=3DTrue)" "test_end_to_end.py") (chdir "../"))) ;; XXX: PEP 517 manual build/install procedures copied fr= om ;; python-isort. (replace 'build (lambda _ ;; ZIP does not support timestamps before 1980. (setenv "SOURCE_DATE_EPOCH" "315532800") (invoke "python" "-m" "build" "--wheel" "--no-isolation" "."))) (replace 'install (lambda* (#:key outputs #:allow-other-keys) (let ((whl (car (find-files "dist" "\\.whl$")))) (invoke "pip" "--no-cache-dir" "--no-input" "install" "--no-deps" "--prefix" (assoc-ref %outputs "out") whl)))) (replace 'check (lambda* (#:key tests? #:allow-other-keys) (when tests? (invoke "pytest" "-vv"))))))) (home-page "https://github.com/hynek/hatch-fancy-pypi-readme") (synopsis "Syntax for styling PyPI READMEs") (description "Defines a syntax for the python-hatch build system, intended for styl= ing READMEs for PyPI.") ;; MIT License (license license:expat))) ;; Has to be done manually. DO NOT copy and paste this one. (define-public python-jsonschema-4.15 (package (inherit python-jsonschema-next) (version "4.16.0") (source (origin (method url-fetch) (uri (pypi-uri "jsonschema" version)) (sha256 (base32 ;; PyPI hashing problem "08sbw5fn19vn8x7c216gkczyzd575702yx2vmqdrgxpgfvq5jl0n" ;;"07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11" )))) (native-inputs (list python-pypa-build python-twisted python-hatch python-hatchling python-pathspec-0.10.1 python-pluggy-1.0 python-editables python-hatch-vcs python-setuptools-scm-7 python-hatch-fancy-pypi-readme)) (propagated-inputs (list python-attrs python-importlib-metadata python-pyrsistent python-typing-extensions python-hatch-vcs)) (home-page "https://github.com/python-jsonschema/jsonschema"))) ;;; OCaml ;; Requires python-jsonschema with version at minimum 4.6.0 to run ;; tests.=20 ;; See https://github.com/ahrefs/atd/issues/306 for more info on that. (define-public ocaml-atd (package (name "ocaml-atd") (version "2.10.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/ahrefs/atd") (commit version))) (file-name (git-file-name name version)) (sha256 (base32 "10fgahdigrl01py0k0q2d6a60yps38q96dxhjnzm9jz4g931716l")))) (build-system dune-build-system) (arguments `(#:phases (modify-phases %standard-phases (replace 'check (lambda* (#:key tests? #:allow-other-keys) ;; The dune-build-system does not run "make test" but ;; "dune runtest test --release". ;; This project, rather, needs us to run "make test". ;; ;; For this package (ocaml-atd), we DO NOT run all the ;; tests. The atd repository has resources for several ;; different interfaces (python, scala, etc), but we ;; don't need to run those tests if we are just ;; interested in the ocaml interface. ;; So we stick with just the ocaml tests here. (when tests? (invoke "make" "test-ocaml"))))))) (propagated-inputs (list ocaml-menhir ocaml-easy-format ocaml-odoc ocaml-re ocaml-camlp-streams ocaml-biniou ocaml-yojson ocaml-cmdliner)) (native-inputs (list ocaml-alcotest python-pypa-build python-jsonschema-4.15 python-flake8 python-mypy python-pytest)) (inputs (list python)) (home-page "https://github.com/ahrefs/atd") (synopsis "Parser for the ATD data format description language") (description "ATD is an OCaml library providing a parser for the Adjustable Type Definitions language.") ;; Modified BSD license (license (license:non-copyleft "LICENSE.md")))) (define-public ocaml-elpi (package (name "ocaml-elpi") ;; For more information on which version works with Coq 8.16, ;; see the relevant issue: ;; https://github.com/math-comp/hierarchy-builder/issues/297 ;; Here we use ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16). ;; (version "1.15.2") ;;(version "1.16.5") (version "1.16.7") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/LPCIC/elpi") (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 (base32 ;; for 1.16.5 ;;"1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl" ;; for the version that the patch is based on (1.16.7) "1i0731f7jj48zvkla959pffj5l0qynmfyxljgszc6z3b4lpni1xc")) ;; Fix incompatibility with ocaml-yojson@2.0.2. ;; See . (patches (search-patches "ocaml-elpi-fix-yojson.patch")) ;(patches '("/home/chips/home/code/guix_packages/built/patche= s/ocaml-elpi-fix-yojson.patch")) )) (build-system dune-build-system) (arguments `(#:test-target "tests")) ;; Build currently fails with error (repeated several times): ;; 'Warning 6 [labels-omitted: label argsdepth was omitted in the ;; application of this function.' (propagated-inputs (list ocaml-stdlib-shims ocaml-ppxlib ocaml-menhir ocaml-re ocaml-ppx-deriving ocaml-atd ocaml-camlp-streams ocaml-biniou ocaml-yojson)) (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time)) (home-page "https://github.com/LPCIC/elpi") (synopsis "ELPI - Embeddable =CE=BBProlog Interpreter") (description "ELPI is an extension language for OCaml. It implements a variant of =CE=BBProlog enriched with Constraint Handling Rules, a programming languag= e for manipulating syntax trees with binders. This package provides both a command line interpreter, elpi, and an OCaml library with the same name.") (license license:lgpl2.1+))) ;;; Coq (define-public coq-elpi (package (name "coq-elpi") (version "1.16.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/LPCIC/coq-elpi") (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 (base32 "18w899fcz4kzx7zyr7a0g4avclbm5f82g7kh76b9fy2s99jz6q5c")))) ;;(build-system gnu-build-system) (build-system ocaml-build-system) (propagated-inputs (list coq-core ocaml-elpi ocaml-zarith)) (inputs (list python lua-5.1 coq-core coq-stdlib))=20 (arguments `(#:test-target "test" ;; From the repo: "COQBIN=3D%{bin}%/" "ELPIDIR=3D%{prefix}%/lib/elpi= " "OCAMLWARN=3D" #:make-flags ,#~(list (string-append "COQBIN=3D" #$(this-package-input "coq-core= ") "/bin/") (string-append "ELPIDIR=3D" #$(this-package-input "ocaml-el= pi") "/lib/ocaml/site-lib/elpi") (string-append "COQLIBINSTALL=3D" #$output "/lib/coq/user-contrib") (string-append "COQMF_COQLIB=3D" #$output "/lib/ocaml/site-lib/coq") (string-append "COQPLUGININSTALL=3D" #$output "/lib/ocaml/site-lib") "OCAMLWARN=3D") #:phases (modify-phases %standard-phases (delete 'configure) #;(add-after 'check 'check-findlib-path (lambda _ (invoke "ocamlfind" "query" "coq-elpi")))))) (home-page "https://github.com/LPCIC/coq-elpi") (synopsis "Elpi extension language for Coq") (description "Coq-elpi provides a Coq plugin that embeds ELPI, an extension language for OCaml that is an implementation of =CE=BBProlog. It also provides a wa= y to embed Coq's terms into =CE=BBProlog using the Higher-Order Abstract Syntax = approach and a way to read terms back. In addition to that it exports to ELPI a set= of Coq's primitives. Finally it provides a way to define new vernacular comma= nds and new tactics.") (license license:lgpl2.1))) (define-public coq-mathcomp-hierarchy-builder (package (name "coq-mathcomp-hierarchy-builder") ;; For more information on which version works with Coq 8.16, ;; see the relevant issue: ;; https://github.com/math-comp/hierarchy-builder/issues/297 ;; Here we use ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16) ;;(version "1.3.0") (version "1.4.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/math-comp/hierarchy-builder") (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 (base32 ;; 1.3.0 ;;"17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc" ;; 1.4.0 "1g7narbx5n8bbnnnn8kmgk62clah9fsy9jb154xcr41p8psrvrxl")))) ;;(build-system ocaml-build-system) ;; fails for same reason as dune. (build-system gnu-build-system) (arguments `(#:make-flags ,#~(list (string-append "ELPIDIR=3D" #$(this-package-input "coq-elpi= ") "/lib/coq/user-contrib/elpi/") (string-append "DESTDIR=3D" (assoc-ref %outputs "out")) (string-append "COQLIBINSTALL=3D" #$output "/lib/coq/user-contrib")) #:test-target "test-suite" #:phases (modify-phases %standard-phases (delete 'configure) ))) (propagated-inputs (list coq-elpi)) (inputs (list coq-core coq-stdlib)) (native-inputs (list ocaml which)) (synopsis "Hierarchy structures for the Coq proof assistant") (description "Hierarchy Builder (HB) provides high level commands to declare a hierarchy of interfaces for the Coq system. Given a structure one can develop its theory, and that theory becomes applicable to all examples of the structure. One can also declare alternat= ive interfaces, for convenience or backward compatibility, and provide glue code linking these interfaces to the structures part of the hierarchy.") (home-page "https://math-comp.github.io/") ;; MIT license (license license:expat))) (define-public coq-mathcomp-analysis (package (name "coq-mathcomp-analysis") (version "0.5.4") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/math-comp/analysis") (commit version))) (file-name (git-file-name name version)) (sha256 (base32 "1l1yaxbmqr4li8x7g51q98a6v383dnf94lw1b74ccpwqz9qybz9m")))) (build-system gnu-build-system) (arguments `( ;No rule to make target 'check'. Stop. ;; Makefile.common has no references to tests. ;; There are also no references to tests found after ;; running the following commands in the top ;; directory of the cloned repo: ;; find -type d | grep -i test ;; rg test # where rg is ripgrep ;; Checking the git log, we find: "Add test suite for ;; joins and several fixes". ;; ;; If tests are included, this quote suggests that they ;; would be part of the source files themselves, ;; and the tests would be run as part of the build ;; process. #:tests? #f #:make-flags ,#~(list (string-append "COQBIN=3D" #$(this-package-input "coq-core= ") "/bin/") (string-append "COQBININSTALL=3D" (assoc-ref %outputs "out") "/bi= n/") (string-append "COQMF_COQLIB=3D" (assoc-ref %outputs "out") "/lib/ocaml/site-lib/coq") (string-append "COQLIBINSTALL=3D" (assoc-ref %outputs "out") "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (delete 'configure) (replace 'build (lambda* (#:key make-flags #:allow-other-keys) (apply invoke "make" "build" make-flags)))))) (inputs (list coq coq-stdlib coq-mathcomp coq-mathcomp-finmap coq-mathcomp-hierarchy-builder coq-elpi coq-mathcomp-bigenough coq-core)) (native-inputs (list ocaml which)) (synopsis "Real analysis for the Coq proof assistant") (description "This repository contains an experimental library for real analysis for the Coq proof-assistant, using the Mathematical Components library.") (home-page "https://math-comp.github.io/") (license license:cecill-c))) coq-mathcomp-analysis --MP_/uvRhSCMl/XdMwbzM4kqo_=n--