[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[Garek Dyszel via Guix-patches via]

* gnu/packages/ocaml.scm (ocaml-elpi)
---
  gnu/packages/ocaml.scm | 102 +++++++++++++++++++++++++++++++++++++++++
  1 file changed, 102 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 0e8e5b2..59f324e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@
  ;;; Copyright © 2021 Sarah Morgensen <iskarian@mgsn.dev>
  ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com>
  ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
  ;;;
  ;;; This file is part of GNU Guix.
  ;;;
@@ -8741,3 +8742,104 @@ (define-public ocaml-bibtex2html
      (description "This package allows you to produce, from a set of
  bibliography files in BibTeX format, a bibliography in HTML format.")
      (license license:gpl2)))
+
+(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
+     `(;; When running phase 'check', fails with the error:
+       ;; Error: Don't know about directory test specified on the
+       ;; command line!
+       ;;
+       ;; The "make tests" command requires replacing /usr/bin/time
+       ;; with the location of the input package "time".
+       #:tests? #f))
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atdgen
+                             ocaml-atdts
+                             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 λProlog Interpreter")
+    (description
+     "ELPI implements a variant of λProlog 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:
+
+- 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.
+
+- 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.
+
+- Native support for higher order unification variables, again via
+HOAS.  Unification variables of the meta-language (λProlog) 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.
+
+- 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).
+
+- Native support for backtracking.  To ease implementation of search.
+
+- The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+- 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.
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))
+
-- 
2.37.2

[bug#57540] [PATCH 1/6] gnu: Add ocaml-atd.

[Garek Dyszel via Guix-patches via]

* gnu/packages/ocaml.scm (ocaml-atd)
---
  gnu/packages/ocaml.scm | 35 +++++++++++++++++++++++++++++++++++
  1 file changed, 35 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 59f324e..c8ffef5 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8843,3 +8843,38 @@ (define-public ocaml-elpi
  ELPI is free software released under the terms of LGPL 2.1 or above.")
      (license license:lgpl2.1)))

+(define-public ocaml-atd
+  (package
+    (name "ocaml-atd")
+    (version "2.10.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/ahrefs/atd/releases/download/" 
version
+                    "/atdts-" version ".tbz"))
+              (sha256
+               (base32
+                
"1609hlj2snpvxnmmg892ic01hv3chdhfmsd2khdw9np9lh4p9lkp"))))
+    (build-system dune-build-system)
+    (arguments
+     `(;; Error: Don't know about directory test specified on the 
command line!
+       #:tests? #f))
+    (propagated-inputs (list ocaml-menhir
+                             ocaml-easy-format
+                             ocaml-odoc
+                             ocaml-re
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson
+                             ocaml-cmdliner
+                             ocaml-menhir))
+    (native-inputs (list ocaml-alcotest python))
+    (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"))))
--
2.37.2

[bug#57540] [PATCH 2/6] gnu: Add ocaml-ansiterminal.

[Garek Dyszel via Guix-patches via]

* gnu/packages/ocaml.scm (ocaml-ansiterminal)
---
  gnu/packages/ocaml.scm | 31 +++++++++++++++++++++++++++++++
  1 file changed, 31 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index c8ffef5..43c19c0 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8878,3 +8878,34 @@ (define-public ocaml-atd
  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
+     `( ;Error: Don't know about directory test specified on the
+       ;; command line!
+       #:tests? #f))
+    (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"))))
-- 
2.37.2

[bug#57540] [PATCH 3/6] gnu: Add coq-elpi.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-elpi)
---
  gnu/packages/coq.scm | 74 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 74 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df..5a37432 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -685,3 +685,77 @@ (define-public coq-stdpp
  @end itemize")
      (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
      (license license:bsd-3)))
+
+(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="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input 
"ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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.
+                      ;; It does not affect
+                      ;; the success of compliation.
+                      (invoke "sed" "-i" "s|src/META.coq-elpi||g"
+                              "_CoqProject")
+                      #t))
+                  (replace 'check
+                    (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-1.15
+                             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 λProlog 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 λProlog.  E.g.
+`{{nat}}` is expanded to the type name of natural numbers, or `{{A ->
+B}}` to the representation of a product by unfolding the `->`
+notation.  Finally it provides a way to define new vernacular commands
+and new tactics.")
+    (license license:lgpl2.1)))
-- 
2.37.2

[bug#57540] [PATCH 4/6] gnu: Add coq-mathcomp-hierarchy-builder.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder)
---
  gnu/packages/coq.scm | 75 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 75 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5a37432..bb4788a 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -759,3 +759,78 @@ (define-public coq-elpi
  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
+     `(#:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") 
"/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input 
"ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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-1.14
+                  ocaml-elpi-1.15))
+    (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)))
-- 
2.37.2

[bug#57540] [PATCH 5/6] gnu: Add coq-mathcomp-finmap.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-finmap)
---
  gnu/packages/coq.scm | 35 +++++++++++++++++++++++++++++++++++
  1 file changed, 35 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bb4788a..f0aa233 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -834,3 +834,38 @@ (define-public coq-mathcomp-hierarchy-builder
      (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.
+       #:tests? #f
+       #:make-flags (list (string-append "COQLIBINSTALL="
+                                         (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 sets
+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)))
-- 
2.37.2

[bug#57540] [PATCH 6/6] gnu: Add coq-mathcomp-bigenough and coq-mathcomp-analysis.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-bigenough coq-mathcomp-analysis)
---
  gnu/packages/coq.scm | 105 +++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 105 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index f0aa233..680c2fa 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -869,3 +869,108 @@ (define-public coq-mathcomp-finmap
  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.
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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 `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")
+    (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
+                
"16bv2kxm6nrgfm9lp88sls1vqs26d4m3fxbccmy328ak5srcbn6l"))))
+    (build-system gnu-build-system)
+    (arguments
+     `( ;No tests were supplied with this library:
+       ;; No rule to make target 'check'. Stop.
+       ;; Makefile.common has no references to tests at all
+       ;; (yet).
+       #:tests? #f
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input 
"coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") 
"/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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-1.14
+                  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)))
-- 
2.37.2

[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[Julien Lepiller]

Hi Garek,

thanks for the patches! As I understand it, these patches introduce 8
new packages, but I count only 7 (with this one which didn't make it as
a part of the series). Could you split the last patch, so each new
package has its own patch?

Also, some points in your patches:

For "Don't know about directory test", you can try with an argument:
#:test-target "some-dir". This directory is the directory where tests
are located. If there is no single directory, you can try
#:test-target "."

Descriptions should use our subset of texinfo. Basically, lists should
look like:

@itemize
@item foo
@item bar
@end itemize

and you can use @file, @code, etc as you see fit (to replace markdown's
"`").

Whenever possible, we try not to rely on github tarballs, so it'd be
best to use a git-reference in all your patches :)

In coq-elpi:

> +                      ;; Remove the useless line
> +                      ;; "src/META.coq-elpi"
> +                      ;; in file _CoqProject.
> +                      ;; It does not affect
> +                      ;; the success of compliation.

should be "compilation". And then I wonder why you need that at all, if
it doesn't change compilation result?

> +                      #t))

Please don't use #t at the end of phases anymore.

> +                  (replace 'check

The gnu-build-system already runs "make test", doesn't it? Why do you
need to replace this phase?


In coq-mathcomp-hierarchy-builder:

> +                  (replace 'check

Instead of replacing this phase, maybe try #:test-target "test-suite"

> +       ;; Makefile.common has no references to tests at all
> +       ;; (yet).

If that means that future versions will have tests (for instance if
master has tests), maybe this should say it more explicitely.

Once you fix all this, could you send a v2 series? Thank you!

[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[Ludovic Courtès]

Hi Julien,

Julien Lepiller <julien@lepiller.eu> skribis:

> thanks for the patches! As I understand it, these patches introduce 8
> new packages, but I count only 7 (with this one which didn't make it as
> a part of the series). Could you split the last patch, so each new
> package has its own patch?

Could you take a look at v2 of this patch series?

  https://issues.guix.gnu.org/57540

TIA!

Ludo’.

[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[Julien Lepiller]

Le Sat, 24 Sep 2022 15:05:18 +0200,
Ludovic Courtès <ludo@gnu.org> a écrit :

> Hi Julien,
> 
> Julien Lepiller <julien@lepiller.eu> skribis:
> 
> > thanks for the patches! As I understand it, these patches introduce
> > 8 new packages, but I count only 7 (with this one which didn't make
> > it as a part of the series). Could you split the last patch, so
> > each new package has its own patch?  
> 
> Could you take a look at v2 of this patch series?
> 
>   https://issues.guix.gnu.org/57540
> 
> TIA!
> 
> Ludo’.

Haha! This went under my radar.

I pushed a part of this series on master as
8371ad64083970f68c8e1dd5f04b1f10d9cf029d to
d46e955d93692f3c4b5387aaf709a2e5e43b57b4.

These were: ocaml-ansiterminal, coq-mathcomp-{finmap,bigenough},
python-version, python-editables and python-icdiff.

I made a few changes esp. to extend descriptions, remove a few comments
that were unneeded. I also removed the recursive? flag for
mathcomp packages since it was not needed. This already took quite a bit
of time because patches were malformed (not your fault, but somehow the
subject line was always incorrect) and in a seemingly random order.
Also, they almost all have conflicts with current master.

I'm a bit too tired to figure out the rest. Could you rebase the
remaining patches on top of master? Please make sure that when applying
a patch, it is possible to build the package without applying more
patches. So, make sure dependencies are added before dependents. If you
lack inspiration, the README is often a good place to use.

A few notes on the patches:

The description is often a single line, a copy of the synopsis, or
missing a final point. In the description of ocaml-elpi, it says (last
line): "ELPI is free software released under the terms of LGPL 2.1 or
above.". No need to repeat the license here. Also, this means that the
license should be lgpl2.1+, instead of plain lgpl2.1.

For python packages, I see you add python to the inputs. Why is that?
The python-build-system already provides python.

python-hatchling should go in python-build instead of xyz.

For jsonschema, please don't change the name of the package. It looks
like python-jsonschema-next (4.5.1) does not have any dependent, so
updating this package instead might be better than adding a new one,
wdyt?

Thanks!

[bug#57540] [RFC PATCH v2 01/19] gnu: Add ocaml-elpi.

[Garek Dyszel via Guix-patches via]

Hi Julien,

Thank you for your thoughtful suggestions! All patches are now split such that each package has its own patch.

* Quickies
> And then I wonder why you need that at all, if it doesn't change
> compilation result?
The file src/META.coq-elpi does not exist in the source tree. I changed the comment; hopefully it's less ambiguous now.

> Please don't use #t at the end of phases anymore.
Thanks for catching this! It's removed.

>  Instead of replacing this phase, maybe try #:test-target "test-suite"
This worked, thanks!

> If that means that future versions will have tests (for instance if
> master has tests), maybe this should say it more explicitely.
It looks like coq-mathcomp-analysis has no tests and no plans to include any tests in the traditional sense. I changed the comment to reflect that.

* Other changes
For all the ocaml packages, using #:test-target as suggested with the appropriate directory worked. There still remain three packages without tests, but tests were not supplied with those three.

I had to add about 10 python packages in order to get the tests for ocaml-atd to pass.

Some packages (python-pluggy-1.0, python-jsonschema-4.15, python-setuptools-scm-7) are present already in the Guix tree  were required by the ocaml-atd tests.

Is there a better way to include those packages without sending this patch through core-updates?

Lists should now be formatted with @itemize (assuming I didn't miss any!).

We now use git-references for most packages. In cases where git-references were not used, they were python packages. The tests with the PyPi versions passed, but using the git repository for the same package yielded failing tests. 

* Remaining issues
This set of patches still is not ready to be merged; python-hatchling breaks Guix. The upstream hash differed this afternoon from a "guix hash -rx ." run from this morning, though the commit we are building from hasn't changed. The command "pytest -vv" in phase "check" fails with: "ERROR Missing dependencies: pluggy>=1.0.0". It seems that python-pluggy-1.0 built correctly, so maybe it is just not specified correctly in the inputs for python-hatchling?

What do you think?

Thanks again for the help!
Garek

* gnu/packages/ocaml.scm (ocaml-elpi): New variable.
---
 gnu/packages/ocaml.scm | 96 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 2fd519ca41..c4fa05b934 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@
 ;;; Copyright © 2021 Sarah Morgensen <iskarian@mgsn.dev>
 ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com>
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -8774,3 +8775,98 @@ (define-public ocaml-guile
      "The OCaml guile library provides high-level OCaml bindings to GNU Guile
 3.0, supporting easy interop between OCaml and GNU Guile Scheme.")
     (license license:gpl3+)))
+
+(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 λProlog Interpreter")
+    (description
+     "ELPI implements a variant of λProlog 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 (λProlog) 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)))
-- 
2.37.2

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[zimoun]

Hi Garek,

Thanks for your contribution.  But in the current state, it is far from
being included because too much manual work is required just to apply
the series.

For instance the series reads,

 [RFC PATCH v2 01/19] gnu: Add ocaml-elpi.
 [RFC PATCH v2 02/19] gnu: Add ocaml-atd.
 [RFC PATCH v2 03/19] gnu: Add ocaml-ansiterminal.
 [RFC PATCH v2 04/19] gnu: Add coq-elpi.
 [RFC PATCH v2 05/19] gnu: Add coq-mathcomp-hierarchy-builder.
 [RFC PATCH v2 06/19] gnu: Add coq-mathcomp-finmap.
 [RFC PATCH v2 07/19] gnu: Add coq-mathcomp-bigenough.
 [RFC PATCH v2 08/19] gnu: Add coq-mathcomp-analysis.
 [RFC PATCH v2 09/19] gnu: Add python-version.
 [RFC PATCH v2 10/19] gnu: Add python-hatchling.
 [RFC PATCH v2 11/19] gnu: Add python-hatch-vcs.
 [RFC PATCH v2 12/19] gnu: Add python-hatch-fancy-pypi-readme.
 [RFC PATCH v2 13/19] gnu: Add python-pprintpp.
 [RFC PATCH v2 14/19] gnu: Add python-icdiff.
 [RFC PATCH v2 15/19] gnu: Add python-pytest-icdiff.
 [RFC PATCH v2 16/19] gnu: Add python-editables.
 [RFC PATCH v2 17/19] gnu: Add python-pluggy-1.0.
 [RFC PATCH v2 18/19] gnu: Add python-setuptools-scm-7.
 [RFC PATCH v2 19/19] gnu: Add python-jsonschema-4.15.

where the logic about the order is not obvious; for example,

  PATCH 04 (coq-elpi)  depends on PATCH 01 (ocaml-elpi)
  PATCH 02 (ocaml-atd) depends on PATCH 19 (python-jsonschema-4.15)

The usual order is to be able to apply (build and run) the patch in
order.  It means coq-elpi must be the last (19/19).


On Sat, 24 Sep 2022 at 20:39, Julien Lepiller <julien@lepiller.eu> wrote:

> I'm a bit too tired to figure out the rest. Could you rebase the
> remaining patches on top of master? Please make sure that when applying
> a patch, it is possible to build the package without applying more
> patches. So, make sure dependencies are added before dependents. If you
> lack inspiration, the README is often a good place to use.

Yes, please Garek, make sure that when applying in order one patch after
the other, then the command ’make’ should not complain about some
missing definition.


I have tried to clean the mess but I give up for now. :-)  It would be
much easier if the series provides,

 1. the Git commit against which revision these patches apply
    (see the option --base of git-format-patch)

 2. the correct dependency order of the patches


Cheers,
simon

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[Garek Dyszel via Guix-patches via]

Hi Julien and simon,

I planned to write back yesterday but had to run out the door
unexpectedly.

At 18:52 2022-09-26 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
> For instance the series reads, ... where the logic about the order is
> not obvious

The logic was essentially adding dependencies in reverse order. I
started with the package that I wanted to build (coq-mathcomp-analysis),
and added the dependencies as I found they were needed.

I'll stick with committing dependencies in forward order (committing
dependencies before packages) from now on.

> I have tried to clean the mess but I give up for now. :-) It would be
> much easier if the series provides,
>
>  1. the Git commit against which revision these patches apply (see the
>     option --base of git-format-patch)
>
>  2. the correct dependency order of the patches

Probably it would also be easier to start over from the new master
branch and recommit the remaining packages in the proper order.

If I don't have another major interruption, I will send out a new set of
commits, in the correct order, formatted with --base, before or by
Friday. Excluding those packages which were already pushed to master, of
course :)

At 20:39 2022-09-24 UTC+0200, Julien Lepiller <julien@lepiller.eu> wrote:
> No need to repeat the license here. Also, this means that the license
> should be lgpl2.1+, instead of plain lgpl2.1.

Ah, seems like I was getting lost in package-ception there and didn't
check over the descriptions too rigorously. I'll keep this in mind when
preparing the next patchset for this thread.

> For python packages, I see you add python to the inputs. Why is that?
> The python-build-system already provides python.

I had been getting errors of the form "python3 was not found on the
PATH" during the 'configure' phase of some python packages, even though
the python-build-system was being used. I added python to everything to
avoid such errors, but forgot to remove it for packages where it was not
really needed.

If I can find the first package that produced that error, I'll submit a
bug report for it with the precise error quoted. 

> It looks like python-jsonschema-next (4.5.1) does not have any
> dependent, so updating this package instead might be better than
> adding a new one, wdyt?

I found evidence to the contrary, I think. With graphviz installed, I
ran

$ guix graph python-jsonschema > /tmp/py-js-deps.dot
$ gc -n /tmp/py-js-deps.dot

which says that there are 186 nodes, or (186 - 1) = 185 packages
dependent on python-jsonschema-next. If you prefer viewing it as an
image,

$ dot /tmp/py-js-deps.dot > /tmp/py-js-deps.png
$ feh /tmp/py-js-deps.png

shows all 185 packages originating from the node named
"python-jsonschema@4.5.1".

Maybe for now we could add this transitional python-jsonschema-4.15 to
build coq-mathcomp-analysis, and remove it in a subsequent patchset? I
don't want to tie this patch up unnecessarily.

If I have malformed patches now with only 20 packages,... well, let's
just say I don't know if I want to see the results just yet, if I'll
need to rebuild 185 :)

-- Garek

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[Garek Dyszel via Guix-patches via]

Hi again,

It looks like Coq has been updated to 8.16 now, which means the two
packages required by coq-mathcomp-hierarchy-builder in this patchset are
now out of date. The build processes have completely changed for
ocaml-elpi and coq-elpi.

The new ocaml-elpi build system got rather confusing and will likely
take me much longer than I originally expected. Maybe we could close
this issue? I think it might be easier if I were to send in ocaml-elpi
on its own, for example.

Let me know.

Thanks!
Garek

At 09:04 2022-09-27 UTC-0400, Garek Dyszel <garekdyszel@disroot.org> wrote:
> Hi Julien and simon,
>
> I planned to write back yesterday but had to run out the door
> unexpectedly.
>
> At 18:52 2022-09-26 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
>> For instance the series reads, ... where the logic about the order is
>> not obvious
>
> The logic was essentially adding dependencies in reverse order. I
> started with the package that I wanted to build (coq-mathcomp-analysis),
> and added the dependencies as I found they were needed.
>
> I'll stick with committing dependencies in forward order (committing
> dependencies before packages) from now on.
>
>> I have tried to clean the mess but I give up for now. :-) It would be
>> much easier if the series provides,
>>
>>  1. the Git commit against which revision these patches apply (see the
>>     option --base of git-format-patch)
>>
>>  2. the correct dependency order of the patches
>
> Probably it would also be easier to start over from the new master
> branch and recommit the remaining packages in the proper order.
>
> If I don't have another major interruption, I will send out a new set of
> commits, in the correct order, formatted with --base, before or by
> Friday. Excluding those packages which were already pushed to master, of
> course :)
>
> At 20:39 2022-09-24 UTC+0200, Julien Lepiller <julien@lepiller.eu> wrote:
>> No need to repeat the license here. Also, this means that the license
>> should be lgpl2.1+, instead of plain lgpl2.1.
>
> Ah, seems like I was getting lost in package-ception there and didn't
> check over the descriptions too rigorously. I'll keep this in mind when
> preparing the next patchset for this thread.
>
>> For python packages, I see you add python to the inputs. Why is that?
>> The python-build-system already provides python.
>
> I had been getting errors of the form "python3 was not found on the
> PATH" during the 'configure' phase of some python packages, even though
> the python-build-system was being used. I added python to everything to
> avoid such errors, but forgot to remove it for packages where it was not
> really needed.
>
> If I can find the first package that produced that error, I'll submit a
> bug report for it with the precise error quoted. 
>
>> It looks like python-jsonschema-next (4.5.1) does not have any
>> dependent, so updating this package instead might be better than
>> adding a new one, wdyt?
>
> I found evidence to the contrary, I think. With graphviz installed, I
> ran
>
> $ guix graph python-jsonschema > /tmp/py-js-deps.dot
> $ gc -n /tmp/py-js-deps.dot
>
> which says that there are 186 nodes, or (186 - 1) = 185 packages
> dependent on python-jsonschema-next. If you prefer viewing it as an
> image,
>
> $ dot /tmp/py-js-deps.dot > /tmp/py-js-deps.png
> $ feh /tmp/py-js-deps.png
>
> shows all 185 packages originating from the node named
> "python-jsonschema@4.5.1".
>
> Maybe for now we could add this transitional python-jsonschema-4.15 to
> build coq-mathcomp-analysis, and remove it in a subsequent patchset? I
> don't want to tie this patch up unnecessarily.
>
> If I have malformed patches now with only 20 packages,... well, let's
> just say I don't know if I want to see the results just yet, if I'll
> need to rebuild 185 :)
>
> -- Garek

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 4331 bytes --]

