;; -*- mode: scheme; mode: guix-devel -*-
;;; Local Variables:
;;; sentence-end-double-space: t
;;; End:
;;; 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

;; To build directly from this file, use the following command.
;; guix build --with-patch=ocaml-elpi=patches/ocaml-elpi-fix-yojson.patch -Kf coq-mathcomp-analysis.scm

(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-system pyproject)
  ;; #: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)
  #: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 lua)
  #:use-module (gnu packages version-control))

;;; Python
(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 pyproject-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 pyproject-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 pyproject-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
  (package
    (name "python-hatchling")
    (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 would result in circular references
       #: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-hatchling
;;     (package
;;     (name "python-hatchling")
;;     (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"))))
;;     (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
;;                   python-hatchling-bootstrap))
;;     (build-system pyproject-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.6.2") ;; at minimum 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
                "0if5ssp6vlfvna1jcvap40r0f7pm45h7kbia78h5ivm17vb8p08b"
                ;;"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
                  python-tomli
                  python-platformdirs
                  python-rich
                  python-tomli-w))
    (build-system pyproject-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 pyproject-build-system)
      (inputs (list python-pypa-build
                    python-pathspec-0.10.1
                    python-pluggy-1.0
                    python-editables
                    git
                    python-hatchling
                    ;; python-hatch
                    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"))))))) ;)
      (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 "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 pyproject-build-system)
    (propagated-inputs (list python-pypa-build python-icdiff python-pprintpp
                             python-pluggy-1.0))
    (native-inputs (list python-pytest))
    (arguments
     `(;; Tests fail with "collecting ... collected 0 items"
       #:tests? #f))
    ;; (arguments
    ;;  `(#:phases
    ;;    (modify-phases %standard-phases
    ;;      (add-before 'check 'chdir-to-test-dir
    ;;        (chdir "tests")))))
    (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
                ;; PyPI hash problem
                ;;"1ykfz1sbz58xbjw5k9xpmn5r6ji16w8vag47j8f969bqy3w52ikx"
                "0sn2wsfbpsbf2mqhjvw62h1cfy5mz3d7iqyqvs5c20cnl0n2i4fs"))))
    (build-system pyproject-build-system)
    (propagated-inputs (list python-tomli python-typing-extensions))
    (native-inputs (list python-pypa-build
                         python-pathspec-0.10.1
                         python-pluggy-1.0
                         python-editables
                         python-hatchling
                         python-wheel
                         python-pytest
                         python-pytest-icdiff))
    (arguments
     `(#:phases (modify-phases %standard-phases
                  (add-before 'build 'disable-broken-tests
                    (lambda _
                      ;; Skip the tests for "building". Guix already does this,
                      ;; so we don't need to test it for 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
                ;; PyPI hashing problem
                "08sbw5fn19vn8x7c216gkczyzd575702yx2vmqdrgxpgfvq5jl0n"
                ;;"07pyh8g4csapkfjgjww7vkxwvh1qwxwqxz82wm2b1kmxj69rgx11"
                ))))
    (native-inputs (list python-pypa-build
                         python-twisted
                         python-hatch
                         python-hatchling
                         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")))

;;; OCaml
;; Requires python-jsonschema with version at minimum 4.6.0 to run
;; tests. 
;; See https://github.com/ahrefs/atd/issues/306 for more info on that.
(define-public ocaml-atd
  (package
    (name "ocaml-atd")
    (version "2.10.0")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/ahrefs/atd")
                    (commit version)))
              (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.")
    ;; Modified BSD license
    (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")
    (version "1.16.7")
    (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
                ;; for 1.16.5
                ;;"1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl"
                ;; for the version that the patch is based on (1.16.7)
                "1i0731f7jj48zvkla959pffj5l0qynmfyxljgszc6z3b4lpni1xc"))
              ;; Fix incompatibility with ocaml-yojson@2.0.2.
              ;; See <https://github.com/LPCIC/elpi/pull/167>.
              (patches (search-patches "ocaml-elpi-fix-yojson.patch"))
              ;(patches '("/home/chips/home/code/guix_packages/built/patches/ocaml-elpi-fix-yojson.patch"))
              ))
    (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+)))

;;; Coq
(define-public coq-elpi
  (package
    (name "coq-elpi")
    (version "1.16.0")
    (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
                "18w899fcz4kzx7zyr7a0g4avclbm5f82g7kh76b9fy2s99jz6q5c"))))
    ;;(build-system gnu-build-system)
    (build-system ocaml-build-system)
    (propagated-inputs (list coq-core ocaml-elpi ocaml-zarith))
    (inputs (list python lua-5.1 coq-core coq-stdlib)) 
    (arguments
     `(#:test-target "test"
       ;; From the repo: "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAMLWARN="
       #: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 "COQLIBINSTALL="
                                            #$output
                                            "/lib/coq/user-contrib")
                             (string-append "COQMF_COQLIB="
                                            #$output
                                            "/lib/ocaml/site-lib/coq")
                             (string-append "COQPLUGININSTALL="
                                            #$output
                                            "/lib/ocaml/site-lib")
                             "OCAMLWARN=")
       #:phases (modify-phases %standard-phases
                  (delete 'configure)
                  #;(add-after 'check 'check-findlib-path
                    (lambda _
                      (invoke "ocamlfind" "query" "coq-elpi"))))))
    (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)))

(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")
    (version "1.4.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
                ;; 1.3.0
                ;;"17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"
                ;; 1.4.0
                "1g7narbx5n8bbnnnn8kmgk62clah9fsy9jb154xcr41p8psrvrxl"))))
    ;;(build-system ocaml-build-system) ;; fails for same reason as dune.
    (build-system gnu-build-system)
    (arguments
     `(#:make-flags ,#~(list (string-append "ELPIDIR="
                                            #$(this-package-input "coq-elpi")
                                            "/lib/coq/user-contrib/elpi/")
                             (string-append "DESTDIR="
                                            (assoc-ref %outputs "out"))
                             (string-append "COQLIBINSTALL="
                                            #$output
                                            "/lib/coq/user-contrib"))
       #:test-target "test-suite"
       #:phases (modify-phases %standard-phases
                  (delete 'configure)
                  )))
    (propagated-inputs (list coq-elpi))
    (inputs (list coq-core
                  coq-stdlib))
    (native-inputs (list ocaml which))
    (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/")
    ;; MIT license
    (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 "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))
    (native-inputs (list ocaml 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)))

coq-mathcomp-analysis