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
