Stream: Coq Universe

Topic: Adding elpi to coq-universe

Roland Coeurjoly Lechuga (Jun 10 2022 at 16:20):

Does it make sense to add elpi to coq-universe? It is not a coq development but it can be used with coq.

Paolo Giarrusso (Jun 10 2022 at 19:18):

I think so, especially since elpi and coq-elpi often evolve in lockstep

Paolo Giarrusso (Jun 10 2022 at 19:20):

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

Emilio Jesús Gallego Arias (Jun 11 2022 at 09:31):

@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

Emilio Jesús Gallego Arias (Jun 11 2022 at 09:31):

Tho I feel that the primary goal of this project is to gather projects that contain .v files, that is to say, Coq projects

Enrico Tassi (Jun 11 2022 at 12:13):

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.

Emilio Jesús Gallego Arias (Jun 11 2022 at 12:27):

They are talking about elpi, not coq-elpi

Paolo Giarrusso (Jun 11 2022 at 18:32):

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

Enrico Tassi (Jun 11 2022 at 20:18):

elpi and coq-elpi go in tandem, but then coupling typically stops there

Ali Caglayan (Jun 14 2022 at 14:10):

@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).

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:11):

Actually we should discuss how to do this

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:11):

because my branch was a hack

Ali Caglayan (Jun 14 2022 at 14:14):

What is the main barrier today? The elpi plugin relying on .elpi files?

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:14):

coq-elpi relying on fl_dynload

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:14):

so we need to update dune

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:15):

that would be easy, if not for this bug

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:15):

https://github.com/ocaml/dune/issues/5833

Ali Caglayan (Jun 14 2022 at 14:16):

Are we talking about the plugin loading or is elpi doing something else with fl_dynload?

Ali Caglayan (Jun 14 2022 at 14:21):

OK so same problem every plugin is having.

Ali Caglayan (Jun 14 2022 at 14:21):

I will propose the work around of (package ...) and putting the plugin in a separate library.

Ali Caglayan (Jun 14 2022 at 14:22):

Not that we should merge that into coq-elpi, but we will at least be able to use it

Ali Caglayan (Jun 14 2022 at 14:31):

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.

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:37):

Not the same problem, elpi is actually really loading elpi as a dep

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:38):

their previous methods was broken in 4.08, so hence why Enrico did implement that

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:39):

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

Emilio Jesús Gallego Arias (Jun 14 2022 at 14:40):

We could just depend on package internally, try that, but it is broken by the same bug I think

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

Actually coq-elpi should work fine with dune now as long as you use the compat syntax

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

it won't work if we compose it with elpi!

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

but if elpi is installed in opam, I think that should fine

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:08):

Umm, maybe we get some problem composing with Coq, but should be very hard to trigger

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:11):

Indeed, if you look carefully at dep_conf_eval.ml

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:11):

where (package ...) is implemented

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:12):

I don't see why depending on package won't trigger the same bug

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:13):

What is this doing tho?

Emilio Jesús Gallego Arias (Jun 14 2022 at 17:13):

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: Nov 29 2023 at 18:01 UTC