Stream: Elpi users & devs

Topic: elpi and coqdep


view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 19:56):

coqdep doesn't output dependencies on elpi files upon Accumulate File "file.elpi". — I noticed because of dune, but coq_makefile can't be too happy. How do you get safe incremental builds with elpi?

view this post on Zulip Enrico Tassi (Feb 01 2022 at 21:07):

See for example: https://github.com/math-comp/algebra-tactics/blob/master/Makefile.coq.local or https://github.com/LPCIC/coq-elpi/blob/master/apps/derive/Makefile.coq.local
make has a syntax to add deps to a target, and coq_makefile can load a custom snippet...

view this post on Zulip Enrico Tassi (Feb 01 2022 at 21:08):

For dune, I've no clue. @Emilio Jesús Gallego Arias is considering a script to generate rules, so maybe that one would be simpler to hack.. dunno.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 10:30):

With dune you can add the dep by hand too, using (rule

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 10:30):

that's painful tho, would be better if coqdep could learn about it

view this post on Zulip Enrico Tassi (Feb 02 2022 at 15:49):

Can you give an example? As far as I know I can't add a new rule for foo.vo since dune already has one.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):

I was thinking of

(rule
  (target foo.v)
  (deps foo.v.in foo.elpi)
  (action (copy_file ...)))

but that's a pain; something very easy to do is to have a field (extra_deps ...) in (coq.theory ...) as a workaround.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):

of have coqdep understand extensions, IMHO that's something needed for plugins , smt integration, elpi, etc....

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):

to be able to register this kind of stuff

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):

I had a look at Isabelle's api

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):

long time ago, but that's a bit offtopic

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2022 at 16:04):

I've added the (extra_files ...) field to my dune todo

view this post on Zulip Paolo Giarrusso (Feb 02 2022 at 23:19):

wait, so you're suggesting to build foo.v.in into foo.v and have that depend on foo.elpi? I'd feel like a naked emperor, since dune can tell foo.v is unchanged and my dependency is a lie?

view this post on Zulip Enrico Tassi (Feb 03 2022 at 07:05):

dune is just too smart

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 10:07):

Enrico Tassi said:

dune is just too smart

That's a problem with declarative languages in general (for example see what real-world programming involves in Prolog) .

But IMHO that's not a bug in dune, but in coqdep.

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 11:19):

But is there a fix, short of redesigning coqdep? Having all elpi code inside .v files might be an alternative, but I'm not sure how well coq-elpi supports that... Can you accumulate the same code into multiple databases without moving it to an elpi file or duplicating it?

view this post on Zulip Enrico Tassi (Feb 03 2022 at 11:56):

Hum, not really. Anyway, I would not use dune for coq projects "in production", it looks to rigid and experimental to me.

About declarative languages I totally disagree, it is just about being pragmatic. For example, even the dependencies within ocaml modules are broken https://github.com/ocaml/dune/issues/753 , but in spite of this issue being paramount to my eyes dune devs have other priorities and some trivial workarounds like letting one write by hand deps is not implemented yet (see https://github.com/ocaml/dune/issues/1753). Incidentally that would let one fix this problem about elpi files as well.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:01):

many Coq projects are conceptually simple and work fine using the "default Coq support" in Dune. The main problem there is interproject-dependencies in a monorepo ((theories X) declarations)

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:03):

Dune can be a hassle for cross-Coq-OCaml projects, but still is usually better than coq_makefile for plugins, and the extraction support is amazing when one can fit into the quite narrow assumptions.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:04):

so my stance is basically that if one can support both Dune and coq_makefile, it's a good idea, and one then one can pick-and-mix for the rest... best of all is running both in CI (we use Nix and opam CI combo for this)

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 12:20):

we use coq_makefile but it isn't incremental enough for CI. Or for local use. Nor does it let you build related projects together without lots of duct tape.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 12:22):

it seems to be true both in set theory and build systems, "to get more you need to assume more"

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 12:39):

either way, everything else in coq-elpi appears great, _except_ Accumulate File resolution :-|.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:05):

Most problems with Dune are just a matter of lack of manpower, help is welcome!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:05):

Dune devs follow their own priorities with are large-scale building

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:05):

I'm not in love with coq_makefile either, but at least you can put the duct tape...
Anyway, I really don't know what to suggest if you want to use dune and get the deps right.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:05):

So yeah in terms of expressivity, it works for them, in terms of performance / caching etc... no so much

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:06):

For now regarding dune and elpi there is no good workaroung, short term I'll add extra_files to coq.theory

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:06):

long term coqdep should produce sound dependencies

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:06):

as any manual maintenance like that doesn't scale

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):

my point is that even if dune would allow you to add the elpi file by hand

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):

that's still a disaster

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):

duct tape indeed

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):

as it puts a considerable burden on the user who has to maintain now deps manually

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:11):

Emilio Jesús Gallego Arias said:

