From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id mLqiGQjLTmOhPgAAbAwnHQ (envelope-from ) for ; Tue, 18 Oct 2022 17:49:28 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id QMiwGQjLTmME4wAA9RJhRA (envelope-from ) for ; Tue, 18 Oct 2022 17:49:28 +0200 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 B6985998D for ; Tue, 18 Oct 2022 17:49:27 +0200 (CEST) Received: from localhost ([::1]:58918 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1okoqL-0006VO-Lw for larch@yhetil.org; Tue, 18 Oct 2022 11:49:25 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:39192) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1okop0-0006LF-Ln for guix-patches@gnu.org; Tue, 18 Oct 2022 11:48:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:54770) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1okop0-00037T-9b for guix-patches@gnu.org; Tue, 18 Oct 2022 11:48:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1okooz-0002IP-SH for guix-patches@gnu.org; Tue, 18 Oct 2022 11:48:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#58310] Temporary manifest for coq-mathcomp-analysis References: <87h70iqji2.fsf@disroot.org> In-Reply-To: <87h70iqji2.fsf@disroot.org> Resent-From: Garek Dyszel Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 18 Oct 2022 15:48:01 +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: 58310@debbugs.gnu.org Received: via spool by 58310-submit@debbugs.gnu.org id=B58310.16661080398677 (code B ref 58310); Tue, 18 Oct 2022 15:48:01 +0000 Received: (at 58310) by debbugs.gnu.org; 18 Oct 2022 15:47:19 +0000 Received: from localhost ([127.0.0.1]:53848 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1okooH-0002Fq-GA for submit@debbugs.gnu.org; Tue, 18 Oct 2022 11:47:19 -0400 Received: from knopi.disroot.org ([178.21.23.139]:56720) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1okooA-0002Fc-3m for 58310@debbugs.gnu.org; Tue, 18 Oct 2022 11:47:16 -0400 Received: from localhost (localhost [127.0.0.1]) by disroot.org (Postfix) with ESMTP id 4E60C4DCC7 for <58310@debbugs.gnu.org>; Tue, 18 Oct 2022 17:47:08 +0200 (CEST) X-Virus-Scanned: SPAM Filter at disroot.org Received: from knopi.disroot.org ([127.0.0.1]) by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024) with UTF8SMTP id ydz3tc_C6h6M for <58310@debbugs.gnu.org>; Tue, 18 Oct 2022 17:47:04 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail; t=1666107786; bh=SDdBBbR/+wVl2bZBSkakG1LERaAqvz/7HOxof/5Hbak=; h=From:To:Subject:Date; b=N+98TT+wvpv0+0NXTzOU4fr7zypXuTurrhfyItio3YCP58/4TnLeQfGLQ7NMcwf6U TyFSgDrk4ev4HhRgFaYkWG2hr69t0V/IQBaw1H+UuLGum+hGEZ39gbIHwVfOTaR8F2 5BGUg30Lccn4lLgHChXU2Yxh6/qoo/CR/kh1VJ2GI6NMYHHBAZ2S1wGDRt/X8SEpck kWMMpMZBC4UxGhscMcCl6NwkCET+kyRGZMgnE1wIKczhHGymsUcvSyJbtWYusplb8i YqUA8aGRWWEmQQVfm9wYSdvIPbIQF9yfPH+AniKUG5xYWMyl3Kp//FcC+rhJoLlO9t XoTRzWB5gAtTA== Date: Tue, 18 Oct 2022 11:42:44 -0400 Message-ID: <87y1td2l57.fsf@disroot.org> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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" Reply-to: Garek Dyszel X-ACL-Warn: , Garek Dyszel via Guix-patches From: Garek Dyszel via Guix-patches via 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=1666108168; h=from:from:sender:sender:reply-to:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: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=icY/yWkYFmRdgBr6zWCLoX6jjpThunqS4HOFc5rmOQM=; b=sJdf2MtDIrz6Bc9HgqlIqQ13vummj3IL9B5tX4PdEd/MrNIjDdczF9VPBrt5ir8JqL6UyL m+AHo4cHiPo2nd/a1D2u2MuW3RRrHZfIIRwtTNvSg6OfEGJHNO0dMfDOdOzKNHUh3hYwtf DX9O7hp59OwFhWwRmbuvrBwi/gyz6J2dOrAbT4KmY/a6V/GCccEOl/1zkX3289nt1w7bi8 vQ9UFJOaG0AzR79oSBtwETPBIghOjkaakuySsPMMVBb2yM9YfNMML8C4NiHdfSraHD0Zts F+fvfmkq7kbnQg+U0ZOXNww1PZ5J7n+kdf0Vk2r1mxPqzb68K9xdexWawMgYxQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1666108168; a=rsa-sha256; cv=none; b=QTQz5DqWkhAB4PJ5hOGPZ1VhyfW66mRd5fOXCt0GHUL3qMb5/UKvyAZRUMic7g4pZQZr9L aFY/a+UjigtGQ6s+qPkv269W+vcCBoaPLIVSvZ8Rxm34XlAoMLkmLlcLfIkq+z5DVog0co aJMSr7fuaBk0119XdyNp0gdISw5lkwfO2uK/u5Yb/C+DHlhV1M3yYC5M6yUVBO0vUJY4Wc mHCPDeT/Eb0nEw/22eDFM9/jmG13k2kGsIB8GGvMfQR2IhBVUTi/t5JL2gUc7pV5jPXy7v F/szm5oayVUMUKqJFpaHnfFcbalmCeN9MNJnVzeD9trPqKlf0zs43eXQpLgSOQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=N+98TT+w; dmarc=pass (policy=none) header.from=gnu.org; 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: -3.22 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=N+98TT+w; dmarc=pass (policy=none) header.from=gnu.org; 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: B6985998D X-Spam-Score: -3.22 X-Migadu-Scanner: scn0.migadu.com X-TUID: hIsyA47zt4wz Since the above patch set does not correctly build with Coq 8.16, here are a manifest file, a channels file, and a package file to get us through. These files rely on Coq 8.15.2. I didn't try to clean these files up or anything. They do work for me, though, until we can figure out how to build coq-mathcomp-analysis for Coq 8.16. I tested it with Emacs Proof General. If all files are in the same folder, they can be used by running the following. (Note also: to get a valid channel for the channels.scm file, we have to create a dummy git repository.) $ mkdir mathcomp-extra-packages && cp coq-mathcomp-analysis.scm ./test $ cd test $ git init $ git add coq-mathcomp-analysis.scm $ git commit "random commit name" $ cd ../ $ guix time-machine -C ./channels.scm\ -- shell -m guix-manifest.scm -- emacs ./ (One can omit "-- emacs ./" if they just want the packages available, but want to use a different editor.) A final note is that if Emacs does not detect the presence of coq-mathcomp-analysis, it could befixed with the following local variables. #+begin_src coq (* Local Variables: *) (* mode: coq *) (* eval: (setq coq-prog-name "coqtop") *) (* eval: (setq coq-compiler "coqc") *) (* eval: (setq coq-dependency-analyzer "coqdep") *) (* End: *) #+end_src coq-mathcomp-analysis.scm --8<---------------cut here---------------start------------->8--- ;;; 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 (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 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 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 version-control)) ;; This manifest builds coq-mathcomp-analysis for Coq 8.15.2. ;;; OCaml (define-public ocaml-elpi (package (name "ocaml-elpi") ;; For more information on which version works with Coq 8.15, ;; see the relevant issue: ;; https://github.com/math-comp/hierarchy-builder/issues/297 ;; Here we use ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15) ;; ;; The package ocaml-elpi@1.16.5 appears to require a different ;; build process. (version "1.15.2") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/LPCIC/elpi") (commit (string-append "v" version)) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy")))) (build-system dune-build-system) (arguments `(#:test-target "tests")) (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 implements a variant of =CE=BBProlog enriched with Constraint Handling Rules, a programming language well suited to manipulate syntax trees with binders. ELPI is designed to be embedded into larger applications written in OCaml as an extension language. It comes with an API to drive the interpreter and with an FFI for defining built-in predicates and data types, as well as quotations and similar goodies that are handy to adapt the language to the host application. This package provides both a command line interpreter (elpi) and a library to be linked in other applications (eg by passing -package elpi to ocamlfind). The ELPI programming language has the following features: @itemize @item Native support for variable binding and substitution, via an Higher Order Abstract Syntax (HOAS) embedding of the object language. The programmer does not need to care about technical devices to handle bound variables, like De Bruijn indices. @item Native support for hypothetical context. When moving under a binder one can attach to the bound variable extra information that is collected when the variable gets out of scope. For example when writing a type-checker the programmer needs not to care about managing the typing context. @item Native support for higher order unification variables, again via HOAS. Unification variables of the meta-language (=CE=BBProlog) can be reused to represent the unification variables of the object language. The programmer does not need to care about the unification-variable assignment map and cannot assign to a unification variable a term containing variables out of scope, or build a circular assignment. @item Native support for syntactic constraints and their meta-level handling rules. The generative semantics of Prolog can be disabled by turning a goal into a syntactic constraint (suspended goal). A syntactic constraint is resumed as soon as relevant variables gets assigned. Syntactic constraints can be manipulated by constraint handling rules (CHR). @item Native support for backtracking. To ease implementation of search. @item The constraint store is extensible. The host application can declare non-syntactic constraints and use custom constraint solvers to check their consistency. @item Clauses are graftable. The user is free to extend an existing program by inserting/removing clauses, both at runtime (using implication) and at \"compilation\" time by accumulating files. @end itemize ELPI is free software released under the terms of LGPL 2.1 or above.") (license license:lgpl2.1))) ;; Requires python-jsonschema version 4.6.0 to run tests. ;; See https://github.com/ahrefs/atd/issues/306 (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) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "10fgahdigrl01py0k0q2d6a60yps38q96dxhjnzm9jz4g931716l")))) (build-system dune-build-system) (arguments `(;; The dependency python-jsonschema needs to be at ;; v4.6 in order for the python tests to pass. ;; See https://github.com/ahrefs/atd/issues/306 for more info ;; on that. ;;#:tests? #f #: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 for the ocaml packag= e. ;; 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 python-pypa-build python-jsonschema-4.15 python-flake8 python-mypy python-pytest)) (home-page "https://github.com/ahrefs/atd") (synopsis "Parser for the ATD data format description language") (description "ATD is the OCaml library providing a parser for the ATD language and various utilities. ATD stands for Adjustable Type Definitions in reference to its main property of supporting annotations that allow a good fit with a variety of data formats.") ;; Modified BSD license (license (license:non-copyleft "LICENSE.md")))) (define-public ocaml-ansiterminal (package (name "ocaml-ansiterminal") (version "0.8.5") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/Chris00/ANSITerminal") (commit version) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "052qnc23vmxp90yympjz9q6lhqw98gs1yvb3r15kcbi1j678l51h")))) (build-system dune-build-system) (arguments `(#:test-target "tests")) (home-page "https://github.com/Chris00/ANSITerminal") (synopsis "Basic control of ANSI compliant terminals and the windows shell") (description "ANSITerminal is a module allowing to use the colors and cursor movements on ANSI terminals.") ;; Variant of the GPL3 which permits ;; static and dynamic linking when producing binary files. ;; In other words, it allows one to link to the library ;; when compiling nonfree software. (license (license:non-copyleft "LICENSE")))) ;;; Coq (define-public coq-elpi (package (name "coq-elpi") ;; For more information on which version works with Coq 8.15, ;; see the relevant issue: ;; https://github.com/math-comp/hierarchy-builder/issues/297 ;; Here we use ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15) (version "1.14.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/LPCIC/coq-elpi") (commit (string-append "v" version)) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp")))) (build-system gnu-build-system) (arguments `(#: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 "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) (add-before 'build 'remove-extra-src-file (lambda* (#:key outputs #:allow-other-keys) ;; Remove the useless line ;; "src/META.coq-elpi" ;; in file _CoqProject. ;; The file src/META.coq-elpi does not exist in ;; the repository, ;; so this line inhibits compilation unnecessarily. (invoke "sed" "-i" "s|src/META.coq-elpi||g" "_CoqProject"))) (replace 'check ;; Error when running the "check" phase: ;; "make: *** No rule to make target 'check'. Stop." (lambda* (#:key tests? make-flags #:allow-other-keys) (when tests? (apply invoke "make" "test" make-flags))))))) (inputs (list python)) (propagated-inputs (list ocaml ocaml-stdlib-shims ocaml-elpi ocaml-zarith coq-core coq-stdlib)) (home-page "https://github.com/LPCIC/coq-elpi") (synopsis "Elpi extension language for Coq") (description "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way 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, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in =CE=BBProlog. E.g. @code{{{nat}}} is expanded to the type name of natural numbers, or @code{{{A -> B}}} to the representation of a product by unfolding the @code{->} notation. Finally it provides a way to define new vernacular commands 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.15, ;; see the relevant issue: ;; https://github.com/math-comp/hierarchy-builder/issues/297 ;; Here we use ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 + ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15) (version "1.3.0") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/math-comp/hierarchy-builder") (commit (string-append "v" version)) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc")))) (build-system gnu-build-system) (arguments `(#:test-target "test-suite" #: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 "DESTDIR=3D" (assoc-ref %outputs "out")) (string-append "ELPIDIR=3D" #$(this-package-input "ocaml-el= pi") "/lib/ocaml/site-lib/elpi") (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))) ;; (replace 'check ;; (lambda* (#:key tests? make-flags #:allow-other-keys) ;; (when tests? ;; (apply invoke "make" "test-suite" make-flags)))) ))) (inputs (list coq coq-core coq-mathcomp which ocaml coq-elpi ocaml-elpi)) (synopsis "Hierarchy structures for the Coq proof assistant") (description "Hierarchy Builder (HB) provides high level commands to declare a hierarchy of algebraic structure (or interfaces if you prefer the glossary of computer science) for the Coq system. Given a structure one can develop its theory, and that theory becomes automatically applicable to all the examples of the structure. One can also declare alternative interfaces, for convenience or backward compatibility, and provide glue code linking these interfaces to the structures part of the hierarchy. HB commands compile down to Coq modules, sections, records, coercions, canonical structure instances and notations following the packed classes discipline which is at the core of the Mathematical Components library. All that complexity is hidden behind a few concepts and a few declarative Coq commands.") (home-page "https://math-comp.github.io/") ;; MIT license (license license:expat))) (define-public coq-mathcomp-finmap (package (name "coq-mathcomp-finmap") (version "1.5.2") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/math-comp/finmap") (commit version) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh")))) (build-system gnu-build-system) (arguments `( ;"No rule to make target 'check'." ;; No tests supplied in Makefile.common. ;; The project doesn't appear to have plans to include tests in ;; the future. #:tests? #f #:make-flags (list (string-append "COQLIBINSTALL=3D" (assoc-ref %outputs "out") "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (delete 'configure)))) (inputs (list coq coq-stdlib coq-mathcomp which)) (synopsis "Finite sets and finite types for coq-mathcomp") (description "This library is an extension of coq-mathcomp which supports finite se= ts and finite maps on choicetypes (rather than finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set libary, which will eventually be used to subsume notations for finite sets.") (home-page "https://math-comp.github.io/") (license license:cecill-b))) (define-public coq-mathcomp-bigenough ;; On the homepage, it is mentioned that coq-mathcomp-bigenough ;; is going to be obsolete sometime in the near future. ;; This package was included because of the following error, ;; encountered while building coq-mathcomp-analysis: ;; "Warning: in file theories/altreals/realseq.v, library ;; mathcomp.bigenough.bigenough is required and has not been ;; found in the loadpath!" ;; So added https://github.com/math-comp/bigenough. (package (name "coq-mathcomp-bigenough") (version "1.0.1") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/math-comp/bigenough") (commit version) (recursive? #t))) (file-name (git-file-name name version)) (sha256 (base32 "02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw")))) (build-system gnu-build-system) (arguments `( ;"No rule to make target 'test'. Stop." ;; No references to tests in Makefile.common. ;; It doesn't appear as though tests will be included ;; by the packaged project in the future. #:tests? #f #:make-flags ,#~(list (string-append "COQBIN=3D" #$(this-package-input "coq-core= ") "/bin/") (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)))) (propagated-inputs (list coq coq-core coq-mathcomp which)) (home-page "https://math-comp.github.io/") (synopsis "Small library to do epsilon - N reasoning") (description "The package contains a package to reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as @code{bigenough} will be subsumed by the near tactics. The formalization is based on the Mathematical Components library.") (license license:cecill-b))) (define-public coq-mathcomp-analysis (package (name "coq-mathcomp-analysis") ;;(version "0.5.3") (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 ;; hash for v0.5.3 ;;"16bv2kxm6nrgfm9lp88sls1vqs26d4m3fxbccmy328ak5srcbn6l" ;; hash for v0.5.4 "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 ;; 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 "DESTDIR=3D" (assoc-ref %outputs "out")) (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) (apply invoke "make" make-flags) ))))) (inputs (list coq coq-stdlib coq-mathcomp coq-mathcomp-finmap coq-mathcomp-hierarchy-builder coq-elpi coq-mathcomp-bigenough coq-core which python)) (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))) ;;; Python ;; (define-public python-import-everything ;; (package ;; (name "python-import-everything") ;; (version "0.0.1") ;; (source (origin ;; (method url-fetch) ;; (uri (pypi-uri "import-everything" version)) ;; (sha256 ;; (base32 ;; "1cq45i421bksg2lwwf5xddp30v0z95qzh2g6dxi1ky989lgxvlv3")))) ;; (build-system python-build-system) ;; (inputs (list python python-pypa-build python-pytest)) ;; (arguments ;; (substitute-keyword-arguments (package-arguments python-jsonschema) ;; ((#:phases phases) ;; #~(modify-phases #$phases ;; (replace 'build ;; (lambda _ ;; ;; ZIP does not support timestamps befo= re 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" #$output whl)= ))) ;; )))) ;; (home-page "https://github.com/profMagija/everything") ;; (synopsis "A module containing everything") ;; (description "This package provides a module containing everything") ;; (license #f))) (define-public python-version ;; No version tags available; just using bare commit instead. (let ((commit "5232eea250ab72cc5cb72b0b75efb35d2192b906")) (package (name "python-python-version") (version "0.0.2") (source (origin (method git-fetch) (uri (git-reference (url "https://gitlab.com/halfak/python_version") (commit commit))) (sha256 (base32 "0w210559ypdynlj9yn40m9awzkaknwrf682i99hswl7h66sdgh0h")))) (build-system python-build-system) (home-page "https://gitlab.com/halfak/python_version") (synopsis "Provides a simple utility for checking the python version.= ") (description "This package provides a simple utility for checking the python vers= ion.") ;; MIT License (license license:expat)))) (define-public python-editables (package (name "python-editables") (version "0.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/pfmoore/editables") (commit version))) (sha256 (base32 "1gbfkgzmrmbd4ycshm09fr2wd4f1n9gq7s567jgkavhfkn7s2pn1")))) (build-system python-build-system) (home-page "https://github.com/pfmoore/editables") (synopsis "Editable installations") (description "Editable installations") (license license:expat))) (define-public python-pluggy-1.0 (package (inherit python-pluggy) (name "python-pluggy-1.0") (version "1.0.0") (source (origin ;; Won't build from github tarballs, throws error: ;; "LookupError: setuptools-scm was unable to detect version = for '/tmp/guix-build-python-pluggy-1.0-1.0.0.drv-0/source'." (method url-fetch) (uri (pypi-uri "pluggy" version)) (sha256 (base32 "0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922")))) (inputs (list python python-pypa-build python-pytest python-setuptools-scm python-setuptools python-wheel)))) ;; (define-public python-hatch-vcs ;; ;; Tags are messed up; just use the commit itself. ;; (let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2")) ;; (package ;; (name "python-hatch-vcs") ;; (version "0.2.0") ;; (source (origin ;; (method git-fetch) ;; (uri (git-reference ;; (url "https://github.com/ofek/hatch-vcs") ;; (commit commit))) ;; (sha256 ;; (base32 ;; "0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05"= )))) ;; (build-system python-build-system) ;; (inputs (list python ;; python-pypa-build ;; python-pathspec-0.10.1 ;; python-pluggy-1.0 ;; python-editables ;; python-pytest ;; git)) ;; (propagated-inputs (list python-hatchling-bootstrap python-setupto= ols-scm-7)) ;python-setuptools-scm-6.4 minimum ;; (arguments ;; (substitute-keyword-arguments (package-arguments python-jsonschem= a) ;; ((#:phases phases) ;; #~(modify-phases #$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")))))))) ;; (home-page "") ;; (synopsis "Hatch plugin for versioning with your preferred VCS") ;; (description "Hatch plugin for versioning with your preferred VCS") ;; (license #f)))) (define-public python-setuptools-scm-7 ;; Another broken python release. Ugh. (let ((commit "c4d37004ab0a16c2cacdc58ef06b36956db02a9f")) (package (name "python-setuptools-scm") (version "7.0.5") (source (origin ;; Won't build with git. Fails with error: ;; "ERROR Backend subproccess exited when trying to invoke ;; get_requires_for_build_wheel" (method url-fetch) (uri (pypi-uri "setuptools_scm" version)) (sha256 (base32 "0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3")) )) (build-system python-build-system) (propagated-inputs (list python-importlib-metadata python-packaging python-setuptools python-tomli python-typing-extensions)) (native-inputs (list python python-pypa-build python-pytest python-virtualenv git-minimal mercurial)) (home-page "https://github.com/pypa/setuptools_scm/") (synopsis "the blessed package to manage your versions by scm tags") (description "the blessed package to manage your versions by scm tags= ") (license license:expat)))) (define-public python-pprintpp ;; Another broken python version (let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0")) (package (name "python-pprintpp") (version "0.3.0") (source (origin ;; No version given in the github repo ;; https://github.com/wolever/pprintpp. (method git-fetch) (uri (git-reference (url "https://github.com/wolever/pprintpp") (commit commit))) (sha256 (base32 "0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li")) )) (inputs (list python python-pypa-build python-pytest python-hypothesis python-setuptools python-wheel python-nose python-parameterized)) (build-system python-build-system) (arguments (substitute-keyword-arguments (package-arguments python-jsonschema) ((#:phases phases) #~(modify-phases #$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 "A drop-in replacement for pprint that's actually pretty") (description "This package provides a drop-in replacement for pprint that's actua= lly pretty") (license license:bsd-3)))) (define-public python-icdiff (package (name "python-icdiff") (version "2.0.5") (source (origin ;; (method url-fetch) ;; (uri (pypi-uri "icdiff" version)) ;; (sha256 ;; (base32 ;; "1bhbcc8mqvhdswfarl12x57yyzpw7dnkhsfv5fhy1ds8irr4plim")) (method git-fetch) (uri (git-reference (url "https://github.com/jeffkaufman/icdiff") (commit (string-append "release-" version)))) (sha256 (base32 "14gr9j2h7sfw47pwfzspm4zinywhqmzm4a0qz5c2k9wbixz120a4")) )) (build-system python-build-system) (home-page "http://www.jefftk.com/icdiff") (synopsis "improved colored diff") (description "improved colored diff") (license #f))) (define-public python-pytest-icdiff (package (name "python-pytest-icdiff") (version "0.6") (source (origin ;; Tests fail in git version, but not in pypi version. (method url-fetch) (uri (pypi-uri "pytest-icdiff" version)) (sha256 (base32 "1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8")))) (build-system python-build-system) (propagated-inputs (list python python-pypa-build python-icdiff python-pprintpp python-pytest)) (home-page "https://github.com/hjwp/pytest-icdiff") (synopsis "use icdiff for better error messages in pytest assertions") (description "use icdiff for better error messages in pytest assertions= ") (license #f))) (define-public python-hatch-fancy-pypi-readme (package (name "python-hatch-fancy-pypi-readme") ;;(version "22.3.0") (version "22.8.0") (source (origin (method url-fetch) (uri (pypi-uri "hatch_fancy_pypi_readme" version)) (sha256 (base32 ;;"1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx" "0sn2wsfbpsbf2mqhjvw62h1cfy5mz3d7iqyqvs5c20cnl0n2i4fs")))) (build-system python-build-system) (propagated-inputs (list python-hatchling-bootstrap python-tomli python-typing-extensions)) (native-inputs (list python python-pypa-build python-pathspec-0.10.1 python-pluggy-1.0 python-editables python-hatchling-bootstrap 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 any Guix 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 _ (invoke "pytest" "-vv")))))) (home-page "") (synopsis "Fancy PyPI READMEs with Hatch") (description "Fancy PyPI READMEs with Hatch") (license #f))) ;; (define-public python-jsonschema-4.6 ;; (package ;; (inherit python-jsonschema) ;; (name "python-jsonschema-4.6") ;; (version "4.15.0") ;; (source (origin ;; (method url-fetch) ;; (uri (pypi-uri "jsonschema" version)) ;; (sha256 ;; (base32 ;; "07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11"))= )) ;; (native-inputs (list python-pypa-build ;; python-twisted ;; python-hatchling-bootstrap ;; python-pathspec ;; 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 ;; python-setuptools-scm-7)) ;; (arguments ;; (substitute-keyword-arguments (package-arguments python-jsonschema-= next) ;; )))) (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 python-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 python-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 python-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-bootstrap (package (name "python-hatchling-bootstrap") (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 ;;"1q25kqw71g8mjwfjz9ph0iigdqa26zzxgmqm0v0bp0z1j8rcl237" ;;"1yqkwck2aihfdm9ljv5q4nygmmqyp35xwyp8lqn2f4vq9p6njq3c" "0ahx62w711a2vnb91ahqxrw8yi0gq0kfch3fk6akzngd13376czj" ;; g= ithub weirdness. )))) ;; 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-pypa-build python-editables python-importlib-metadata python-version python-packaging-next python-pathspec-0.10.1 python-pluggy-1.0 ;TODO: Not detected by pytest? python-tomli python-platformdirs)) (build-system python-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.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 "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-bootstrap python-tomli python-platformdirs python-rich python-tomli-w)) (build-system python-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 python-build-system) (inputs (list python-pypa-build python-pathspec-0.10.1 python-pluggy-1.0 python-editables git python-hatchling-bootstrap 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"))))))) ;) (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 python-build-system) (propagated-inputs (list python-pypa-build python-icdiff python-pprintp= p)) (native-inputs (list python-pytest)) (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 ;; "1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx"))= )) ;; (build-system python-build-system) ;; (propagated-inputs (list python-tomli python-typing-extensions)) ;; (native-inputs (list python-pypa-build ;; python-pathspec ;; python-pluggy-1.0 ;; python-editables ;; python-hatch ;; python-hatchling-bootstrap ;; 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 doe= s this, ;; ;; 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= from ;; ;; 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 s= tyling ;; 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 ;; old pypi hash ;; ;;"07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11" ;; new pypi hash "08sbw5fn19vn8x7c216gkczyzd575702yx2vmqdrgxpgfvq5jl0n")))) (native-inputs (list python-pypa-build python-twisted python-hatch python-hatchling-bootstrap 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"))) coq-mathcomp-analysis --8<---------------cut here---------------end--------------->8--- channels.scm --8<---------------cut here---------------start------------->8--- ;;; 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 (list ;; guix (channel (name 'guix) ;;(url "https://git.savannah.gnu.org/git/guix.git") (url "https://github.com/guix-mirror/guix") (introduction (make-channel-introduction "9edb3f66fd807b096b48283debdcddccfea34bad" (openpgp-fingerprint "BBB0 2DDF 2CEA F6A8 0D1D E643 A2A0 6DF2 A33A 54FA"))) (commit "9f391b90faca02ca97c5018d6c095ecdaa1a94a7")) ;; The commit ;; just before the upgrade to Coq 8.16! ;; The channel that contains coq-mathcomp-analysis package ;; definitions.=20 (channel (name 'coq-mathcomp-analysis-packages) ;;(url ;;"/home/chips/home/code/coq-my-theories/mathcomp-extra-packages" (url "./mathcomp-extra-packages"))) --8<---------------cut here---------------end--------------->8--- guix-manifest.scm --8<---------------cut here---------------start------------->8--- ;;; 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 (use-modules (guix packages) (gnu packages coq) (coq-mathcomp-analysis)) (packages->manifest (list coq coq-stdlib coq-mathcomp coq-mathcomp-finmap c= oq-mathcomp-hierarchy-builder coq-elpi coq-mathcomp-bigenough coq-core coq-= mathcomp-analysis)) --8<---------------cut here---------------end--------------->8---