Paolo Giarrusso (Feb 01 2022 at 19:56): 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?
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...
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.
Emilio Jesús Gallego Arias (Feb 02 2022 at 10:30):With dune you can add the dep by hand too, using (rule
Emilio Jesús Gallego Arias (Feb 02 2022 at 10:30):that's painful tho, would be better if coqdep could learn about it
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.
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.
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....
Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):to be able to register this kind of stuff
Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):I had a look at Isabelle's api
Emilio Jesús Gallego Arias (Feb 02 2022 at 15:56):long time ago, but that's a bit offtopic
Emilio Jesús Gallego Arias (Feb 02 2022 at 16:04):I've added the (extra_files ...) field to my dune todo
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?
Enrico Tassi (Feb 03 2022 at 07:05):dune is just too smart
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.
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?
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.
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)
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.
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)
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.
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"
Paolo Giarrusso (Feb 03 2022 at 12:39):either way, everything else in coq-elpi appears great, _except_ Accumulate File resolution :-|.
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!
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:05):Dune devs follow their own priorities with are large-scale building
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.
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
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:06):long term coqdep should produce sound dependencies
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:06):as any manual maintenance like that doesn't scale
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):that's still a disaster
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:07):duct tape indeed
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
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.
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
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?
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:13):PR merging in Dune is pretty quick usually
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
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).
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.
Enrico Tassi (Feb 03 2022 at 13:37):This approach would be "elpi independent" and work for any external file.
Paolo Giarrusso (Feb 03 2022 at 13:38):Yep, that's what option (b) tried to hint at.
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 ?
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:40):Sure, I think that's a very good start
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
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:41):We should ask Chantal and other people using files
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:41):if that would work for them too
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?
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:42):It could be resolved in the same way .vo files are
Paolo Giarrusso (Feb 03 2022 at 13:42):yes, the more code is shared with Require the better
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
Enrico Tassi (Feb 03 2022 at 13:42):@Emilio Jesús Gallego Arias Well, this is what Loadpath.physical gives me
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.
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/...
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?
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:44):Yeah just do the same that is done for .vo files
Enrico Tassi (Feb 03 2022 at 13:44):It does, so we can do the same.
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
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_.
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 ?
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...
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:47):If you pass an abs path
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:48):coqdep will use an abspath
Enrico Tassi (Feb 03 2022 at 13:48):I pass a relative path
Enrico Tassi (Feb 03 2022 at 13:48):but maybe I abspath myself, don't worry about this thing
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
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)
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...
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):As of today, dune doesn't filter the dependencies that coqdep generates
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):so if you update coqdep like that
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:49):it should work out of the box (TM / famous last words)
Enrico Tassi (Feb 03 2022 at 13:49):IIRC it bails out if one of the deps is not in the source tree
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):yes it needs to know how to build the dep of course
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):it could be generated
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):or be part of the sources as there is an implicit rule
Emilio Jesús Gallego Arias (Feb 03 2022 at 13:50):for the sources
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...
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
;-)
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: Jun 06 2023 at 23:01 UTC