[PATCH] Add coq-mathcomp-analysis

  • Open
  • quality assurance status badge
Details
4 participants
  • Garek Dyszel
  • Julien Lepiller
  • Lars-Dominik Braun
  • zimoun
Owner
unassigned
Submitted by
Garek Dyszel
Severity
normal
G
G
Garek Dyszel wrote on 5 Oct 2022 19:15
(address . guix-patches@gnu.org)
87h70iqji2.fsf@disroot.org
This patch set adds coq-mathcomp-analysis, but it does not build
correctly.

The build process for ocaml-elpi@1.16.5 is broken. I did, however, get
coq-mathcomp-analysis to successfully build when using an older
version: ocaml-elpi@1.15.2, which builds just fine.

To aid in debugging, I left the information for both versions of
ocaml-elpi in the commit which adds ocaml-elpi (ocaml-elpi@1.15.2's
info is commented out).

We will have to see whether it's possible to upgrade coq-elpi to
1.15.6 without breaking coq-mathcomp-hierarchy-builder. The same goes
for whether it's possible to upgrade coq-mathcomp-hierarchy-builder to
1.4.0 without breaking coq-mathcomp-analysis.

There is an unresolved warning from guix lint that says
"python-hatch@1.5.0: can be upgraded to 1.10.0". In fact, both
python-hatch and python-hatch-bootstrap are located in the same
repository, and the newest tag for hatch is hatch-v1.5.0. In this
case, guix lint is incorrect.

Let me know what you think!
G
G
Garek Dyszel wrote on 5 Oct 2022 19:40
[PATCH 01/14] gnu: Add python-pprintpp.
(address . 58310@debbugs.gnu.org)
87lepuqidb.fsf@disroot.org
* gnu/packages/python-xyz.scm (python-pprintpp): New variable.
---
gnu/packages/python-xyz.scm | 54 +++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)