Dune devs follow their own priorities with are large-scale building

as I think we all know, the problem is not manpower in general, but rather lack of people who are sufficiently in tune with Dune devs to get PRs with changes merged.

view this post on Zulip Karl Palmskog (Feb 03 2022 at 13:12):

duct tape at least gets your project to build, but if you have to get a Dune PR merged instead, this is a huge threshold

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:13):

Let's move this discussion to the Dune channel, but what are examples of PR waiting to merge?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:13):

PR merging in Dune is pretty quick usually

view this post on Zulip Notification Bot (Feb 03 2022 at 13:29):

This topic was moved by Emilio Jesús Gallego Arias to #Dune devs & users > Making PRs to Dune

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:30):

@Enrico Tassi back on this topic, how could coqdep produce the right dependencies? I don't know a good way without (a) hardcoding support for elpi, or (b) replacing Accumulate File with some standard primitive that coqdep understands. Or (c) adding some plugin architecture to coqdep (doesn't seem quick).

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:37):

I really don't see an easy way.
A non super easy way could be to move the resolver code based on the loadpath I'm writing to Coq, then do something like

External File "foo.elpi" From logpath As x.
(* a coq command, using the new resolver and adding "x -> path to foo.elpi" to some DB *)

Elpi Accumulate File x.
(* Elpi command undersatand name from that DB *)

Today coqdep parses the file in an approximate way, one could add support for "External File" once and forall.

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:37):

This approach would be "elpi independent" and work for any external file.

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:38):

Yep, that's what option (b) tried to hint at.

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:39):

@Emilio Jesús Gallego Arias would be dune fine with coqdep spitting a.vo : a.v abspath_to_foo.elpi ?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:40):

Sure, I think that's a very good start

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:41):

FYI the "resolver" would look for a file "foo.elpi" in a directory bound to logpath "logpath". Inside elpi I encode this as coq://log.path/file.elpi and then resolve this to an absolute path. But I'm afraid abspaths are not OK in dune

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:41):

We should ask Chantal and other people using files

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:41):

if that would work for them too

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:41):

We could process the abspath and do inverse resolution, but why it has to be absolute?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:42):

It could be resolved in the same way .vo files are

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:42):

yes, the more code is shared with Require the better

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:42):

@Enrico Tassi absolute paths in coq_makefile can be dangerous, because GNU Make doesn't actually understand paths (!) https://www.cmcrossroads.com/article/gnu-make-path-handling

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:42):

@Emilio Jesús Gallego Arias Well, this is what Loadpath.physical gives me

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:43):

Thanks for the heads up, but for now I'm only using the path to read the file, so absolute is good.

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:44):

did you add absolute paths to Coq's LoadPath? I think today coqdep respects relative/absolute in -Q/...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:44):

I can't look at the code now sorry, but if coqdep is able to resolve .vo files relatively, I guess it should be the same for "data" files?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:44):

Yeah just do the same that is done for .vo files

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:44):

It does, so we can do the same.

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:45):

In my code I ask Coq to resolve a logpath to a directory, and I get an abspath... but coqdep must be using another API I guess

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:46):

this might not be a deal breaker for make, since Elpi files aren't themselves generated, but _might_.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:47):

Enrico Tassi said:

In my code I ask Coq to resolve a logpath to a directory, and I get an abspath... but coqdep must be using another API I guess

What options are you passing to -Q / -R ?

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:47):

Right, but I think I could get a relative path when the logpath is from a -R or something.
OK, we have a plan...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:47):

If you pass an abs path

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:48):

coqdep will use an abspath

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:48):

I pass a relative path

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:48):

but maybe I abspath myself, don't worry about this thing

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:48):

Yeah shouldn't be a big deal to find the right function, it is already done for .vo files

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:48):

(so FWIW I'm just spreading info about cursed corner cases, I can't predict if it's a problem... anyway good luck)

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:49):

the "resolver" is something I give to the parser of elpi, that wants abspaths, since the resolver may change dir...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):

As of today, dune doesn't filter the dependencies that coqdep generates

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):

so if you update coqdep like that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):

it should work out of the box (TM / famous last words)

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:49):

IIRC it bails out if one of the deps is not in the source tree

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):

yes it needs to know how to build the dep of course

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):

it could be generated

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):

or be part of the sources as there is an implicit rule

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):

for the sources

view this post on Zulip Paolo Giarrusso (Feb 03 2022 at 13:50):

that's the one that copies sources into _build, right? I think I saw that in action...

view this post on Zulip Enrico Tassi (Feb 03 2022 at 13:51):

I'll open an isse in Coq with this wish, then go back to elpi... almost got a stack overflow in my tasks
;-)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 13:51):

Paolo Giarrusso said:

that's the one that copies sources into _build, right? I think I saw that in action...

Yes, but only if the sources are the dependency of some other target


Last updated: Feb 05 2023 at 13:02 UTC