Stream: Dune devs & users

Topic: Multiple bindings of same logical path revisited

Karl Palmskog (Aug 31 2020 at 19:23):

Emilio Jesús Gallego Arias said:

By the way Karl Palmskog , where is the issue for multiple binding of logical paths?

I didn't make an issue since I managed to use copy_files to solve my problem. But I can create one, since this solution may be far from obvious for many people.

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:24):

That's one of the TODOs for 1.0 which I didn't settle yet

Karl Palmskog (Aug 31 2020 at 19:26):

OK, so should I write the issue? Basically the following works, but is a bit awkward and forces creation of another directory:

(copy_files ../core/*.v)
(copy_files  ../extraction/*.v)

(coq.theory
 (name Cheerios)
 (package coq-cheerios)
 (synopsis "Coq library for verified serialization"))

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:28):

Let me re-read the discussion

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:28):

I'm not sure if that's a dune issue of a Coq issue

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:28):

I'm not sure we'd like to multiple bind in Coq

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:29):

having a/a.v and b/a.v with both bound to the same loadpath is kind of fragile

Karl Palmskog (Aug 31 2020 at 19:29):

ẁell, it will break many projects if you stop supporting it in Coq, so it needs to be deprecated now and removed in say 8.15 or later (if you want to remove it from Coq)

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:29):

on the other hand the extension use case is legit

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:29):

like done in haskell

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:30):

how do Haskell / Rust handle clashes within their hiearchies?

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:31):

I guess we could allow merging paths indeed

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:31):

but even so Coq code should be fixed

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:31):

merging the map is not the end of the world, and can be implemented in such a way that we only take a perf hit when used

Karl Palmskog (Aug 31 2020 at 19:31):

I think allowing it would be nice to us users

Karl Palmskog (Aug 31 2020 at 19:32):

and really big projects are likely to use hierarchies of directories anyway

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:32):

The implementation in loadpath.ml is kinda weird

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:33):

it uses a list!

Karl Palmskog (Aug 31 2020 at 19:33):

so it just piles on everything? I thought there was some merging logic for sure.

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

It tries to implement a map using a list

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

See find_load_path etc...

Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

so indeed maybe we should cleanup that

Last updated: Jun 03 2023 at 18:01 UTC