Toggle diff (69 lines)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8575d4a67e..439765dc4f 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -16688,6 +16688,60 @@ (define-public python-tabulate
data in Python.")
(license license:expat)))
+(define-public python-pprintpp
+ ;; Git version tags are inaccurate for this package; use the
+ ;; bare commit.
+ (let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0")
+ (revision "1"))
+ (package
+ (name "python-pprintpp")
+ (version (git-version "0.3.0" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/wolever/pprintpp")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li"))))
+ (inputs (list python-pypa-build python-hypothesis python-wheel
+ python-parameterized))
+ (native-inputs (list python-pytest python-nose))
+ (build-system python-build-system)
+ (arguments
+ (list #:phases #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (setenv "SOURCE_DATE_EPOCH" "315532800")
+ (invoke "python"
+ "-m"
+ "build"
+ "--wheel"
+ "--no-isolation"
+ ".")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((whl (car (find-files "dist" "\\.whl$"))))
+ (invoke "pip"
+ "--no-cache-dir"
+ "--no-input"
+ "install"
+ "--no-deps"
+ "--prefix"
+ #$output
+ whl))))
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ (when tests?
+ (invoke "python" "test.py")))))))
+ (home-page "https://github.com/wolever/pprintpp")
+ (synopsis "Python pretty-printer")
+ (description
+ "This package is a printer for Python which pretty-prints structures.
+It also attempts to print Unicode characters without escaping them.")
+ (license license:bsd-3))))
+
(define-public python-kazoo
(package
(name "python-kazoo")

base-commit: fd6cd9de8682c7ddf96bf8deb637b1ca6cdbd205
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:41
[PATCH 02/14] gnu: Add python-pluggy-1.0.* gnu/packages/python-xyz.scm (python-pluggy-1.0): New variable.
(address . 58310@debbugs.gnu.org)
87ilkyqibo.fsf@disroot.org
* gnu/packages/python-xyz.scm (python-pluggy-1.0): New variable.
---
gnu/packages/python-xyz.scm | 14 ++++++++++++++
1 file changed, 14 insertions(+)

Toggle diff (27 lines)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 439765dc4f..8a4ac37abf 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -14741,6 +14741,20 @@ (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
+ (method url-fetch)
+ (uri (pypi-uri "pluggy" version))
+ (sha256
+ (base32
+ "0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922"))))
+ (inputs (list python-pypa-build python-wheel))
+ (native-inputs (list python-pytest python-setuptools-scm))))
+
(define-public python-plumbum
(package
(name "python-plumbum")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:41
[PATCH 03/14] gnu: Add python-setuptools-scm-7.* gnu/packages/python-build.scm (python-setuptools-scm-7): New variable.
(address . 58310@debbugs.gnu.org)
87fsg2qib6.fsf@disroot.org
* gnu/packages/python-build.scm (python-setuptools-scm-7): New variable.
---
gnu/packages/python-build.scm | 19 +++++++++++++++++++
1 file changed, 19 insertions(+)

Toggle diff (32 lines)
diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
index 9d9b07f769..e17cde16d9 100644
--- a/gnu/packages/python-build.scm
+++ b/gnu/packages/python-build.scm
@@ -476,6 +476,25 @@ (define-public python-setuptools-scm
them as the version argument or in a SCM managed file.")
(license license:expat)))
+(define-public python-setuptools-scm-7
+ (package
+ (inherit python-setuptools-scm)
+ (version "7.0.5")
+ (source (origin
+ (method url-fetch)
+ (uri (pypi-uri "setuptools_scm" version))
+ (sha256
+ (base32
+ "0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3"))))
+ (build-system python-build-system)
+ (arguments
+ `( ;Disabled tests to avoid extra dependencies.
+ #:tests? #f
+ #:phases (modify-phases %standard-phases
+ ;; Disabled sanity check to avoid extra dependencies.
+ (delete 'sanity-check))))
+ (propagated-inputs (list python-packaging-bootstrap python-tomli))))
+
(define-public python-editables
(package
(name "python-editables")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:41
[PATCH 04/14] gnu: Add python-hatchling-bootstrap.
(address . 58310@debbugs.gnu.org)
87czb6qiah.fsf@disroot.org
* gnu/packages/python-build.scm (python-hatchling-bootstrap): New variable.
---
gnu/packages/python-build.scm | 63 +++++++++++++++++++++++++++++++++++
1 file changed, 63 insertions(+)

Toggle diff (73 lines)
diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
index e17cde16d9..f90d23874f 100644
--- a/gnu/packages/python-build.scm
+++ b/gnu/packages/python-build.scm
@@ -516,3 +516,66 @@ (define-public python-editables
``editable mode''. In other words, changes to the package source will be
reflected in the package visible to Python, without needing a reinstall.")
(license license:expat)))
+
+;; This depends on packages in python-xyz.scm:
+;; python-version, python-importlib-metadata, python-pathspec,
+;; python-pluggy-1.0, and python-platformdirs.
+(define-public python-hatchling-bootstrap
+ (package
+ (name "python-hatchling-bootstrap")
+ (version "1.10.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/pypa/hatch")
+ (commit (string-append "hatchling-v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ ;;"1q25kqw71g8mjwfjz9ph0iigdqa26zzxgmqm0v0bp0z1j8rcl237"
+ "1yqkwck2aihfdm9ljv5q4nygmmqyp35xwyp8lqn2f4vq9p6njq3c"))))
+ ;; python-pypa-build needed for bootstrapping.
+ ;; Otherwise we get a circular reference:
+ ;; python-hatchling trying to build itself, without
+ ;; first having hatchling installed.
+ (inputs (list python-pypa-build
+ python-editables
+ python-importlib-metadata
+ python-version
+ python-packaging-next
+ python-pathspec
+ python-pluggy-1.0 ;TODO: Not detected by pytest?
+ python-tomli
+ python-platformdirs))
+ (build-system python-build-system)
+ (arguments
+ `( ;Tests depend on module python-hatch, which this
+ ;; is bootstrapping.
+ #:tests? #f
+ #:phases (modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (chdir "backend")
+ ;; ZIP does not support timestamps before 1980.
+ (setenv "SOURCE_DATE_EPOCH" "315532800")
+ (invoke "python"
+ "-m"
+ "build"
+ "--wheel"
+ "--no-isolation"
+ ".")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((whl (car (find-files "dist" "\\.whl$"))))
+ (invoke "pip"
+ "--no-cache-dir"
+ "--no-input"
+ "install"
+ "--no-deps"
+ "--prefix"
+ (assoc-ref %outputs "out")
+ whl)))))))
+ (home-page "https://ofek.dev/projects/hatch/")
+ (synopsis "Bootstrap binaries to build @code{python-hatch}")
+ (description "Bootstrap binaries to build @code{python-hatch}")
+ (license license:expat)))
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:46
[PATCH 05/14] gnu: Add python-hatch.
(address . 58310@debbugs.gnu.org)
878rluqi3n.fsf@disroot.org
Toggle diff (71 lines)
diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
index f90d23874f..0b8d8a7647 100644
--- a/gnu/packages/python-build.scm
+++ b/gnu/packages/python-build.scm
@@ -579,3 +579,64 @@ (define-public python-hatchling-bootstrap
(synopsis "Bootstrap binaries to build @code{python-hatch}")
(description "Bootstrap binaries to build @code{python-hatch}")
(license license:expat)))
+
+(define-public python-hatch
+ (package
+ (name "python-hatch")
+ (version "1.10.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/pypa/hatch")
+ (commit (string-append "hatch-v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "030yi9hw50mn899pq073lw2a55r57skl2g9agjp3b4l95f3nay30"))))
+ (inputs (list python-pypa-build
+ python-editables
+ python-importlib-metadata
+ python-version
+ python-packaging-next
+ python-pathspec
+ python-pluggy-1.0 ;TODO: Not detected by pytest?
+ python-hatchling-bootstrap
+ python-tomli
+ python-platformdirs
+ python-rich
+ python-tomli-w))
+ (build-system python-build-system)
+ (arguments
+ `( ;Tests appear to be written such that the input python-pluggy-1.0 is
+ ;; not detected.
+ #:tests? #f
+ #:phases (modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ ;; ZIP does not support timestamps before 1980.
+ (setenv "SOURCE_DATE_EPOCH" "315532800")
+ (invoke "hatchling" "build")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((whl (car (find-files "dist" "\\.whl$"))))
+ (invoke "pip"
+ "--no-cache-dir"
+ "--no-input"
+ "install"
+ "--no-deps"
+ "--prefix"
+ (assoc-ref %outputs "out")
+ whl))))
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ (when tests?
+ (chdir "tests")
+ (invoke "pytest" "-vv"))))
+ ;; Can't have hatch as a requirement of itself.
+ (delete 'sanity-check))))
+ (home-page "https://ofek.dev/projects/hatch/")
+ (synopsis "Python build system with project generation")
+ (description
+ "Python build system with project generation. It also defines a specific
+syntax in @code{toml} files to check for dependencies.")
+ (license license:expat)))
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:46
[PATCH 06/14] gnu: Add python-hatch-vcs.
(address . 58310@debbugs.gnu.org)
875ygyqi37.fsf@disroot.org
Toggle diff (73 lines)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8a4ac37abf..5739c759de 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -27391,6 +27391,66 @@ (define-public python-versioneer
process.")
(license license:public-domain)))
+(define-public python-hatch-vcs
+ ;; Tags are not accurate; just use the commit itself.
+ (let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2")
+ (revision "1"))
+ (package
+ (name "python-hatch-vcs")
+ (version (git-version "0.2.0" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ofek/hatch-vcs")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05"))))
+ (build-system python-build-system)
+ (inputs (list python-pypa-build
+ python-pathspec
+ python-pluggy-1.0
+ python-editables
+ git
+ python-hatchling-bootstrap
+ python-typing-extensions))
+ (native-inputs (list python-pytest
+ ;; python-setuptools-scm-6.4 minimum
+ python-setuptools-scm-7))
+ (arguments
+ (list #:phases #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (setenv "SOURCE_DATE_EPOCH" "315532800")
+ (invoke "python"
+ "-m"
+ "build"
+ "--wheel"
+ "--no-isolation"
+ ".")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((whl (car (find-files "dist" "\\.whl$"))))
+ (invoke "pip"
+ "--no-cache-dir"
+ "--no-input"
+ "install"
+ "--no-deps"
+ "--prefix"
+ #$output
+ whl))))
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ (when tests?
+ (invoke "pytest" "-vvv"))))))) ;)
+ (home-page "https://ofek.dev/projects/hatch/")
+ (synopsis "Plugin for @code{python-hatch} to include versions")
+ (description
+ "This plugin defines a version-control syntax for use with
+@code{toml} files intended for use with @code{python-hatch}.")
+ (license license:expat))))
+
(define-public python-gamera
(package
(name "python-gamera")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:46
[PATCH 07/14] gnu: Add python-pytest-icdiff.
(address . 58310@debbugs.gnu.org)
8735c2qi2r.fsf@disroot.org
Toggle diff (41 lines)
diff --git a/gnu/packages/python-check.scm b/gnu/packages/python-check.scm
index 2358e7448d..6d0885d6dc 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.
;;;
@@ -182,6 +183,26 @@ (define-public python-pytest-csv
it adds to the Pytest command line interface (CLI).")
(license license:gpl3+)))
+(define-public python-pytest-icdiff
+ (package
+ (name "python-pytest-icdiff")
+ (version "0.6")
+ (source (origin
+ (method url-fetch)
+ (uri (pypi-uri "pytest-icdiff" version))
+ (sha256
+ (base32
+ "1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8"))))
+ (build-system python-build-system)
+ (propagated-inputs (list python-pypa-build python-icdiff python-pprintpp))
+ (native-inputs (list python-pytest))
+ (home-page "https://github.com/hjwp/pytest-icdiff")
+ (synopsis "Colored diffs using @code{python-icdiff} for pytest output")
+ (description
+ "This package uses @code{python-icdiff} to add color to the output of
+pytest assertions.")
+ (license (license:non-copyleft "LICENSE"))))
+
(define-public python-testfixtures
(package
(name "python-testfixtures")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:46
[PATCH 08/14] gnu: Add python-hatch-fancy-pypi-readme.
(address . 58310@debbugs.gnu.org)
87zgeap3hx.fsf@disroot.org
Toggle diff (81 lines)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 5739c759de..8ee2da0a07 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -30074,6 +30074,74 @@ (define-public python-style
a port of the chalk package for javascript.")
(license license:expat)))
+(define-public python-hatch-fancy-pypi-readme
+ (package
+ (name "python-hatch-fancy-pypi-readme")
+ (version "22.8.0")
+ (source (origin
+ (method url-fetch)
+ (uri (pypi-uri "hatch_fancy_pypi_readme" version))
+ (sha256
+ (base32
+ "1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx"))))
+ (build-system python-build-system)
+ (propagated-inputs (list python-tomli python-typing-extensions))
+ (native-inputs (list python-pypa-build
+ python-pathspec
+ python-pluggy-1.0
+ python-editables
+ python-hatch
+ python-hatchling-bootstrap
+ python-wheel
+ python-pytest
+ python-pytest-icdiff))
+ (arguments
+ `(#:phases (modify-phases %standard-phases
+ (add-before 'build 'disable-broken-tests
+ (lambda _
+ ;; Skip the tests for "building". Guix already does this,
+ ;; so we don't need to test it for this package.
+ (chdir "tests")
+ (invoke "sed" "-i"
+ "11ipytest.skip('No need to test\
+ building; guix does this already', allow_module_level=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 "Syntax for styling PyPI READMEs")
+ (description
+ "Defines a syntax for the python-hatch build system, intended for styling
+READMEs for PyPI.")
+ (license license:expat)))
+
(define-public python-sre-yield
(package
(name "python-sre-yield")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:47
[PATCH 09/14] gnu: python-jsonschema-next: Update to 4.16.0.
(address . 58310@debbugs.gnu.org)
87wn9ep3hk.fsf@disroot.org
Toggle diff (49 lines)
diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm
index 8ee2da0a07..e1da4386e2 100644
--- a/gnu/packages/python-xyz.scm
+++ b/gnu/packages/python-xyz.scm
@@ -3631,13 +3631,13 @@ (define-public python-jsonschema
(define-public python-jsonschema-next
(package
(inherit python-jsonschema)
- (version "4.5.1")
+ (version "4.16.0")
(source
(origin
(method url-fetch)
(uri (pypi-uri "jsonschema" version))
(sha256
- (base32 "1z0x22691jva7lwfcfh377jdmlz68zhiawxzl53k631l34k8hvbw"))))
+ (base32 "07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11"))))
(arguments
(substitute-keyword-arguments (package-arguments python-jsonschema)
((#:phases phases)
@@ -3655,13 +3655,23 @@ (define-public python-jsonschema-next
(invoke "pip" "--no-cache-dir" "--no-input"
"install" "--no-deps" "--prefix" #$output whl))))))))
(native-inputs (list python-pypa-build
- python-setuptools-scm
- python-twisted))
+ python-twisted
+ python-hatch
+ python-hatchling-bootstrap
+ python-pathspec
+ python-pluggy-1.0
+ python-editables
+ python-hatch-vcs
+ python-setuptools-scm-7
+ python-hatch-fancy-pypi-readme))
(propagated-inputs
(list python-attrs
python-importlib-metadata
python-pyrsistent
- python-typing-extensions))))
+ python-typing-extensions
+ python-hatch-vcs))
+ (home-page
+ "https://github.com/python-jsonschema/jsonschema")))
(define-public python-schema
(package
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:47
[PATCH 10/14] gnu: Add ocaml-atd.
(address . 58310@debbugs.gnu.org)
87tu4ip3h2.fsf@disroot.org
Toggle diff (65 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 4bc159481e..bc876d60a1 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -4955,6 +4955,58 @@ (define-public ocaml-earley
is also support for writing OCaml syntax extensions in a camlp4 style.")
(license license:cecill-b)))
+(define-public ocaml-atd
+ (package
+ (name "ocaml-atd")
+ (version "2.10.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ahrefs/atd")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "10fgahdigrl01py0k0q2d6a60yps38q96dxhjnzm9jz4g931716l"))))
+ (build-system dune-build-system)
+ (arguments
+ `(#:phases (modify-phases %standard-phases
+ (replace 'check
+ (lambda* (#:key tests? #:allow-other-keys)
+ ;; The dune-build-system does not run "make test" but
+ ;; "dune runtest test --release".
+ ;; This project, rather, needs us to run "make test".
+ ;;
+ ;; For this package (ocaml-atd), we DO NOT run all the
+ ;; tests. The atd repository has resources for several
+ ;; different interfaces (python, scala, etc), but we
+ ;; don't need to run those tests if we are just
+ ;; interested in the ocaml interface.
+ ;; So we stick with just the ocaml tests here.
+ (when tests?
+ (invoke "make" "test-ocaml")))))))
+ (propagated-inputs (list ocaml-menhir
+ ocaml-easy-format
+ ocaml-odoc
+ ocaml-re
+ ocaml-camlp-streams
+ ocaml-biniou
+ ocaml-yojson
+ ocaml-cmdliner))
+ (native-inputs (list ocaml-alcotest
+ python-pypa-build
+ python-jsonschema-4.15
+ python-flake8
+ python-mypy
+ python-pytest))
+ (inputs (list python))
+ (home-page "https://github.com/ahrefs/atd")
+ (synopsis "Parser for the ATD data format description language")
+ (description
+ "ATD is an OCaml library providing a parser for the Adjustable Type
+Definitions language.")
+ (license (license:non-copyleft "LICENSE.md"))))
+
(define-public ocaml-timed
(package
(name "ocaml-timed")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:51
[PATCH 11/14] gnu: Add ocaml-elpi.
(address . 58310@debbugs.gnu.org)
87r0zmp3ar.fsf@disroot.org
Toggle diff (61 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index bc876d60a1..641a139e51 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -5007,6 +5007,54 @@ (define-public ocaml-atd
Definitions language.")
(license (license:non-copyleft "LICENSE.md"))))
+(define-public ocaml-elpi
+ (package
+ (name "ocaml-elpi")
+ ;; For more information on which version works with Coq 8.16,
+ ;; see the relevant issue:
+ ;; https://github.com/math-comp/hierarchy-builder/issues/297
+ ;; Here we use
+ ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 +
+ ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16).
+ ;; (version "1.15.2")
+ (version "1.16.5")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/LPCIC/elpi")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ ;; "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy")
+ "1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl"))))
+ (build-system dune-build-system)
+ (arguments
+ `(#:test-target "tests"))
+ ;; Build currently fails with error (repeated several times):
+ ;; 'Warning 6 [labels-omitted: label argsdepth was omitted in the
+ ;; application of this function.'
+ (propagated-inputs (list ocaml-stdlib-shims
+ ocaml-ppxlib
+ ocaml-menhir
+ ocaml-re
+ ocaml-ppx-deriving
+ ocaml-atd
+ ocaml-camlp-streams
+ ocaml-biniou
+ ocaml-yojson))
+ (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
+ (home-page "https://github.com/LPCIC/elpi")
+ (synopsis "ELPI - Embeddable λProlog Interpreter")
+ (description
+ "ELPI is an extension language for OCaml. It implements a variant of
+λProlog enriched with Constraint Handling Rules, a programming language for
+manipulating syntax trees with binders.
+
+This package provides both a command line interpreter, elpi, and an OCaml
+library with the same name.")
+ (license license:lgpl2.1+)))
+
(define-public ocaml-timed
(package
(name "ocaml-timed")
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:51
[PATCH 12/14] gnu: Add coq-elpi.
(address . 58310@debbugs.gnu.org)
87o7uqp3ac.fsf@disroot.org
Toggle diff (82 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 60937af750..313366cb11 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -771,3 +771,75 @@ (define-public coq-mathcomp-bigenough
purposes as @code{bigenough} will be subsumed by the near tactics. The
formalization is based on the Mathematical Components library.")
(license license:cecill-b)))
+
+(define-public coq-elpi
+ (package
+ (name "coq-elpi")
+ ;; For more information on which version works with Coq 8.16,
+ ;; see the relevant issue:
+ ;; https://github.com/math-comp/hierarchy-builder/issues/297
+ ;; Here we use
+ ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 +
+ ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16)
+ (version "1.15.4")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/LPCIC/coq-elpi")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "115ll1g5dyn8z58x7xg6nsliga669875s560j5053flr6cvb8mq1"))))
+ (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)
+ ;; --- old phase from version 1.14.0
+ (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)))))))
+ (propagated-inputs (list ocaml
+ ocaml-stdlib-shims
+ ocaml-elpi
+ ocaml-zarith
+ coq-core
+ coq-stdlib))
+ (inputs (list python))
+ (home-page "https://github.com/LPCIC/coq-elpi")
+ (synopsis "Elpi extension language for Coq")
+ (description
+ "Coq-elpi provides a Coq plugin that embeds ELPI, an extension language
+for OCaml that is an implementation of λProlog. 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. Finally it provides a way to define new vernacular commands
+and new tactics.")
+ (license license:lgpl2.1)))
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:51
[PATCH 13/14] gnu: Add coq-mathcomp-hierarchy-builder.
(address . 58310@debbugs.gnu.org)
87lepup39u.fsf@disroot.org
Toggle diff (72 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 313366cb11..184e503dd5 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -843,3 +843,65 @@ (define-public coq-elpi
Coq's primitives. 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.16,
+ ;; see the relevant issue:
+ ;; https://github.com/math-comp/hierarchy-builder/issues/297
+ ;; Here we use
+ ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 +
+ ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16)
+ (version "1.3.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/math-comp/hierarchy-builder")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "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 interfaces for the Coq system.
+
+Given a structure one can develop its theory, and that theory becomes
+applicable to all examples of the structure. One can also declare alternative
+interfaces, for convenience or backward compatibility, and provide glue code
+linking these interfaces to the structures part of the hierarchy.")
+ (home-page "https://math-comp.github.io/")
+ (license license:expat)))
--
2.37.3
G
G
Garek Dyszel wrote on 5 Oct 2022 19:51
[PATCH 14/14] gnu: Add coq-mathcomp-analysis.
(address . 58310@debbugs.gnu.org)
87ilkyp39g.fsf@disroot.org
Toggle diff (74 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 184e503dd5..f7b4c504f9 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -905,3 +905,67 @@ (define-public coq-mathcomp-hierarchy-builder
linking these interfaces to the structures part of the hierarchy.")
(home-page "https://math-comp.github.io/")
(license license:expat)))
+
+(define-public coq-mathcomp-analysis
+ (package
+ (name "coq-mathcomp-analysis")
+ (version "0.5.4")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/math-comp/analysis")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1l1yaxbmqr4li8x7g51q98a6v383dnf94lw1b74ccpwqz9qybz9m"))))
+ (build-system gnu-build-system)
+ (arguments
+ `( ;No rule to make target 'check'. Stop.
+ ;; Makefile.common has no references to tests.
+ ;; There are also no references to tests found after
+ ;; running the following commands in the top
+ ;; directory of the cloned repo:
+ ;; find -type d | grep -i test
+ ;; rg test # where rg is ripgrep
+ ;; Checking the git log, we find: "Add test suite for
+ ;; joins and several fixes".
+ ;;
+ ;; If tests are included, this quote suggests that they
+ ;; would be part of the source files themselves,
+ ;; and the tests would be run as part of the build
+ ;; process.
+ #:tests? #f
+ #:make-flags ,#~(list (string-append "COQBIN="
+ #$(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))
+ (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.3
G
G
Garek Dyszel wrote on 18 Oct 2022 17:42
Temporary manifest for coq-mathcomp-analysis
(address . 58310@debbugs.gnu.org)
87y1td2l57.fsf@disroot.org
Since the above patch set does not correctly build with Coq 8.16,
here are a manifest file, a channels file, and a package file to get us
through. These files rely on Coq 8.15.2.

I didn't try to clean these files up or anything. They do work for me,
though, until we can figure out how to build coq-mathcomp-analysis for
Coq 8.16. I tested it with Emacs Proof General.

If all files are in the same folder, they can be used by running the
following. (Note also: to get a valid channel for the channels.scm file,
we have to create a dummy git repository.)

$ mkdir mathcomp-extra-packages && cp coq-mathcomp-analysis.scm ./test
$ cd test
$ git init
$ git add coq-mathcomp-analysis.scm
$ git commit "random commit name"
$ cd ../
$ guix time-machine -C ./channels.scm\
-- shell -m guix-manifest.scm -- emacs ./

(One can omit "-- emacs ./" if they just want the packages available,
but want to use a different editor.)

A final note is that if Emacs does not detect the presence of
coq-mathcomp-analysis, it could befixed with the following local
variables.
#+begin_src coq
(* Local Variables: *)
(* mode: coq *)
(* eval: (setq coq-prog-name "coqtop") *)
(* eval: (setq coq-compiler "coqc") *)
(* eval: (setq coq-dependency-analyzer "coqdep") *)
(* End: *)
#+end_src

coq-mathcomp-analysis.scm
Toggle snippet (423 lines)
;;; This module extends GNU Guix and is licensed under the same terms, those
;;; of the GNU GPL version 3 or (at your option) any later version.
;;;
;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>

(define-module (coq-mathcomp-analysis)
#:use-module (guix)
#:use-module (guix git-download)
#:use-module (guix download)
#:use-module (guix packages)
#:use-module (guix build-system gnu)
#:use-module (guix build gnu-build-system)
#:use-module (guix build-system dune)
#:use-module (guix build-system ocaml)
;; #:use-module ((guix build utils) #:prefix utils:)
#:use-module ((guix licenses)
#:prefix license:)
#:use-module ((gnu packages base)
#:prefix base:)
#:use-module (guix build utils)
#:use-module (guix utils)
#:use-module (guix profiles)
#:use-module (gnu packages coq)
#:use-module (gnu packages base)
#:use-module (gnu packages ocaml)
#:use-module (gnu packages time)
#:use-module (gnu packages python)
#:use-module (gnu packages python-xyz)
#:use-module (gnu packages python-build)
#:use-module (gnu packages python-web)
#:use-module (gnu packages python-crypto)
#:use-module (gnu packages xdisorg)
#:use-module (guix build-system python)
#:use-module (gnu packages python-check)
#:use-module (gnu packages check)
#:use-module (gnu packages java)
#:use-module (gnu packages python-compression)
#:use-module (gnu packages version-control))

;; This manifest builds coq-mathcomp-analysis for Coq 8.15.2.

;;; OCaml
(define-public ocaml-elpi
(package
(name "ocaml-elpi")
;; For more information on which version works with Coq 8.15,
;; see the relevant issue:
;; https://github.com/math-comp/hierarchy-builder/issues/297
;; Here we use
;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
;;
;; The package ocaml-elpi@1.16.5 appears to require a different
;; build process.
(version "1.15.2")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/LPCIC/elpi")
(commit (string-append "v" version))
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy"))))
(build-system dune-build-system)
(arguments
`(#:test-target "tests"))
(propagated-inputs (list ocaml-stdlib-shims
ocaml-ppxlib
ocaml-menhir
ocaml-re
ocaml-ppx-deriving
ocaml-atd
ocaml-camlp-streams
ocaml-biniou
ocaml-yojson))
(native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
(home-page "https://github.com/LPCIC/elpi")
(synopsis "ELPI - Embeddable λ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)))

;; Requires python-jsonschema version 4.6.0 to run tests.
;; See https://github.com/ahrefs/atd/issues/306
(define-public ocaml-atd
(package
(name "ocaml-atd")
(version "2.10.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/ahrefs/atd")
(commit version)
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"10fgahdigrl01py0k0q2d6a60yps38q96dxhjnzm9jz4g931716l"))))
(build-system dune-build-system)
(arguments
`(;; The dependency python-jsonschema needs to be at
;; v4.6 in order for the python tests to pass.
;; See https://github.com/ahrefs/atd/issues/306 for more info
;; on that.
;;#:tests? #f
#:phases (modify-phases %standard-phases
(replace 'check
(lambda* (#:key tests? #:allow-other-keys)
;; The dune-build-system does not run "make test" but
;; "dune runtest test --release".
;; This project, rather, needs us to run "make test".
;;
;; For this package (ocaml-atd), we DO NOT run all the
;; tests. The atd repository has resources for several
;; different interfaces (python, scala, etc), but we
;; don't need to run those tests for the ocaml package.
;; So we stick with just the ocaml
;; tests here.
(when tests?
(invoke "make" "test-ocaml")))))))
(propagated-inputs (list ocaml-menhir
ocaml-easy-format
ocaml-odoc
ocaml-re
ocaml-camlp-streams
ocaml-biniou
ocaml-yojson
ocaml-cmdliner))
(native-inputs (list ocaml-alcotest
python
python-pypa-build
python-jsonschema-4.15
python-flake8
python-mypy
python-pytest))
(home-page "https://github.com/ahrefs/atd")
(synopsis "Parser for the ATD data format description language")
(description
"ATD is the OCaml library providing a parser for the ATD language
and various utilities. ATD stands for Adjustable Type Definitions in
reference to its main property of supporting annotations that allow a
good fit with a variety of data formats.")
;; Modified BSD license
(license (license:non-copyleft "LICENSE.md"))))

(define-public ocaml-ansiterminal
(package
(name "ocaml-ansiterminal")
(version "0.8.5")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/Chris00/ANSITerminal")
(commit version)
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"052qnc23vmxp90yympjz9q6lhqw98gs1yvb3r15kcbi1j678l51h"))))
(build-system dune-build-system)
(arguments
`(#:test-target "tests"))
(home-page "https://github.com/Chris00/ANSITerminal")
(synopsis
"Basic control of ANSI compliant terminals and the windows shell")
(description
"ANSITerminal is a module allowing to use the colors and cursor
movements on ANSI terminals.")
;; Variant of the GPL3 which permits
;; static and dynamic linking when producing binary files.
;; In other words, it allows one to link to the library
;; when compiling nonfree software.
(license (license:non-copyleft "LICENSE"))))

;;; Coq
(define-public coq-elpi
(package
(name "coq-elpi")
;; For more information on which version works with Coq 8.15,
;; see the relevant issue:
;; https://github.com/math-comp/hierarchy-builder/issues/297
;; Here we use
;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
(version "1.14.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/LPCIC/coq-elpi")
(commit (string-append "v" version))
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"))))
(build-system gnu-build-system)
(arguments
`(#:make-flags ,#~(list (string-append "COQBIN="
#$(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."
(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)))

(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)))
;; (replace 'check
;; (lambda* (#:key tests? make-flags #:allow-other-keys)
;; (when tests?
;; (apply invoke "make" "test-suite" make-flags))))
)))
(inputs (list coq
coq-core
coq-mathcomp
which
ocaml
coq-elpi
ocaml-elpi))
(synopsis "Hierarchy structures for the Coq proof assistant")
(description
"Hierarchy Builder (HB) provides high level commands to declare a
hierarchy of algebraic structure (or interfaces if you prefer the
glossary of computer science) for the Coq system.

Given a structure one can develop its theory, and that theory becomes
automatically applicable to all the examples of the structure. One can
also declare alternative interfaces, for convenience or backward
compatibility, and provide glue code linking these interfaces to the
structures part of the hierarchy.

HB commands compile down to Coq modules, sections, records, coercions,
canonical structure instances and notations following the packed
classes discipline which is at the core of the Mathematical Components
library. All that complexity is hidden behind a few concepts and a few
declarative Coq commands.")
(home-page "https://math-comp.github.io/")
;; MIT license
(license license:expat)))

(define-public coq-mathcomp-finmap
(package
(name "coq-mathcomp-finmap")
(version "1.5.2")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/math-comp/finmap")
(commit version)
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh"))))
(build-system gnu-build-system)
(arguments
`( ;"No rule to make target 'check'."
;; No tests supplied in Makefile.common.
;; The project doesn't appear to have plans to include tests in
;; the future.
#:tests? #f
#:make-flags (list (string-append "COQLIBINSTALL="
(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)))

(define-public coq-mathcomp-bigenough
;; On the homepage, it is mentio
This message was truncated. Download the full message here.
Z
Z
zimoun wrote on 2 Nov 2022 18:08
Re: [bug#58310] [PATCH 03/14] gnu: Add python-setuptools-scm-7.
87sfj1cmi7.fsf@gmail.com
Hi,

CC: python team

On mer., 05 oct. 2022 at 13:41, Garek Dyszel via Guix-patches via <guix-patches@gnu.org> wrote:

Toggle quote (5 lines)
> +(define-public python-setuptools-scm-7
> + (package
> + (inherit python-setuptools-scm)
> + (version "7.0.5")

The issue with this is then

guix install python python-setuptools-scm

will install python-setuptools-scm@7 and not the current one at 6.3.2.
Since I am not an expert on this setuptools_scm, the question is: is it
an issue? For instance, it can be for python-numpy so the term ’-next’
is appended to the name.

Here, we could also append ’-next’, WDYT?

Cheers,
simon
Z
Z
zimoun wrote on 2 Nov 2022 18:11
Re: [bug#58310] [PATCH 04/14] gnu: Add python-hatchling-bootstrap.
87leotcmdd.fsf@gmail.com
Hi,

CC: python team

On mer., 05 oct. 2022 at 13:41, Garek Dyszel via Guix-patches via <guix-patches@gnu.org> wrote:
Toggle quote (45 lines)
> * gnu/packages/python-build.scm (python-hatchling-bootstrap): New variable.
> ---
> gnu/packages/python-build.scm | 63 +++++++++++++++++++++++++++++++++++
> 1 file changed, 63 insertions(+)
>
> diff --git a/gnu/packages/python-build.scm b/gnu/packages/python-build.scm
> index e17cde16d9..f90d23874f 100644
> --- a/gnu/packages/python-build.scm
> +++ b/gnu/packages/python-build.scm
> @@ -516,3 +516,66 @@ (define-public python-editables
> ``editable mode''. In other words, changes to the package source will be
> reflected in the package visible to Python, without needing a reinstall.")
> (license license:expat)))
> +
> +;; This depends on packages in python-xyz.scm:
> +;; python-version, python-importlib-metadata, python-pathspec,
> +;; python-pluggy-1.0, and python-platformdirs.
> +(define-public python-hatchling-bootstrap
> + (package
> + (name "python-hatchling-bootstrap")
> + (version "1.10.0")
> + (source (origin
> + (method git-fetch)
> + (uri (git-reference
> + (url "https://github.com/pypa/hatch")
> + (commit (string-append "hatchling-v" version))))
> + (file-name (git-file-name name version))
> + (sha256
> + (base32
> + ;;"1q25kqw71g8mjwfjz9ph0iigdqa26zzxgmqm0v0bp0z1j8rcl237"
> + "1yqkwck2aihfdm9ljv5q4nygmmqyp35xwyp8lqn2f4vq9p6njq3c"))))
> + ;; python-pypa-build needed for bootstrapping.
> + ;; Otherwise we get a circular reference:
> + ;; python-hatchling trying to build itself, without
> + ;; first having hatchling installed.
> + (inputs (list python-pypa-build
> + python-editables
> + python-importlib-metadata
> + python-version
> + python-packaging-next
> + python-pathspec
> + python-pluggy-1.0 ;TODO: Not detected by pytest?
> + python-tomli
> + python-platformdirs))

The issue here is that many dependencies are from the module (gnu
packages python-xyz). Well, moving this python-hatchling-bootstrap and
the next patch adding python-hatch to python-xyz does not look like the
correct home. And dragging these dependencies to python-build neither.

What could be the best solution here?


Cheers,
simon
L
L
Lars-Dominik Braun wrote on 3 Nov 2022 10:22
Re: [bug#58310] [PATCH 03/14] gnu: Add python-setuptools-scm-7.
(name . zimoun)(address . zimon.toutoune@gmail.com)
Y2OIVxwfZw0dpWw7@philomena
Hi,

Toggle quote (3 lines)
> Since I am not an expert on this setuptools_scm, the question is: is it
> an issue? For instance, it can be for python-numpy so the term ’-next’
> is appended to the name.
as long as setuptools_scm’s dependencies are compatible and it does
not break current behavior – I don’t see any breaking changes in
the ChangeLog – the -next is not justified imo.

Lars
L
L
Lars-Dominik Braun wrote on 3 Nov 2022 10:26
Re: [bug#58310] [PATCH 04/14] gnu: Add python-hatchling-bootstrap.
(name . zimoun)(address . zimon.toutoune@gmail.com)
Y2OJNPeY2AjATign@philomena
Hi,

Toggle quote (4 lines)
> The issue here is that many dependencies are from the module (gnu
> packages python-xyz). Well, moving this python-hatchling-bootstrap and
> the next patch adding python-hatch to python-xyz does not look like the
> correct home. And dragging these dependencies to python-build neither.
I think hatchling can go to python-build, since it
contains a PEP 517 build system, but hatchling should go to
python-xyz. python-hatchling-bootstrap should not be used anywhere,
but build a proper python-hatchling instead. Also hatchling has no
dependencies. These are for hatch.

The entire patchset should also use the pyproject build system where possible.

Lars
Z
Z
zimoun wrote on 3 Nov 2022 12:14
Re: [bug#58310] [PATCH 03/14] gnu: Add python-setuptools-scm-7.
(name . Lars-Dominik Braun)(address . lars@6xq.net)
867d0cb87o.fsf@gmail.com
Hi Lars,

On Thu, 03 Nov 2022 at 18:22, Lars-Dominik Braun <lars@6xq.net> wrote:

Toggle quote (8 lines)
>> Since I am not an expert on this setuptools_scm, the question is: is it
>> an issue? For instance, it can be for python-numpy so the term ’-next’
>> is appended to the name.
>
> as long as setuptools_scm’s dependencies are compatible and it does
> not break current behavior – I don’t see any breaking changes in
> the ChangeLog – the -next is not justified imo.

The update of python-setuptools-scm from 6 to 7 is not possible without
going via core-updates, no?

Toggle snippet (4 lines)
$ guix refresh -l python-setuptools-scm | cut -f1 -d':'
Building the following 2406 packages would ensure 5564 dependent packages are rebuilt

Therefore, there are only two options for the patchset:

1. try to build the patchset using the current v6 of python-setuptools-scm
or
2. add v7 as a separated package

I have not tried #1. About #2, if the name of this new package is not
tweaked, then it can be confusing to get v7 at the command line (or
specifications->manifest) when all the other Python stack is built using
v6; even if there is no incompatibilities between v6 and v7 according to
upstream notes.

Well, so you opinion is to keep the name for v7 as it is, right?


Cheers,
simon
Z
Z
zimoun wrote on 3 Nov 2022 12:18
Re: [bug#58310] [PATCH 04/14] gnu: Add python-hatchling-bootstrap.
(name . Lars-Dominik Braun)(address . lars@6xq.net)
86zgd89thp.fsf@gmail.com
Hi,

On Thu, 03 Nov 2022 at 18:26, Lars-Dominik Braun <lars@6xq.net> wrote:

Toggle quote (10 lines)
>> The issue here is that many dependencies are from the module (gnu
>> packages python-xyz). Well, moving this python-hatchling-bootstrap and
>> the next patch adding python-hatch to python-xyz does not look like the
>> correct home. And dragging these dependencies to python-build neither.
> I think hatchling can go to python-build, since it
> contains a PEP 517 build system, but hatchling should go to
> python-xyz. python-hatchling-bootstrap should not be used anywhere,
> but build a proper python-hatchling instead. Also hatchling has no
> dependencies. These are for hatch.

Lars, I am sorry I am missed your advice about what is going where. Is
your point to revamp a bit the bootstrap and put all in python-xyz?

Toggle quote (2 lines)
> The entire patchset should also use the pyproject build system where possible.

Garek, do you want to give a try?


Cheers,
simon
L
L
Lars-Dominik Braun wrote on 3 Nov 2022 12:57
Re: [bug#58310] [PATCH 03/14] gnu: Add python-setuptools-scm-7.
(name . zimoun)(address . zimon.toutoune@gmail.com)
Y2Osj3fA7T9kxb0U@philomena
Hi zimoun,

Toggle quote (2 lines)
> The update of python-setuptools-scm from 6 to 7 is not possible without
> going via core-updates, no?
it’s just an addition and not replacing the current setuptools-scm,
if I see correctly.

Cheers,
Lars
L
L
Lars-Dominik Braun wrote on 3 Nov 2022 12:59
Re: [bug#58310] [PATCH 04/14] gnu: Add python-hatchling-bootstrap.
(name . zimoun)(address . zimon.toutoune@gmail.com)
Y2OtLVz4g58X71DY@philomena
Hi,

Toggle quote (8 lines)
> > I think hatchling can go to python-build, since it
> > contains a PEP 517 build system, but hatchling should go to
> > python-xyz. python-hatchling-bootstrap should not be used anywhere,
> > but build a proper python-hatchling instead. Also hatchling has no
> > dependencies. These are for hatch.
>
> Lars, I am sorry I am missed your advice about what is going where. Is
> your point to revamp a bit the bootstrap and put all in python-xyz?
sorry, misstyped. hatchling -> python-build.scm, hatch ->
python-xyz.scm. And hatchling’s dependencies actually belong to hatch,
not hatchling, so there should be no cycles with python-xyz.scm.

Cheers,
Lars
Z
Z
zimoun wrote on 3 Nov 2022 19:34
Re: [bug#58310] [PATCH 03/14] gnu: Add python-setuptools-scm-7.
(name . Lars-Dominik Braun)(address . lars@6xq.net)
87r0yjanuh.fsf@gmail.com
Hi Lars,

On jeu., 03 nov. 2022 at 20:57, Lars-Dominik Braun <lars@6xq.net> wrote:

Toggle quote (6 lines)
>> The update of python-setuptools-scm from 6 to 7 is not possible without
>> going via core-updates, no?
>
> it’s just an addition and not replacing the current setuptools-scm,
> if I see correctly.

Yes, so “guix install python-setuptools-scm” will install v7 and not the
version v6 used by default. And it can be confusing, IMHO.


Cheers,
simon
L
L
Lars-Dominik Braun wrote on 4 Nov 2022 01:44
(name . zimoun)(address . zimon.toutoune@gmail.com)
Y2Rgbv46ZwDBTTIb@philomena
Hi zimoun,

Toggle quote (2 lines)
> Yes, so “guix install python-setuptools-scm” will install v7 and not the
> version v6 used by default. And it can be confusing, IMHO.
yep, that’s unfortunate but how `guix install` works. It’d be nice
to be able to designate a “default” package. In this case I don’t
see a danger for breakage and setuptools-scm is afaik only a build-time
dependency.

Cheers,
Lars
G
G
Garek Dyszel wrote on 4 Nov 2022 16:15
Re: [bug#58310] [PATCH 04/14] gnu: Add python-hatchling-bootstrap.
(name . Lars-Dominik Braun)(address . lars@6xq.net)
87cza2rbru.fsf@disroot.org
Hi Lars,

At 20:59 2022-11-03 UTC+0900, Lars-Dominik Braun wrote:
Toggle quote (3 lines)
> And hatchling’s dependencies actually belong to hatch,
> not hatchling, so there should be no cycles with python-xyz.scm.

It seems dependencies from python-xyz.scm are still required to enter
the build process for python-hatchling-bootstrap, even if hatchling does
not explicitly require them.

(1) If we comment out the dependencies from python-xyz.scm, we get this
error:
Toggle snippet (8 lines)
starting phase `build'
* Getting dependencies for wheel...

ERROR Missing dependencies:
pathspec>=0.10.1
pluggy>=1.0.0

(2) If we minimize the dependency list to the following, then
python-hatchling-bootstrap builds correctly:
Toggle snippet (8 lines)
(inputs (list python-editables
python-packaging-bootstrap
;; Below from python-xyz.scm, can be moved to python-build.scm
python-pathspec-0.10.1
;; Below from python-xyz.scm, can be moved to python-build.scm
python-pluggy-1.0
python-tomli))
Changing the build system to (pyproject-build-system) produces the same
results.

Since python-pluggy-1.0 and python-pathspec depend only on packages
defined in python-build.scm, I propose moving them to python-build.scm.

What do you think?

Garek

---
Revised python-hatchling-boostrap definition (in case it is of
interest):
Toggle snippet (68 lines)
(define-public python-hatchling-bootstrap
(package
(name "python-hatchling-bootstrap")
(version "1.10.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/pypa/hatch")
(commit (string-append "hatchling-v" version))))
(file-name (git-file-name name version))
(sha256
(base32
"0ahx62w711a2vnb91ahqxrw8yi0gq0kfch3fk6akzngd13376czj"))))
;; python-pypa-build needed for bootstrapping.
;; Otherwise we get a circular reference:
;; python-hatchling trying to build itself, without
;; first having hatchling installed.
(inputs (list python-editables
python-packaging-bootstrap
;; Below from python-xyz.scm, can be moved to python-build.scm
python-pathspec-0.10.1
;; Below from python-xyz.scm, can be moved to python-build.scm
python-pluggy-1.0
python-tomli))
(build-system pyproject-build-system)
(arguments
`(;; Tests depend on module python-hatch, which this
;; is bootstrapping.
#:tests? #f
#:phases
;; Test for pyproject-build-system. This pre-build phase fails.
;;
;; (modify-phases %standard-phases
;; (add-before 'build 'chdir-to-backend
;; (lambda _
;; (chdir "backend"))))
;;
;; Original phases.
(modify-phases %standard-phases
(replace 'build
(lambda _
(chdir "backend")
;; ZIP does not support timestamps before 1980.
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "python"
"-m"
"build"
"--wheel"
"--no-isolation"
".")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
(assoc-ref %outputs "out")
whl)))))))
(home-page "https://ofek.dev/projects/hatch/")
(synopsis "Bootstrap binaries to build @code{python-hatch}")
(description "Bootstrap binaries to build @code{python-hatch}")
;; MIT License
(license license:expat)))
G
G
Garek Dyszel wrote on 13 Nov 2022 00:48
Manifest for coq-mathcomp-analysis
87v8njspi5.fsf@disroot.org
Hi,

CC: ocaml team

I am including a manifest file instead of sending patches for now. It
seems like a good idea to stick with that until these packages are ready
to be put into the Guix source tree. I'm refactoring them too often.

After opening an issue on Github [1] [2], it seems that coq-elpi is the
package that is not building properly. It is clear that ocamlfind (from
ocaml-findlib) can't find coq-elpi after coq-elpi's install phase.

It looks like the META file is not being installed by coq-elpi either.
I'm not sure whether that's relevant, since ocamlfind couldn't find
coq-elpi even when META was present (in a much older revision of this
manifest; I can dig for it but just today don't have time).

The problem seems to be something in the build process itself; if the
extra phase 'check-findlib-path' is omitted then coq-elpi's build is
reported as a success.

The later package coq-mathcomp-hierarchy-builder runs ocamlfind to find
coq-elpi, too.

What would be a way to ensure that coq-elpi is found by ocamlfind?

Thanks!
Garek

(Manifest attached with an ocaml-elpi patch. You will need to change the path for
the ocaml-elpi (patches) field to match your directory structure, but otherwise
this manifest should work.)
J
J
Julien Lepiller wrote on 13 Nov 2022 10:17
(name . pukkamustard)(address . pukkamustard@posteo.net)
A2D9782B-4542-4403-B078-51C3A2BD7640@lepiller.eu
Hi!

I tried building your file (it's technically not a manifest) and indeed it's failing in the chack-findlib-path.

Why do you want to run it? There's no way it could work at this point, right after the check phase, since the package is not even installed yet. Also, the OCAMLPATH that would allow findlib to find it is not set to the outputs, only to the inputs.

Le 13 novembre 2022 00:48:50 GMT+01:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
Toggle quote (35 lines)
>Hi,
>
>CC: ocaml team
>
>I am including a manifest file instead of sending patches for now. It
>seems like a good idea to stick with that until these packages are ready
>to be put into the Guix source tree. I'm refactoring them too often.
>
>After opening an issue on Github [1] [2], it seems that coq-elpi is the
>package that is not building properly. It is clear that ocamlfind (from
>ocaml-findlib) can't find coq-elpi after coq-elpi's install phase.
>[1]: https://github.com/math-comp/hierarchy-builder/issues/320
>[2]: https://github.com/LPCIC/coq-elpi/issues/384
>
>It looks like the META file is not being installed by coq-elpi either.
>I'm not sure whether that's relevant, since ocamlfind couldn't find
>coq-elpi even when META was present (in a much older revision of this
>manifest; I can dig for it but just today don't have time).
>
>The problem seems to be something in the build process itself; if the
>extra phase 'check-findlib-path' is omitted then coq-elpi's build is
>reported as a success.
>
>The later package coq-mathcomp-hierarchy-builder runs ocamlfind to find
>coq-elpi, too.
>
>What would be a way to ensure that coq-elpi is found by ocamlfind?
>
>Thanks!
>Garek
>
>(Manifest attached with an ocaml-elpi patch. You will need to change the path for
>the ocaml-elpi (patches) field to match your directory structure, but otherwise
>this manifest should work.)
>
Attachment: file
J
J
Julien Lepiller wrote on 13 Nov 2022 11:53
Re: [bug#58310] Manifest for coq-mathcomp-analysis
(name . pukkamustard)(address . pukkamustard@posteo.net)
20221113115303.66ccb071@sybil.lepiller.eu
So, I've had a further look at the sources for the failing packages and
figured that some variables were missing in the make-flags. Attached is
the fixed version of your file that builds coq-mathcomp-analysis. Note
that the build of mathcomp-analysis is very quiet and takes a long time,
but it works eventually.

Le Sun, 13 Nov 2022 10:17:07 +0100,
Julien Lepiller <julien@lepiller.eu> a écrit :

Toggle quote (50 lines)
> Hi!
>
> I tried building your file (it's technically not a manifest) and
> indeed it's failing in the chack-findlib-path.
>
> Why do you want to run it? There's no way it could work at this
> point, right after the check phase, since the package is not even
> installed yet. Also, the OCAMLPATH that would allow findlib to find
> it is not set to the outputs, only to the inputs.
>
> Le 13 novembre 2022 00:48:50 GMT+01:00, Garek Dyszel
> <garekdyszel@disroot.org> a écrit :
> >Hi,
> >
> >CC: ocaml team
> >
> >I am including a manifest file instead of sending patches for now. It
> >seems like a good idea to stick with that until these packages are
> >ready to be put into the Guix source tree. I'm refactoring them too
> >often.
> >
> >After opening an issue on Github [1] [2], it seems that coq-elpi is
> >the package that is not building properly. It is clear that
> >ocamlfind (from ocaml-findlib) can't find coq-elpi after coq-elpi's
> >install phase. [1]:
> >https://github.com/math-comp/hierarchy-builder/issues/320 [2]:
> >https://github.com/LPCIC/coq-elpi/issues/384
> >
> >It looks like the META file is not being installed by coq-elpi
> >either. I'm not sure whether that's relevant, since ocamlfind
> >couldn't find coq-elpi even when META was present (in a much older
> >revision of this manifest; I can dig for it but just today don't
> >have time).
> >
> >The problem seems to be something in the build process itself; if the
> >extra phase 'check-findlib-path' is omitted then coq-elpi's build is
> >reported as a success.
> >
> >The later package coq-mathcomp-hierarchy-builder runs ocamlfind to
> >find coq-elpi, too.
> >
> >What would be a way to ensure that coq-elpi is found by ocamlfind?
> >
> >Thanks!
> >Garek
> >
> >(Manifest attached with an ocaml-elpi patch. You will need to change
> >the path for the ocaml-elpi (patches) field to match your directory
> >structure, but otherwise this manifest should work.)
> >
G
G
Garek Dyszel wrote on 13 Nov 2022 19:54
(name . pukkamustard)(address . pukkamustard@posteo.net)
87tu32eldg.fsf@disroot.org
I'm in UTC-0400, so your first email arrived in my inbox at around
04:00. Sorry I didn't see these!

At 10:17 2022-11-13 UTC+0100, Julien Lepiller wrote:
Toggle quote (3 lines)
>> I tried building your file (it's technically not a manifest) and
>> indeed it's failing in the chack-findlib-path.

You're right that it's not a manifest. I had put a (packages->manifest)
invocation at the end of the file to see why coq-elpi wasn't building.
Later I just threw a package at the end when testing it later, and
forgot that the file then became a package file.

Toggle quote (2 lines)
>> Why do you want to run it?

I knew that ocamlfind wasn't able to find the file coq-elpi.elpi when
building coq-mathcomp-hierarchy-builder. I was trying to test for the
presence of that file...

Toggle quote (3 lines)
>> There's no way it could work at this point, right after the check
>> phase, since the package is not even installed yet.

...and I thought that the phase 'check' came after the phase 'install'
for some reason :/

Toggle quote (3 lines)
>> Also, the OCAMLPATH that would allow findlib to find it is not set to
>> the outputs, only to the inputs.

Looks like I'll need to take a closer look at ocaml-build-system!

At 11:53 2022-11-13 UTC+0100, Julien Lepiller wrote:
Toggle quote (3 lines)
> So, I've had a further look at the sources for the failing packages
> and figured that some variables were missing in the make-flags.

Tweaking the make-flags is exactly what's been occupying my time for the
last few months off and on, yep :)

Toggle quote (3 lines)
> Attached is the fixed version of your file that builds
> coq-mathcomp-analysis.

Wow! Thanks so much! I can finally move to using it instead of building
it, although trying to get it to build was still a lot of fun :)

Toggle quote (3 lines)
> Note that the build of mathcomp-analysis is
> very quiet and takes a long time, but it works eventually.

For anybody else who might be reading this thread, it took about 12
minutes to build on my system. I ran 'guix gc' beforehand to get an
accurate number:
$ until guix gc && time guix build -Kf coq-mathcomp-analysis.scm;\
$ do sleep 0.1; done
...

real 11m18.769s
user 0m7.332s
sys 0m0.490s

Out of curiosity, where did you put the patch file so that (patches
(search-patches "ocaml-elpi-fix-yojson.patch")) worked? My system throws
this error, so I had to switch the patch's path back: "guix build:
error: ocaml-elpi-fix-yojson.patch: patch not found".
J
J
Julien Lepiller wrote on 13 Nov 2022 20:40
(name . pukkamustard)(address . pukkamustard@posteo.net)
C693105D-9179-4B5B-81BA-AE12CC358739@lepiller.eu
There's a trick for patches: they are loaded from the search path, so you can add the file to any empty directory and add that directory to the load path.

For instance, if you have ~/guix-patches/my.patch, then you can build a package that looks for my.patch with:

guix build -L ~/guix-patches

Le 13 novembre 2022 19:54:03 GMT+01:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
Toggle quote (61 lines)
>I'm in UTC-0400, so your first email arrived in my inbox at around
>04:00. Sorry I didn't see these!
>
>At 10:17 2022-11-13 UTC+0100, Julien Lepiller wrote:
>>> I tried building your file (it's technically not a manifest) and
>>> indeed it's failing in the chack-findlib-path.
>
>You're right that it's not a manifest. I had put a (packages->manifest)
>invocation at the end of the file to see why coq-elpi wasn't building.
>Later I just threw a package at the end when testing it later, and
>forgot that the file then became a package file.
>
>>> Why do you want to run it?
>
>I knew that ocamlfind wasn't able to find the file coq-elpi.elpi when
>building coq-mathcomp-hierarchy-builder. I was trying to test for the
>presence of that file...
>
>>> There's no way it could work at this point, right after the check
>>> phase, since the package is not even installed yet.
>
>...and I thought that the phase 'check' came after the phase 'install'
>for some reason :/
>
>>> Also, the OCAMLPATH that would allow findlib to find it is not set to
>>> the outputs, only to the inputs.
>
>Looks like I'll need to take a closer look at ocaml-build-system!
>
>At 11:53 2022-11-13 UTC+0100, Julien Lepiller wrote:
>> So, I've had a further look at the sources for the failing packages
>> and figured that some variables were missing in the make-flags.
>
>Tweaking the make-flags is exactly what's been occupying my time for the
>last few months off and on, yep :)
>
>> Attached is the fixed version of your file that builds
>> coq-mathcomp-analysis.
>
>Wow! Thanks so much! I can finally move to using it instead of building
>it, although trying to get it to build was still a lot of fun :)
>
>> Note that the build of mathcomp-analysis is
>> very quiet and takes a long time, but it works eventually.
>
>For anybody else who might be reading this thread, it took about 12
>minutes to build on my system. I ran 'guix gc' beforehand to get an
>accurate number:
>$ until guix gc && time guix build -Kf coq-mathcomp-analysis.scm;\
>$ do sleep 0.1; done
>...
>
>real 11m18.769s
>user 0m7.332s
>sys 0m0.490s
>
>Out of curiosity, where did you put the patch file so that (patches
>(search-patches "ocaml-elpi-fix-yojson.patch")) worked? My system throws
>this error, so I had to switch the patch's path back: "guix build:
>error: ocaml-elpi-fix-yojson.patch: patch not found".
>
Attachment: file
?
Your comment

Commenting via the web interface is currently disabled.

To comment on this conversation send an email to 58310@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 58310
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch