Does it make sense to add elpi to coq-universe? It is not a coq development but it can be used with coq.
I think so, especially since elpi and coq-elpi often evolve in lockstep
Said otherwise, if developing elpi can require rebuilding client coq libraries, it seems to make sense. But I'm an outsider, and @Enrico Tassi knows better
@Roland Coeurjoly for now we are not vendoring OCaml packages, as this is usually a bit more complex. But for example elpi or menhir (which Ali did vendor originally) could be added to it
Tho I feel that the primary goal of this project is to gather projects that contain .v files, that is to say, Coq projects
Do you mean elpi
or coq-elpi
? Because elpi
alone has to be seen as an ocaml dependency, like zarith or menhir.
coq-elpi
is a Coq project, why not add it. But it does not have a dune file for a technical reason: only from Coq 8.16 it will be possible to build (and load) a working coq-elpi with dune. @Emilio Jesús Gallego Arias wrote the dune file a few times, but it was never ok, for that technical reason primarily. So maybe we should wait a month (8.16 will come out soon), and then try again porting coq-elpi to dune.
They are talking about elpi
, not coq-elpi
my answer was about elpi
— for the goals of coq-universe, I guess the question is how often changes to elpi
itself might propagate to e.g. hierarchy-builder and hb-based-math-comp
elpi and coq-elpi go in tandem, but then coupling typically stops there
@Emilio Jesús Gallego Arias Do you have a link to the dune branch, we should add elpi as an opam dep, and then put your branch of coq-elpi in. I would love to get HB working (with dune).
Actually we should discuss how to do this
because my branch was a hack
What is the main barrier today? The elpi plugin relying on .elpi files?
coq-elpi relying on fl_dynload
so we need to update dune
that would be easy, if not for this bug
https://github.com/ocaml/dune/issues/5833
Are we talking about the plugin loading or is elpi doing something else with fl_dynload?
OK so same problem every plugin is having.
I will propose the work around of (package ...)
and putting the plugin in a separate library.
Not that we should merge that into coq-elpi, but we will at least be able to use it
The reason I think we should use a work around for now, is that the fix you were describing with a ".lib" runtime dep folder, is probably gonna take some work to set up in Dune. I am still not fully convinced that it is what we want for doing fl_dynload, but I am not against it either.
Not the same problem, elpi is actually really loading elpi as a dep
their previous methods was broken in 4.08, so hence why Enrico did implement that
Ali Caglayan said:
I will propose the work around of
(package ...)
and putting the plugin in a separate library.
Umm, I think that doesn't work either
We could just depend on package internally, try that, but it is broken by the same bug I think
Actually coq-elpi should work fine with dune now as long as you use the compat syntax
it won't work if we compose it with elpi!
but if elpi is installed in opam, I think that should fine
Umm, maybe we get some problem composing with Coq, but should be very hard to trigger
Indeed, if you look carefully at dep_conf_eval.ml
where (package ...)
is implemented
I don't see why depending on package won't trigger the same bug
What is this doing tho?
let package_install ~(context : Build_context.t) ~(pkg : Package.t) =
let dir =
let dir = Package.dir pkg in
Path.Build.append_source context.build_dir dir
in
let name = Package.name pkg in
sprintf ".%s-files" (Package.Name.to_string name)
|> Alias.Name.of_string |> Alias.make ~dir
Last updated: Jun 10 2023 at 06:31 UTC