You can close by sending a reply to nnnnn-close@debbugs.gnu.org, where nnnnn is the bug number. If it's easier for you, let's focus on ocaml-elpi first :)

If you have any question or need help, don't hesitate to ask!

Le 29 septembre 2022 19:13:25 GMT+02:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
>Hi again,
>
>It looks like Coq has been updated to 8.16 now, which means the two
>packages required by coq-mathcomp-hierarchy-builder in this patchset are
>now out of date. The build processes have completely changed for
>ocaml-elpi and coq-elpi.
>
>The new ocaml-elpi build system got rather confusing and will likely
>take me much longer than I originally expected. Maybe we could close
>this issue? I think it might be easier if I were to send in ocaml-elpi
>on its own, for example.
>
>Let me know.
>
>Thanks!
>Garek
>
>At 09:04 2022-09-27 UTC-0400, Garek Dyszel <garekdyszel@disroot.org> wrote:
>> Hi Julien and simon,
>>
>> I planned to write back yesterday but had to run out the door
>> unexpectedly.
>>
>> At 18:52 2022-09-26 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
>>> For instance the series reads, ... where the logic about the order is
>>> not obvious
>>
>> The logic was essentially adding dependencies in reverse order. I
>> started with the package that I wanted to build (coq-mathcomp-analysis),
>> and added the dependencies as I found they were needed.
>>
>> I'll stick with committing dependencies in forward order (committing
>> dependencies before packages) from now on.
>>
>>> I have tried to clean the mess but I give up for now. :-) It would be
>>> much easier if the series provides,
>>>
>>>  1. the Git commit against which revision these patches apply (see the
>>>     option --base of git-format-patch)
>>>
>>>  2. the correct dependency order of the patches
>>
>> Probably it would also be easier to start over from the new master
>> branch and recommit the remaining packages in the proper order.
>>
>> If I don't have another major interruption, I will send out a new set of
>> commits, in the correct order, formatted with --base, before or by
>> Friday. Excluding those packages which were already pushed to master, of
>> course :)
>>
>> At 20:39 2022-09-24 UTC+0200, Julien Lepiller <julien@lepiller.eu> wrote:
>>> No need to repeat the license here. Also, this means that the license
>>> should be lgpl2.1+, instead of plain lgpl2.1.
>>
>> Ah, seems like I was getting lost in package-ception there and didn't
>> check over the descriptions too rigorously. I'll keep this in mind when
>> preparing the next patchset for this thread.
>>
>>> For python packages, I see you add python to the inputs. Why is that?
>>> The python-build-system already provides python.
>>
>> I had been getting errors of the form "python3 was not found on the
>> PATH" during the 'configure' phase of some python packages, even though
>> the python-build-system was being used. I added python to everything to
>> avoid such errors, but forgot to remove it for packages where it was not
>> really needed.
>>
>> If I can find the first package that produced that error, I'll submit a
>> bug report for it with the precise error quoted. 
>>
>>> It looks like python-jsonschema-next (4.5.1) does not have any
>>> dependent, so updating this package instead might be better than
>>> adding a new one, wdyt?
>>
>> I found evidence to the contrary, I think. With graphviz installed, I
>> ran
>>
>> $ guix graph python-jsonschema > /tmp/py-js-deps.dot
>> $ gc -n /tmp/py-js-deps.dot
>>
>> which says that there are 186 nodes, or (186 - 1) = 185 packages
>> dependent on python-jsonschema-next. If you prefer viewing it as an
>> image,
>>
>> $ dot /tmp/py-js-deps.dot > /tmp/py-js-deps.png
>> $ feh /tmp/py-js-deps.png
>>
>> shows all 185 packages originating from the node named
>> "python-jsonschema@4.5.1".
>>
>> Maybe for now we could add this transitional python-jsonschema-4.15 to
>> build coq-mathcomp-analysis, and remove it in a subsequent patchset? I
>> don't want to tie this patch up unnecessarily.
>>
>> If I have malformed patches now with only 20 packages,... well, let's
>> just say I don't know if I want to see the results just yet, if I'll
>> need to rebuild 185 :)
>>
>> -- Garek

