diff mbox series

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

Message ID 87sfl3vxws.fsf@disroot.org
State Accepted
Headers show
Series [bug#57540,RFC,v2,01/19] gnu: Add ocaml-elpi. | expand

Commit Message

Garek Dyszel Sept. 7, 2022, 6:31 p.m. UTC
Hi Julien,

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

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

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

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

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

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

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

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

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

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

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

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

What do you think?

Thanks again for the help!
Garek

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

Comments

Simon Tournier Sept. 26, 2022, 4:52 p.m. UTC | #1
Hi Garek,

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

For instance the series reads,

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

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

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

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


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

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

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


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

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

 2. the correct dependency order of the patches


Cheers,
simon
Garek Dyszel Sept. 27, 2022, 1:04 p.m. UTC | #2
Hi Julien and simon,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- Garek
Garek Dyszel Sept. 29, 2022, 5:13 p.m. UTC | #3
Hi again,

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

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

Let me know.

Thanks!
Garek

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

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

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

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

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

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

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

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

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


Cheers,
simon
Garek Dyszel Sept. 30, 2022, 3:02 p.m. UTC | #6
Sounds like a plan. Thanks again!

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

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

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

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

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

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

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

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


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


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


Cheers,
simon
diff mbox series

Patch

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 2fd519ca41..c4fa05b934 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@ 
 ;;; Copyright © 2021 Sarah Morgensen <iskarian@mgsn.dev>
 ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com>
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -8774,3 +8775,98 @@  (define-public ocaml-guile
      "The OCaml guile library provides high-level OCaml bindings to GNU Guile
 3.0, supporting easy interop between OCaml and GNU Guile Scheme.")
     (license license:gpl3+)))
+
+(define-public ocaml-elpi
+  (package
+    (name "ocaml-elpi")
+    ;; For more information on which version works with Coq 8.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    ;;
+    ;; The package ocaml-elpi@1.16.5 appears to require a different
+    ;; build process.
+    (version "1.15.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:test-target "tests"))
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atd
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson))
+    (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
+    (home-page "https://github.com/LPCIC/elpi")
+    (synopsis "ELPI - Embeddable λProlog Interpreter")
+    (description
+     "ELPI implements a variant of λProlog enriched with Constraint
+Handling Rules, a programming language well suited to manipulate
+syntax trees with binders.
+
+ELPI is designed to be embedded into larger applications written in
+OCaml as an extension language.  It comes with an API to drive the
+interpreter and with an FFI for defining built-in predicates and data
+types, as well as quotations and similar goodies that are handy to
+adapt the language to the host application.
+
+This package provides both a command line interpreter (elpi) and a
+library to be linked in other applications (eg by passing -package
+elpi to ocamlfind).
+
+The ELPI programming language has the following features:
+
+@itemize
+@item Native support for variable binding and substitution, via an Higher
+Order Abstract Syntax (HOAS) embedding of the object language.  The
+programmer does not need to care about technical devices to handle
+bound variables, like De Bruijn indices.
+
+@item Native support for hypothetical context.  When moving under a binder
+one can attach to the bound variable extra information that is
+collected when the variable gets out of scope.  For example when
+writing a type-checker the programmer needs not to care about managing
+the typing context.
+
+@item Native support for higher order unification variables, again via
+HOAS.  Unification variables of the meta-language (λProlog) can be
+reused to represent the unification variables of the object language.
+The programmer does not need to care about the unification-variable
+assignment map and cannot assign to a unification variable a term
+containing variables out of scope, or build a circular assignment.
+
+@item Native support for syntactic constraints and their meta-level
+handling rules.  The generative semantics of Prolog can be disabled by
+turning a goal into a syntactic constraint (suspended goal).  A
+syntactic constraint is resumed as soon as relevant variables gets
+assigned.  Syntactic constraints can be manipulated by constraint
+handling rules (CHR).
+
+@item Native support for backtracking.  To ease implementation of search.
+
+@item The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+@item Clauses are graftable.  The user is free to extend an existing
+program by inserting/removing clauses, both at runtime (using
+implication) and at \"compilation\" time by accumulating files.
+@end itemize
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))