Stream: Dune devs & users

Topic: Multiple bindings of same logical path revisited


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"))

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:28):

Let me re-read the discussion

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:28):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:29):

on the other hand the extension use case is legit

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:29):

like done in haskell

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:30):

how do Haskell / Rust handle clashes within their hiearchies?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:31):

I guess we could allow merging paths indeed

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:31):

but even so Coq code should be fixed

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Aug 31 2020 at 19:31):

I think allowing it would be nice to us users

view this post on Zulip Karl Palmskog (Aug 31 2020 at 19:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:32):

The implementation in loadpath.ml is kinda weird

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:33):

it uses a list!

view this post on Zulip Karl Palmskog (Aug 31 2020 at 19:33):

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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

It tries to implement a map using a list

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

See find_load_path etc...

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:34):

so indeed maybe we should cleanup that


Last updated: Oct 16 2021 at 07:02 UTC