Stream: Hierarchy Builder devs & users

Topic: Accessing predicates defined in tc


view this post on Zulip Quentin VERMANDE (Nov 07 2023 at 15:48):

Hi. I am experimenting with the code of HB and I would like to declare a mixin as a class (hence editing factory.elpi). Furthermore, I would like to use the typeclass resolution solver defined in coq-elpi. It seems that I need to use the predicate add-class-gr defined in coq-elpi/apps/tc/elpi/create\_tc\_predicate.elpi. Is there a way to access it?

view this post on Zulip Enrico Tassi (Nov 07 2023 at 15:48):

This is a question for @Davide F

view this post on Zulip Quentin VERMANDE (Nov 07 2023 at 15:52):

We have already discussed it. The only solution he found is to declare the required file as an explicit dependency, which only works because both projects are on my machine. This is unsatisfying since that means I will never be able to push anything.

view this post on Zulip Enrico Tassi (Nov 07 2023 at 15:53):

I'm a bit lost. HB depends on Coq-Elpi.

view this post on Zulip Enrico Tassi (Nov 07 2023 at 15:55):

I guess you should be able to accumulate the db and add to it the same predicates.
But I guess this is much easier to discuss looking at the same screen.

view this post on Zulip Quentin VERMANDE (Nov 07 2023 at 15:56):

Indeed, but the solution entails adding the directory coq-elpi/apps/tc/elpi to the \_CoqProject file of HB and add a From xxx Extra Dependency ..." in structures.v`.

view this post on Zulip Quentin VERMANDE (Nov 07 2023 at 15:58):

I am not sure what you mean by "accumulate the db", the operation done by add-class-gr looks non-trivial before the accumulate is done.

view this post on Zulip Enrico Tassi (Nov 07 2023 at 16:10):

At least for Db, you should be able to do:

From elpi.apps Require tc.

Elpi Command foo.
Elpi Accumulate Db tc.db.

There is no notion of "library", but that can be surely added.
Of course today you can put any code in a Db, but that is a bit of a hack.

view this post on Zulip Enrico Tassi (Nov 07 2023 at 16:12):

Finally, coq-elpi should install its .elpi files, so you should be able to just use them.
Maybe we forgot for the apps, but the other elpi files should be in ..../lib/coq/user-contrib/elpi/ and be accessible via From elpi.apps.tc Extra Dep "bla".

view this post on Zulip Enrico Tassi (Nov 07 2023 at 16:14):

Look at
https://github.com/LPCIC/coq-elpi/blob/36b62814516accfcf16701ed86cf4b57406c617e/Makefile.coq.local#L16-L21
maybe this is missing in apps/tc/Makefile.coq.local

view this post on Zulip Paolo Giarrusso (Nov 07 2023 at 17:24):

I think I can confirm that From xxx Extra Dependency ... works when the extra dependency is installed.

view this post on Zulip Paolo Giarrusso (Nov 07 2023 at 17:25):

https://github.com/bedrocksystems/BRiCk/blob/4a0187bf63bcc046ad6d8b991d6ebac80da708b0/coq-lens/Lens/Elpi/Elpi.v has

From elpi.apps.derive Extra Dependency "lens.elpi" as lens.
From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.

and the two .elpi files in question only live in the coq-elpi package.
The only _unusual_ thing is that coqdep on those lines will warn it can't find the files — but unlike all other coqdep warnings I've ever seen, coqc works fine.

view this post on Zulip Quentin VERMANDE (Nov 08 2023 at 08:58):

I managed to intall the files, now it works. Thanks for the help.


Last updated: Apr 21 2024 at 02:41 UTC