[-- Attachment #2: Type: text/html, Size: 5397 bytes --]

bug#57540: Splitting into several packages instead

[Garek Dyszel via Guix-patches via]

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[Garek Dyszel via Guix-patches via]

Sounds like a plan. Thanks again!

At 19:39 2022-09-29 UTC+0200, Julien Lepiller <julien@lepiller.eu> wrote:
> You can close by sending a reply to nnnnn-close@debbugs.gnu.org, where nnnnn is the bug number. If it's easier for you, let's focus on ocaml-elpi first :)
>
> If you have any question or need help, don't hesitate to ask!
>
> Le 29 septembre 2022 19:13:25 GMT+02:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
>>Hi again,
>>
>>It looks like Coq has been updated to 8.16 now, which means the two
>>packages required by coq-mathcomp-hierarchy-builder in this patchset are
>>now out of date. The build processes have completely changed for
>>ocaml-elpi and coq-elpi.
>>
>>The new ocaml-elpi build system got rather confusing and will likely
>>take me much longer than I originally expected. Maybe we could close
>>this issue? I think it might be easier if I were to send in ocaml-elpi
>>on its own, for example.
>>
>>Let me know.
>>
>>Thanks!
>>Garek
>>
>>At 09:04 2022-09-27 UTC-0400, Garek Dyszel <garekdyszel@disroot.org> wrote:
>>> Hi Julien and simon,
>>>
>>> I planned to write back yesterday but had to run out the door
>>> unexpectedly.
>>>
>>> At 18:52 2022-09-26 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
>>>> For instance the series reads, ... where the logic about the order is
>>>> not obvious
>>>
>>> The logic was essentially adding dependencies in reverse order. I
>>> started with the package that I wanted to build (coq-mathcomp-analysis),
>>> and added the dependencies as I found they were needed.
>>>
>>> I'll stick with committing dependencies in forward order (committing
>>> dependencies before packages) from now on.
>>>
>>>> I have tried to clean the mess but I give up for now. :-) It would be
>>>> much easier if the series provides,
>>>>
>>>>  1. the Git commit against which revision these patches apply (see the
>>>>     option --base of git-format-patch)
>>>>
>>>>  2. the correct dependency order of the patches
>>>
>>> Probably it would also be easier to start over from the new master
>>> branch and recommit the remaining packages in the proper order.
>>>
>>> If I don't have another major interruption, I will send out a new set of
>>> commits, in the correct order, formatted with --base, before or by
>>> Friday. Excluding those packages which were already pushed to master, of
>>> course :)
>>>
>>> At 20:39 2022-09-24 UTC+0200, Julien Lepiller <julien@lepiller.eu> wrote:
>>>> No need to repeat the license here. Also, this means that the license
>>>> should be lgpl2.1+, instead of plain lgpl2.1.
>>>
>>> Ah, seems like I was getting lost in package-ception there and didn't
>>> check over the descriptions too rigorously. I'll keep this in mind when
>>> preparing the next patchset for this thread.
>>>
>>>> For python packages, I see you add python to the inputs. Why is that?
>>>> The python-build-system already provides python.
>>>
>>> I had been getting errors of the form "python3 was not found on the
>>> PATH" during the 'configure' phase of some python packages, even though
>>> the python-build-system was being used. I added python to everything to
>>> avoid such errors, but forgot to remove it for packages where it was not
>>> really needed.
>>>
>>> If I can find the first package that produced that error, I'll submit a
>>> bug report for it with the precise error quoted. 
>>>
>>>> It looks like python-jsonschema-next (4.5.1) does not have any
>>>> dependent, so updating this package instead might be better than
>>>> adding a new one, wdyt?
>>>
>>> I found evidence to the contrary, I think. With graphviz installed, I
>>> ran
>>>
>>> $ guix graph python-jsonschema > /tmp/py-js-deps.dot
>>> $ gc -n /tmp/py-js-deps.dot
>>>
>>> which says that there are 186 nodes, or (186 - 1) = 185 packages
>>> dependent on python-jsonschema-next. If you prefer viewing it as an
>>> image,
>>>
>>> $ dot /tmp/py-js-deps.dot > /tmp/py-js-deps.png
>>> $ feh /tmp/py-js-deps.png
>>>
>>> shows all 185 packages originating from the node named
>>> "python-jsonschema@4.5.1".
>>>
>>> Maybe for now we could add this transitional python-jsonschema-4.15 to
>>> build coq-mathcomp-analysis, and remove it in a subsequent patchset? I
>>> don't want to tie this patch up unnecessarily.
>>>
>>> If I have malformed patches now with only 20 packages,... well, let's
>>> just say I don't know if I want to see the results just yet, if I'll
>>> need to rebuild 185 :)
>>>
>>> -- Garek

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[zimoun]

