[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#58310] Temporary manifest for coq-mathcomp-analysis
|
From: |
Garek Dyszel |
|
Subject: |
[bug#58310] Temporary manifest for coq-mathcomp-analysis |
|
Date: |
Tue, 18 Oct 2022 11:42:44 -0400 |
Since the above patch set does not correctly build with Coq 8.16,
here are a manifest file, a channels file, and a package file to get us
through. These files rely on Coq 8.15.2.
I didn't try to clean these files up or anything. They do work for me,
though, until we can figure out how to build coq-mathcomp-analysis for
Coq 8.16. I tested it with Emacs Proof General.
If all files are in the same folder, they can be used by running the
following. (Note also: to get a valid channel for the channels.scm file,
we have to create a dummy git repository.)
$ mkdir mathcomp-extra-packages && cp coq-mathcomp-analysis.scm ./test
$ cd test
$ git init
$ git add coq-mathcomp-analysis.scm
$ git commit "random commit name"
$ cd ../
$ guix time-machine -C ./channels.scm\
-- shell -m guix-manifest.scm -- emacs ./
(One can omit "-- emacs ./" if they just want the packages available,
but want to use a different editor.)
A final note is that if Emacs does not detect the presence of
coq-mathcomp-analysis, it could befixed with the following local
variables.
#+begin_src coq
(* Local Variables: *)
(* mode: coq *)
(* eval: (setq coq-prog-name "coqtop") *)
(* eval: (setq coq-compiler "coqc") *)
(* eval: (setq coq-dependency-analyzer "coqdep") *)
(* End: *)
#+end_src
coq-mathcomp-analysis.scm
--8<---------------cut here---------------start------------->8---
;;; This module extends GNU 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 mentioned that coq-mathcomp-bigenough
;; is going to be obsolete sometime in the near future.
;; This package was included because of the following error,
;; encountered while building coq-mathcomp-analysis:
;; "Warning: in file theories/altreals/realseq.v, library
;; mathcomp.bigenough.bigenough is required and has not been
;; found in the loadpath!"
;; So added https://github.com/math-comp/bigenough.
(package
(name "coq-mathcomp-bigenough")
(version "1.0.1")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/math-comp/bigenough";)
(commit version)
(recursive? #t)))
(file-name (git-file-name name version))
(sha256
(base32
"02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
(build-system gnu-build-system)
(arguments
`( ;"No rule to make target 'test'. Stop."
;; No references to tests in Makefile.common.
;; It doesn't appear as though tests will be included
;; by the packaged project in the future.
#:tests? #f
#:make-flags ,#~(list (string-append "COQBIN="
#$(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)))
(define-public coq-mathcomp-analysis
(package
(name "coq-mathcomp-analysis")
;;(version "0.5.3")
(version "0.5.4")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/math-comp/analysis";)
(commit version)))
(file-name (git-file-name name version))
(sha256
(base32
;; hash for v0.5.3
;;"16bv2kxm6nrgfm9lp88sls1vqs26d4m3fxbccmy328ak5srcbn6l"
;; hash for v0.5.4
"1l1yaxbmqr4li8x7g51q98a6v383dnf94lw1b74ccpwqz9qybz9m"
))))
(build-system gnu-build-system)
(arguments
`( ;No rule to make target 'check'. Stop.
;; Makefile.common has no references to tests.
;; There are also no references to tests found after
;; running the following commands in the top
;; directory of the cloned repo:
;; find -type d | grep -i test
;; rg test
;; Checking the git log, we find: "Add test suite for
;; joins and several fixes".
;;
;; If tests are included, this quote suggests that they
;; would be part of the source files themselves,
;; and the tests would be run as part of the build
;; process.
#:tests? #f
#:make-flags ,#~(list (string-append "COQBIN="
#$(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)
(apply invoke "make" make-flags)
)))))
(inputs (list coq
coq-stdlib
coq-mathcomp
coq-mathcomp-finmap
coq-mathcomp-hierarchy-builder
coq-elpi
coq-mathcomp-bigenough
coq-core
which
python))
(synopsis "Real analysis for the Coq proof assistant")
(description
"This repository contains an experimental library for
real analysis for the Coq proof-assistant, using the Mathematical
Components library.")
(home-page "https://math-comp.github.io/";)
(license license:cecill-c)))
;;; Python
;; (define-public python-import-everything
;; (package
;; (name "python-import-everything")
;; (version "0.0.1")
;; (source (origin
;; (method url-fetch)
;; (uri (pypi-uri "import-everything" version))
;; (sha256
;; (base32
;; "1cq45i421bksg2lwwf5xddp30v0z95qzh2g6dxi1ky989lgxvlv3"))))
;; (build-system python-build-system)
;; (inputs (list python python-pypa-build python-pytest))
;; (arguments
;; (substitute-keyword-arguments (package-arguments python-jsonschema)
;; ((#:phases phases)
;; #~(modify-phases #$phases
;; (replace 'build
;; (lambda _
;; ;; ZIP does not support timestamps 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" #$output whl))))
;; ))))
;; (home-page "https://github.com/profMagija/everything";)
;; (synopsis "A module containing everything")
;; (description "This package provides a module containing everything")
;; (license #f)))
(define-public python-version
;; No version tags available; just using bare commit instead.
(let ((commit "5232eea250ab72cc5cb72b0b75efb35d2192b906"))
(package
(name "python-python-version")
(version "0.0.2")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://gitlab.com/halfak/python_version";)
(commit commit)))
(sha256
(base32
"0w210559ypdynlj9yn40m9awzkaknwrf682i99hswl7h66sdgh0h"))))
(build-system python-build-system)
(home-page "https://gitlab.com/halfak/python_version";)
(synopsis "Provides a simple utility for checking the python version.")
(description
"This package provides a simple utility for checking the python
version.")
;; MIT License
(license license:expat))))
(define-public python-editables
(package
(name "python-editables")
(version "0.3")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/pfmoore/editables";)
(commit version)))
(sha256
(base32
"1gbfkgzmrmbd4ycshm09fr2wd4f1n9gq7s567jgkavhfkn7s2pn1"))))
(build-system python-build-system)
(home-page "https://github.com/pfmoore/editables";)
(synopsis "Editable installations")
(description "Editable installations")
(license license:expat)))
(define-public python-pluggy-1.0
(package
(inherit python-pluggy)
(name "python-pluggy-1.0")
(version "1.0.0")
(source (origin
;; Won't build from github tarballs, throws error:
;; "LookupError: setuptools-scm was unable to detect version for
'/tmp/guix-build-python-pluggy-1.0-1.0.0.drv-0/source'."
(method url-fetch)
(uri (pypi-uri "pluggy" version))
(sha256
(base32
"0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922"))))
(inputs (list python
python-pypa-build
python-pytest
python-setuptools-scm
python-setuptools
python-wheel))))
;; (define-public python-hatch-vcs
;; ;; Tags are messed up; just use the commit itself.
;; (let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2"))
;; (package
;; (name "python-hatch-vcs")
;; (version "0.2.0")
;; (source (origin
;; (method git-fetch)
;; (uri (git-reference
;; (url "https://github.com/ofek/hatch-vcs";)
;; (commit commit)))
;; (sha256
;; (base32
;; "0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05"))))
;; (build-system python-build-system)
;; (inputs (list python
;; python-pypa-build
;; python-pathspec-0.10.1
;; python-pluggy-1.0
;; python-editables
;; python-pytest
;; git))
;; (propagated-inputs (list python-hatchling-bootstrap
python-setuptools-scm-7)) ;python-setuptools-scm-6.4 minimum
;; (arguments
;; (substitute-keyword-arguments (package-arguments python-jsonschema)
;; ((#:phases phases)
;; #~(modify-phases #$phases
;; (replace 'build
;; (lambda _
;; (setenv "SOURCE_DATE_EPOCH" "315532800")
;; (invoke "python"
;; "-m"
;; "build"
;; "--wheel"
;; "--no-isolation"
;; ".")))
;; (replace 'install
;; (lambda* (#:key outputs #:allow-other-keys)
;; (let ((whl (car (find-files "dist" "\\.whl$"))))
;; (invoke "pip"
;; "--no-cache-dir"
;; "--no-input"
;; "install"
;; "--no-deps"
;; "--prefix"
;; #$output
;; whl))))
;; (replace 'check
;; (lambda* (#:key tests? #:allow-other-keys)
;; (when tests?
;; (invoke "pytest" "-vvv"))))))))
;; (home-page "")
;; (synopsis "Hatch plugin for versioning with your preferred VCS")
;; (description "Hatch plugin for versioning with your preferred VCS")
;; (license #f))))
(define-public python-setuptools-scm-7
;; Another broken python release. Ugh.
(let ((commit "c4d37004ab0a16c2cacdc58ef06b36956db02a9f"))
(package
(name "python-setuptools-scm")
(version "7.0.5")
(source (origin
;; Won't build with git. Fails with error:
;; "ERROR Backend subproccess exited when trying to invoke
;; get_requires_for_build_wheel"
(method url-fetch)
(uri (pypi-uri "setuptools_scm" version))
(sha256
(base32
"0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3"))
))
(build-system python-build-system)
(propagated-inputs (list python-importlib-metadata python-packaging
python-setuptools python-tomli
python-typing-extensions))
(native-inputs (list python
python-pypa-build
python-pytest
python-virtualenv
git-minimal
mercurial))
(home-page "https://github.com/pypa/setuptools_scm/";)
(synopsis "the blessed package to manage your versions by scm tags")
(description "the blessed package to manage your versions by scm tags")
(license license:expat))))
(define-public python-pprintpp
;; Another broken python version
(let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0"))
(package
(name "python-pprintpp")
(version "0.3.0")
(source (origin
;; No version given in the github repo
;; https://github.com/wolever/pprintpp.
(method git-fetch)
(uri (git-reference
(url "https://github.com/wolever/pprintpp";)
(commit commit)))
(sha256
(base32
"0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li"))
))
(inputs (list python
python-pypa-build
python-pytest
python-hypothesis
python-setuptools
python-wheel
python-nose
python-parameterized))
(build-system python-build-system)
(arguments
(substitute-keyword-arguments (package-arguments python-jsonschema)
((#:phases phases)
#~(modify-phases #$phases
(replace 'build
(lambda _
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "python"
"-m"
"build"
"--wheel"
"--no-isolation"
".")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
#$output
whl))))
(replace 'check
(lambda* (#:key tests? #:allow-other-keys)
(when tests?
(invoke "python" "test.py"))))))))
(home-page "https://github.com/wolever/pprintpp";)
(synopsis "A drop-in replacement for pprint that's actually pretty")
(description
"This package provides a drop-in replacement for pprint that's actually
pretty")
(license license:bsd-3))))
(define-public python-icdiff
(package
(name "python-icdiff")
(version "2.0.5")
(source (origin
;; (method url-fetch)
;; (uri (pypi-uri "icdiff" version))
;; (sha256
;; (base32
;; "1bhbcc8mqvhdswfarl12x57yyzpw7dnkhsfv5fhy1ds8irr4plim"))
(method git-fetch)
(uri (git-reference
(url "https://github.com/jeffkaufman/icdiff";)
(commit (string-append "release-" version))))
(sha256
(base32
"14gr9j2h7sfw47pwfzspm4zinywhqmzm4a0qz5c2k9wbixz120a4"))
))
(build-system python-build-system)
(home-page "http://www.jefftk.com/icdiff";)
(synopsis "improved colored diff")
(description "improved colored diff")
(license #f)))
(define-public python-pytest-icdiff
(package
(name "python-pytest-icdiff")
(version "0.6")
(source (origin
;; Tests fail in git version, but not in pypi version.
(method url-fetch)
(uri (pypi-uri "pytest-icdiff" version))
(sha256
(base32
"1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8"))))
(build-system python-build-system)
(propagated-inputs (list python python-pypa-build python-icdiff
python-pprintpp python-pytest))
(home-page "https://github.com/hjwp/pytest-icdiff";)
(synopsis "use icdiff for better error messages in pytest assertions")
(description "use icdiff for better error messages in pytest assertions")
(license #f)))
(define-public python-hatch-fancy-pypi-readme
(package
(name "python-hatch-fancy-pypi-readme")
;;(version "22.3.0")
(version "22.8.0")
(source (origin
(method url-fetch)
(uri (pypi-uri "hatch_fancy_pypi_readme" version))
(sha256
(base32
;;"1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx"
"0sn2wsfbpsbf2mqhjvw62h1cfy5mz3d7iqyqvs5c20cnl0n2i4fs"))))
(build-system python-build-system)
(propagated-inputs (list python-hatchling-bootstrap python-tomli
python-typing-extensions))
(native-inputs (list python
python-pypa-build
python-pathspec-0.10.1
python-pluggy-1.0
python-editables
python-hatchling-bootstrap
python-wheel
python-pytest
python-pytest-icdiff))
(arguments
`(#:phases (modify-phases %standard-phases
(add-before 'build 'disable-broken-tests
(lambda _
;; Skip the tests for "building". Guix already does 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 _
(invoke "pytest" "-vv"))))))
(home-page "")
(synopsis "Fancy PyPI READMEs with Hatch")
(description "Fancy PyPI READMEs with Hatch")
(license #f)))
;; (define-public python-jsonschema-4.6
;; (package
;; (inherit python-jsonschema)
;; (name "python-jsonschema-4.6")
;; (version "4.15.0")
;; (source (origin
;; (method url-fetch)
;; (uri (pypi-uri "jsonschema" version))
;; (sha256
;; (base32
;; "07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11"))))
;; (native-inputs (list python-pypa-build
;; python-twisted
;; python-hatchling-bootstrap
;; python-pathspec
;; python-pluggy-1.0
;; python-editables
;; python-hatch-vcs
;; python-setuptools-scm-7
;; python-hatch-fancy-pypi-readme))
;; (propagated-inputs (list python-attrs
;; python-importlib-metadata
;; python-pyrsistent
;; python-typing-extensions
;; python-hatch-vcs
;; python-setuptools-scm-7))
;; (arguments
;; (substitute-keyword-arguments (package-arguments python-jsonschema-next)
;; ))))
(define-public python-pprintpp
;; Git version tags are inaccurate for this package; use the
;; bare commit.
(let ((commit "7ede6da1f3062bbfb32ee04353d675a5bff185e0")
(revision "1"))
(package
(name "python-pprintpp")
(version (git-version "0.3.0" revision commit))
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/wolever/pprintpp";)
(commit commit)))
(file-name (git-file-name name version))
(sha256
(base32
"0nk935m3ig8sc32laqbh698vwpk037yw27gd3nvwwzdv42jal2li"))))
(inputs (list python-pypa-build python-hypothesis python-wheel
python-parameterized))
(native-inputs (list python-pytest python-nose))
(build-system python-build-system)
(arguments
(list #:phases #~(modify-phases %standard-phases
(replace 'build
(lambda _
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "python"
"-m"
"build"
"--wheel"
"--no-isolation"
".")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
#$output
whl))))
(replace 'check
(lambda* (#:key tests? #:allow-other-keys)
(when tests?
(invoke "python" "test.py")))))))
(home-page "https://github.com/wolever/pprintpp";)
(synopsis "Python pretty-printer")
(description
"This package is a printer for Python which pretty-prints structures.
It also attempts to print Unicode characters without escaping them.")
(license license:bsd-3))))
(define-public python-pluggy-1.0
(package
(inherit python-pluggy)
(name "python-pluggy")
(version "1.0.0")
(source (origin
(method url-fetch)
(uri (pypi-uri "pluggy" version))
(sha256
(base32
"0n8iadlas2z1b4h0fc73b043c7iwfvx9rgvqm1azjmffmhxkf922"))))
(inputs (list python-pypa-build python-wheel))
(native-inputs (list python-pytest python-setuptools-scm))))
(define-public python-setuptools-scm-7
(package
(inherit python-setuptools-scm)
(version "7.0.5")
(source (origin
(method url-fetch)
(uri (pypi-uri "setuptools_scm" version))
(sha256
(base32
"0i28zghzdzzkm9w8rrjwphggkfs58nh6xnqsjhmqjvqxfypi67h3"))))
(build-system python-build-system)
(arguments
`( ;Disabled tests to avoid extra dependencies.
#:tests? #f
#:phases (modify-phases %standard-phases
;; Disabled sanity check to avoid extra dependencies.
(delete 'sanity-check))))
(propagated-inputs (list python-packaging-bootstrap python-tomli))))
(define-public python-pathspec-0.10.1
(package
(name "python-pathspec")
(version "0.10.1")
(source ;; (origin
;; (method url-fetch)
;; (uri (pypi-uri "pathspec" version))
;; (sha256
;; (base32
;; "0g9jhhhf3zmrnvzvjjd2yhizsb6i93hmlszb09wixlr1nrhn3kks")))
(origin
(method git-fetch)
(uri (git-reference
(url
"https://github.com/cpburnz/python-pathspec";)
(commit (string-append "v" version))))
(sha256
(base32 "0sgzh7ad1x098d0rln01f0qabpa7mnp26863isncbiyqsxh1gaxp"))))
(build-system python-build-system)
(home-page "https://github.com/cpburnz/python-pathspec";)
(synopsis
"Utility library for gitignore style pattern matching of file paths.")
(description
"Utility library for gitignore style pattern matching of file paths.")
(license license:mpl2.0)))
;; This depends on packages in python-xyz.scm:
;; python-version, python-importlib-metadata, python-pathspec,
;; python-pluggy-1.0, and python-platformdirs.
(define-public python-hatchling-bootstrap
(package
(name "python-hatchling-bootstrap")
(version "1.10.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/pypa/hatch";)
(commit (string-append "hatchling-v" version))))
(file-name (git-file-name name version))
(sha256
(base32
;;"1q25kqw71g8mjwfjz9ph0iigdqa26zzxgmqm0v0bp0z1j8rcl237"
;;"1yqkwck2aihfdm9ljv5q4nygmmqyp35xwyp8lqn2f4vq9p6njq3c"
"0ahx62w711a2vnb91ahqxrw8yi0gq0kfch3fk6akzngd13376czj" ;;
github weirdness.
))))
;; python-pypa-build needed for bootstrapping.
;; Otherwise we get a circular reference:
;; python-hatchling trying to build itself, without
;; first having hatchling installed.
(inputs (list python-pypa-build
python-editables
python-importlib-metadata
python-version
python-packaging-next
python-pathspec-0.10.1
python-pluggy-1.0 ;TODO: Not detected by pytest?
python-tomli
python-platformdirs))
(build-system python-build-system)
(arguments
`( ;Tests depend on module python-hatch, which this
;; is bootstrapping.
#:tests? #f
#:phases (modify-phases %standard-phases
(replace 'build
(lambda _
(chdir "backend")
;; ZIP does not support timestamps before 1980.
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "python"
"-m"
"build"
"--wheel"
"--no-isolation"
".")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
(assoc-ref %outputs "out")
whl)))))))
(home-page "https://ofek.dev/projects/hatch/";)
(synopsis "Bootstrap binaries to build @code{python-hatch}")
(description "Bootstrap binaries to build @code{python-hatch}")
;; MIT License
(license license:expat)))
(define-public python-hatch
(package
(name "python-hatch")
(version "1.5.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/pypa/hatch";)
(commit (string-append "hatch-v" version))))
(file-name (git-file-name name version))
(sha256
(base32
"030yi9hw50mn899pq073lw2a55r57skl2g9agjp3b4l95f3nay30"))))
(inputs (list python-pypa-build
python-editables
python-importlib-metadata
python-version
python-packaging-next
python-pathspec
python-pluggy-1.0 ;TODO: Not detected by pytest?
python-hatchling-bootstrap
python-tomli
python-platformdirs
python-rich
python-tomli-w))
(build-system python-build-system)
(arguments
`( ;Tests appear to be written such that the input python-pluggy-1.0 is
;; not detected.
#:tests? #f
#:phases (modify-phases %standard-phases
(replace 'build
(lambda _
;; ZIP does not support timestamps before 1980.
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "hatchling" "build")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
(assoc-ref %outputs "out")
whl))))
(replace 'check
(lambda* (#:key tests? #:allow-other-keys)
(when tests?
(chdir "tests")
(invoke "pytest" "-vv"))))
;; Can't have hatch as a requirement of itself.
(delete 'sanity-check))))
(home-page "https://ofek.dev/projects/hatch/";)
(synopsis "Python build system with project generation")
(description
"Python build system with project generation. It also defines a specific
syntax in @code{toml} files to check for dependencies.")
;; MIT License
(license license:expat)))
(define-public python-hatch-vcs
;; Tags are not accurate; just use the commit itself.
(let ((commit "367daedb23ba906f3e0714c64392fdd6ffa69ab2")
(revision "1"))
(package
(name "python-hatch-vcs")
(version (git-version "0.2.0" revision commit))
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/ofek/hatch-vcs";)
(commit commit)))
(file-name (git-file-name name version))
(sha256
(base32
"0nlnv32jqiz8ikc013h5simmiqqg0qa7pm0qcbd8yiqq1p43iw05"))))
(build-system python-build-system)
(inputs (list python-pypa-build
python-pathspec-0.10.1
python-pluggy-1.0
python-editables
git
python-hatchling-bootstrap
python-typing-extensions))
(native-inputs (list python-pytest
;; python-setuptools-scm-6.4 minimum
python-setuptools-scm-7))
(arguments
(list #:phases #~(modify-phases %standard-phases
(replace 'build
(lambda _
(setenv "SOURCE_DATE_EPOCH" "315532800")
(invoke "python"
"-m"
"build"
"--wheel"
"--no-isolation"
".")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(let ((whl (car (find-files "dist" "\\.whl$"))))
(invoke "pip"
"--no-cache-dir"
"--no-input"
"install"
"--no-deps"
"--prefix"
#$output
whl))))
(replace 'check
(lambda* (#:key tests? #:allow-other-keys)
(when tests?
(invoke "pytest" "-vvv"))))))) ;)
(home-page "https://ofek.dev/projects/hatch/";)
(synopsis "Plugin for @code{python-hatch} to include versions")
(description
"This plugin defines a version-control syntax for use with
@code{toml} files intended for use with @code{python-hatch}.")
;; MIT License
(license license:expat))))
(define-public python-pytest-icdiff
(package
(name "python-pytest-icdiff")
(version "0.6")
(source (origin
(method url-fetch)
(uri (pypi-uri "pytest-icdiff" version))
(sha256
(base32
"1b8vzn2hvv6x25w1s446q1rfsbdik617lzpal3qb94x8a12yzwg8"))))
(build-system python-build-system)
(propagated-inputs (list python-pypa-build python-icdiff python-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-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.")
;; ;; MIT License
;; (license license:expat)))
;; Has to be done manually. DO NOT copy and paste this one.
(define-public python-jsonschema-4.15
(package
(inherit python-jsonschema-next)
(version "4.16.0")
(source (origin
(method url-fetch)
(uri (pypi-uri "jsonschema" version))
(sha256
(base32
;; old pypi hash
;; ;;"07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11"
;; new pypi hash
"08sbw5fn19vn8x7c216gkczyzd575702yx2vmqdrgxpgfvq5jl0n"))))
(native-inputs (list python-pypa-build
python-twisted
python-hatch
python-hatchling-bootstrap
python-pathspec-0.10.1
python-pluggy-1.0
python-editables
python-hatch-vcs
python-setuptools-scm-7
python-hatch-fancy-pypi-readme))
(propagated-inputs (list python-attrs
python-importlib-metadata
python-pyrsistent
python-typing-extensions
python-hatch-vcs))
(home-page "https://github.com/python-jsonschema/jsonschema";)))
coq-mathcomp-analysis
--8<---------------cut here---------------end--------------->8---
channels.scm
--8<---------------cut here---------------start------------->8---
;;; This module extends GNU 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>
(list
;; guix
(channel
(name 'guix)
;;(url "https://git.savannah.gnu.org/git/guix.git";)
(url "https://github.com/guix-mirror/guix";)
(introduction
(make-channel-introduction
"9edb3f66fd807b096b48283debdcddccfea34bad"
(openpgp-fingerprint
"BBB0 2DDF 2CEA F6A8 0D1D E643 A2A0 6DF2 A33A 54FA")))
(commit "9f391b90faca02ca97c5018d6c095ecdaa1a94a7")) ;; The commit
;; just before the upgrade to Coq 8.16!
;; The channel that contains coq-mathcomp-analysis package
;; definitions.
(channel
(name 'coq-mathcomp-analysis-packages)
;;(url
;;"/home/chips/home/code/coq-my-theories/mathcomp-extra-packages"
(url
"./mathcomp-extra-packages")))
--8<---------------cut here---------------end--------------->8---
guix-manifest.scm
--8<---------------cut here---------------start------------->8---
;;; This module extends GNU 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>
(use-modules
(guix packages)
(gnu packages coq)
(coq-mathcomp-analysis))
(packages->manifest (list coq coq-stdlib coq-mathcomp coq-mathcomp-finmap
coq-mathcomp-hierarchy-builder coq-elpi coq-mathcomp-bigenough coq-core
coq-mathcomp-analysis))
--8<---------------cut here---------------end--------------->8---
- [bug#58310] [PATCH 08/14] gnu: Add python-hatch-fancy-pypi-readme., (continued)
- [bug#58310] [PATCH 08/14] gnu: Add python-hatch-fancy-pypi-readme., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 07/14] gnu: Add python-pytest-icdiff., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 05/14] gnu: Add python-hatch., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 06/14] gnu: Add python-hatch-vcs., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 10/14] gnu: Add ocaml-atd., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 09/14] gnu: python-jsonschema-next: Update to 4.16.0., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 14/14] gnu: Add coq-mathcomp-analysis., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 11/14] gnu: Add ocaml-elpi., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 12/14] gnu: Add coq-elpi., Garek Dyszel, 2022/10/05
- [bug#58310] [PATCH 13/14] gnu: Add coq-mathcomp-hierarchy-builder., Garek Dyszel, 2022/10/05
- [bug#58310] Temporary manifest for coq-mathcomp-analysis,
Garek Dyszel <=