Hi,

On Thu, 29 Sep 2022 at 13:13, Garek Dyszel via Guix-patches via <guix-patches@gnu.org> wrote:

> It looks like Coq has been updated to 8.16 now, which means the two
> packages required by coq-mathcomp-hierarchy-builder in this patchset are
> now out of date. The build processes have completely changed for
> ocaml-elpi and coq-elpi.

From my point of view, the easiest to send this patch set with the
correct order and against the current master.  Even if some patches does
not build correctly.

Based on that, we could merge what is currently ready.  And collectively
fixes what is missing.

Because today, it is too much work to unknot your patch set.

If it is too much work for you, please point against which Git commit
you generated the patch set.


Cheers,
simon

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[Garek Dyszel via Guix-patches via]

I didn't see this last email before I closed the issue a couple of days
ago. Sorry for not catching it sooner.

At 14:06 2022-09-30 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
> Because today, it is too much work to unknot your patch set.
I agree. For a first patch set, it is a mess! :)

> If it is too much work for you, please point against which Git commit
> you generated the patch set.
At this point I don't know. Before you had mentioned --base, I had
already started working on another package and lost track of which
commit this patch set was generated from.

> From my point of view, the easiest to send this patch set with the
> correct order and against the current master. Even if some patches
> does not build correctly.
>
> Based on that, we could merge what is currently ready. And
> collectively fixes what is missing.
Oh, I suppose it didn't occur to me that we could fix the broken parts
collectively :/ Would it be better to re-open this issue or start a new
one?

[bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis))

[zimoun]

Hi,

On dim., 02 oct. 2022 at 16:52, Garek Dyszel via Guix-patches via <guix-patches@gnu.org> wrote:
> I didn't see this last email before I closed the issue a couple of days
> ago. Sorry for not catching it sooner.
>
> At 14:06 2022-09-30 UTC+0200, zimoun <zimon.toutoune@gmail.com> wrote:
>> Because today, it is too much work to unknot your patch set.
> I agree. For a first patch set, it is a mess! :)
>
>> If it is too much work for you, please point against which Git commit
>> you generated the patch set.
> At this point I don't know. Before you had mentioned --base, I had
> already started working on another package and lost track of which
> commit this patch set was generated from.
>
>> From my point of view, the easiest to send this patch set with the
>> correct order and against the current master. Even if some patches
>> does not build correctly.
>>
>> Based on that, we could merge what is currently ready. And
>> collectively fixes what is missing.
> Oh, I suppose it didn't occur to me that we could fix the broken parts
> collectively :/ Would it be better to re-open this issue or start a new
> one?

That’s why ’--base’ is documented in «Submitting patches»; see #1 in [1].

Because if the branch evolves between the submission and the moment when
others give a look, it is still possible by others to apply the patch
and rebase.

Something to have in mind for the next time. :-)


Well, personally I am not able to reuse your work and Julien neither,
IIUC.  Therefore, feel free to close this submission and reopen another
one.


1: <https://guix.gnu.org/manual/devel/en/guix.html#Submitting-Patches>


Cheers,
simon

[bug#57540] [RFC PATCH v2 02/19] gnu: Add ocaml-atd.* gnu/packages/ocaml.scm (ocaml-atd): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/ocaml.scm (ocaml-atd): New variable.
---
 gnu/packages/ocaml.scm | 59 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index c4fa05b934..11b982519b 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8870,3 +8870,62 @@ (define-public ocaml-elpi
 
 ELPI is free software released under the terms of LGPL 2.1 or above.")
     (license license:lgpl2.1)))
+
+;; NOTE: requires python-jsonschema with version at minimum 4.6.0 to run
+;; tests.
+;; 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)
+                    (recursive? #t)))
+              (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
+                         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"))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 03/19] gnu: Add ocaml-ansiterminal.* gnu/packages/ocaml.scm (ocaml-ansiterminal): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/ocaml.scm (ocaml-ansiterminal): New variable.
---
 gnu/packages/ocaml.scm | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 11b982519b..ac0e0c0bc1 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8929,3 +8929,32 @@ (define-public ocaml-atd
 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"))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 04/19] gnu: Add coq-elpi.* gnu/packages/coq.scm (coq-elpi): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-elpi): New variable.
---
 gnu/packages/coq.scm | 79 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df27d..5ae5392db4 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -8,6 +8,7 @@
 ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
 ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -685,3 +686,81 @@ (define-public coq-stdpp
 @end itemize")
     (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
     (license license:bsd-3)))
+
+(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)
+    (outputs '("out"))
+    (arguments
+     `(#:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input "ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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."
+                    ;; Tests run if we invoke "make test" instead.
+                    (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 λProlog 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 λProlog.
+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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 05/19] gnu: Add coq-mathcomp-hierarchy-builder.* gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder): New variable.
---
 gnu/packages/coq.scm | 72 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5ae5392db4..24f9492175 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -764,3 +764,75 @@ (define-public coq-elpi
 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="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") "/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input "ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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-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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 06/19] gnu: Add coq-mathcomp-finmap.* gnu/packages/coq.scm (coq-mathcomp-finmap): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-finmap): New variable.
---
 gnu/packages/coq.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 24f9492175..d123860172 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -836,3 +836,40 @@ (define-public coq-mathcomp-hierarchy-builder
     (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="
+                                         (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 sets
+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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 07/19] gnu: Add coq-mathcomp-bigenough.* gnu/packages/coq.scm (coq-mathcomp-bigenough): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-bigenough): New variable.
---
 gnu/packages/coq.scm | 50 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index d123860172..78ef5473fd 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -873,3 +873,53 @@ (define-public coq-mathcomp-finmap
 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!"
+  (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="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 08/19] gnu: Add coq-mathcomp-analysis.* gnu/packages/coq.scm (coq-mathcomp-analysis): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/coq.scm (coq-mathcomp-analysis): New variable.
---
 gnu/packages/coq.scm | 66 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 78ef5473fd..036134b8ff 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -923,3 +923,69 @@ (define-public coq-mathcomp-bigenough
 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.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="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") "/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (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
+                  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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 09/19] gnu: Add python-version.* gnu/packages/python-xyz.scm (python-version): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-version): New variable.
---
 gnu/packages/python-xyz.scm | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index a73f07ece3..cc5b85c3a1 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -128,6 +128,7 @@
 ;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
 ;;; Copyright © 2022 Hilton Chain <hako@ultrarare.space>
 ;;; Copyright © 2022 Tomasz Jeneralczyk <tj@schwi.pl>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -30746,3 +30747,27 @@ (define-public python-lief
      "@code{python-lief} is a cross platform library which can parse, modify
 and abstract ELF, PE and MachO formats.")
     (license license:asl2.0)))
+
+(define-public python-version
+  ;; No version tags available in the git repo; just using bare commit instead.
+  (let ((commit "5232eea250ab72cc5cb72b0b75efb35d2192b906")
+        (revision "1"))
+    (package
+      (name "python-python-version")
+      (version (git-version "0.0.2" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://gitlab.com/halfak/python_version")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (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 version.")
+      ;; MIT License
+      (license license:expat))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 10/19] gnu: Add python-hatchling.* gnu/packages/python-xyz.scm (python-hatchling): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-hatchling): New variable.
---
 gnu/packages/python-xyz.scm | 64 +++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index cc5b85c3a1..8dd8d902a5 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30771,3 +30771,67 @@ (define-public python-version
        "This package provides a simple utility for checking the python version.")
       ;; MIT License
       (license license:expat))))
+
+(define-public python-hatchling
+  (package
+    (name "python-hatchling")
+    (version "1.8.1")
+    (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"))))
+    ;; 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
+                  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-tomli
+                  python-platformdirs))
+    (build-system python-build-system)
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  ;; Copied directly from the build process for
+                  ;; python-jsonschema-next.
+                  (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))))
+                  (replace 'check
+                    (lambda* (#:key tests? #:allow-other-keys)
+                      (when tests?
+                        (invoke "pytest" "-vv")))))))
+    (home-page "https://ofek.dev/projects/hatch/")
+    (synopsis "Modern, extensible Python project management")
+    (description "Modern, extensible Python project management")
+    ;; MIT License
+    (license license:expat)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 11/19] gnu: Add python-hatch-vcs.* gnu/packages/python-xyz.scm (python-hatch-vcs): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-hatch-vcs): New variable.
---
 gnu/packages/python-xyz.scm | 62 +++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8dd8d902a5..b5b319cfde 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30835,3 +30835,65 @@ (define-public python-hatchling
     (description "Modern, extensible Python project management")
     ;; 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
+                    python-pypa-build
+                    python-pathspec
+                    python-pluggy-1.0
+                    python-editables
+                    git))
+      ;; python-setuptools-scm-6.4 minimum
+      (propagated-inputs (list python-hatchling))
+      (native-inputs (list python-pytest python-setuptools-scm-7))
+      (arguments
+       ;; Copied directly from the build process for
+       ;; python-jsonschema-next.
+       (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 "pytest" "-vvv"))))))))
+      (home-page "https://ofek.dev/projects/hatch/")
+      (synopsis "Hatch plugin for versioning with your preferred VCS")
+      (description "Hatch plugin for versioning with your preferred VCS")
+      ;; MIT License
+      (license license:expat))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 12/19] gnu: Add python-hatch-fancy-pypi-readme.* gnu/packages/python-xyz.scm (python-hatch-fancy-pypi-readme): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-hatch-fancy-pypi-readme): New variable.
---
 gnu/packages/python-xyz.scm | 66 +++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index b5b319cfde..2c358b8c58 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30897,3 +30897,69 @@ (define-public python-hatch-vcs
       (description "Hatch plugin for versioning with your preferred VCS")
       ;; MIT License
       (license license:expat))))
+
+(define-public python-hatch-fancy-pypi-readme
+  (package
+    (name "python-hatch-fancy-pypi-readme")
+    (version "22.3.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-hatchling python-tomli
+                             python-typing-extensions))
+    (native-inputs (list python
+                         python-pypa-build
+                         python-pathspec
+                         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 this,
+                      ;; 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=True)"
+                       "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 "Fancy PyPI READMEs with Hatch")
+    (description "Fancy PyPI READMEs with Hatch")
+    ;; MIT License
+    (license license:expat)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 13/19] gnu: Add python-pprintpp.* gnu/packages/python-xyz.scm (python-pprintpp): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-pprintpp): New variable.
---
 gnu/packages/python-xyz.scm | 58 +++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 2c358b8c58..90bf269341 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30963,3 +30963,61 @@ (define-public python-hatch-fancy-pypi-readme
     (description "Fancy PyPI READMEs with Hatch")
     ;; MIT License
     (license license:expat)))
+
+(define-public python-pprintpp
+  ;; Git version tags are inaccurate for this package, too; 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 python-pypa-build python-hypothesis python-wheel
+                    python-parameterized))
+      (native-inputs (list python-pytest python-nose))
+      (build-system python-build-system)
+      (arguments
+       ;; Copied directly from the build process for
+       ;; python-jsonschema-next.
+       (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 "Drop-in replacement for pprint that's actually pretty")
+      (description
+       "This package provides a drop-in replacement for pprint that's actually pretty.")
+      (license license:bsd-3))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 14/19] gnu: Add python-icdiff.* gnu/packages/python-xyz.scm (python-icdiff): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-icdiff): New variable.
---
 gnu/packages/python-xyz.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 90bf269341..1651f00054 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -31021,3 +31021,23 @@ (define-public python-pprintpp
       (description
        "This package provides a drop-in replacement for pprint that's actually pretty.")
       (license license:bsd-3))))
+
+(define-public python-icdiff
+  (package
+    (name "python-icdiff")
+    (version "2.0.5")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/jeffkaufman/icdiff")
+                    (commit (string-append "release-" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "14gr9j2h7sfw47pwfzspm4zinywhqmzm4a0qz5c2k9wbixz120a4"))))
+    (build-system python-build-system)
+    (home-page "https://www.jefftk.com/icdiff")
+    (synopsis "Improved colored diff")
+    (description "Improved colored diff.")
+    ;; Python Software Foundation License version 2
+    (license license:psfl)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 15/19] gnu: Add python-pytest-icdiff.* gnu/packages/python-check.scm (python-pytest-icdiff): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-check.scm (python-pytest-icdiff): New variable.
---
 gnu/packages/python-check.scm | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/gnu/packages/python-check.scm b/gnu/packages/python-check.scm
index 5ee1d41f34..6199b1e147 100644
--- a/gnu/packages/python-check.scm
+++ b/gnu/packages/python-check.scm
@@ -16,6 +16,7 @@
 ;;; Copyright © 2022 Malte Frank Gerdes <malte.f.gerdes@gmail.com>
 ;;; Copyright © 2022 Felix Gruber <felgru@posteo.net>
 ;;; Copyright © 2022 Tomasz Jeneralczyk <tj@schwi.pl>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -2468,3 +2469,24 @@ (define-public python-xvfbwrapper
 physical display.  Only a network layer is necessary.  Xvfb is useful for
 running acceptance tests on headless servers.")
     (license license:expat)))
+
+(define-public python-pytest-icdiff
+  (package
+    (name "python-pytest-icdiff")
+    (version "0.6")
+    (source (origin
+              ;; Tests fail in git version, but not in the PyPi version.
+              ;; The PyPi version is also more up-to-date.
+              (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))
+    (native-inputs (list 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 (license:non-copyleft "LICENSE"))))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 16/19] gnu: Add python-editables.* gnu/packages/python-build.scm (python-editables): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-build.scm (python-editables): New variable.
---
 gnu/packages/python-build.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
index e7023aca0c..d7f93543f4 100644
--- a/gnu/packages/python-build.scm
+++ b/gnu/packages/python-build.scm
@@ -7,6 +7,7 @@
 ;;; Copyright © 2018, 2021, 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com>
 ;;; Copyright © 2021 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2021, 2022 Ricardo Wurmus <rekado@elephly.net>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -474,3 +475,22 @@ (define-public python-setuptools-scm
 @dfn{software configuration management} (SCM) metadata instead of declaring
 them as the version argument or in a SCM managed file.")
     (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)))
+              (file-name (git-file-name name 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)))
-- 
2.37.2

[bug#57540] [RFC PATCH v2 17/19] gnu: Add python-pluggy-1.0.* gnu/packages/python-xyz.scm (python-pluggy-1.0): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-pluggy-1.0): New variable.
---
 gnu/packages/python-xyz.scm | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 1651f00054..7febf50286 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -14585,6 +14585,26 @@ (define-public python-pluggy
    (home-page "https://pypi.org/project/pluggy/")
    (license license:expat)))
 
+(define-public python-pluggy-1.0
+  (package
+    (inherit python-pluggy)
+    (name "python-pluggy")
+    (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'."
+              ;;
+              ;; The PyPi version does not throw this error.
+              (method url-fetch)
+              (uri (pypi-uri "pluggy" version))
+              (sha256
+               (base32
+                "0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922"))))
+    (inputs (list python python-pypa-build python-wheel))
+    (native-inputs (list python-pytest python-setuptools-scm))))
+
 (define-public python-plumbum
   (package
     (name "python-plumbum")
-- 
2.37.2

[bug#57540] [RFC PATCH v2 18/19] gnu: Add python-setuptools-scm-7.* gnu/packages/python.xyz.scm (python-setuptools-scm-7): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python.xyz.scm (python-setuptools-scm-7): New variable.
---
 gnu/packages/python-xyz.scm | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 7febf50286..0e67adc95f 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -20859,6 +20859,38 @@ (define-public python-setuptools-scm-git-archive
 belong to tagged versions.")
     (license license:expat)))
 
+(define-public python-setuptools-scm-7
+  ;; The version tags are inaccurate. Use the bare commit.
+  (let ((commit "c4d37004ab0a16c2cacdc58ef06b36956db02a9f")
+        (revision "1"))
+    (package
+      (name "python-setuptools-scm")
+      (version (git-version "7.0.5" revision commit))
+      (source (origin
+                ;; Won't build with git. Fails with error:
+                ;; "ERROR Backend subproccess exited when trying to invoke
+                ;; get_requires_for_build_wheel"
+                ;;
+                ;; The PyPi version has no such issue.
+                (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-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-setuptools-git
   (package
     (name "python-setuptools-git")
-- 
2.37.2

[bug#57540] [RFC PATCH v2 19/19] gnu: Add python-jsonschema-4.15.* gnu/packages/python-xyz.scm (python-jsonschema-4.15): New variable.

[Garek Dyszel via Guix-patches via]

* gnu/packages/python-xyz.scm (python-jsonschema-4.15): New variable.
---
 gnu/packages/python-xyz.scm | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 0e67adc95f..fd470652bc 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -3661,6 +3661,37 @@ (define-public python-jsonschema-next
            python-pyrsistent
            python-typing-extensions))))
 
+(define-public python-jsonschema-4.15
+  (package
+    (inherit python-jsonschema)
+    (name "python-jsonschema-4.15")
+    (version "4.15.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/python-jsonschema/jsonschema")
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "1yv01id6l0s1dq6khal9jvxh9dqivy394z04y6yr5lv8cimwcx2x"))))
+    (native-inputs (list python-pypa-build
+                         python-twisted
+                         python-hatchling
+                         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))
+    (arguments
+     (substitute-keyword-arguments
+         (package-arguments python-jsonschema-next)))
+    (home-page "https://github.com/python-jsonschema/jsonschema")))
+
 (define-public python-schema
   (package
     (name "python-schema")
-- 
2.37.2