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.
That's one of the TODOs for 1.0 which I didn't settle yet
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"))
Let me re-read the discussion
I'm not sure if that's a dune issue of a Coq issue
I'm not sure we'd like to multiple bind in Coq
b/a.v with both bound to the same loadpath is kind of fragile
ẁ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)
on the other hand the extension use case is legit
like done in haskell
how do Haskell / Rust handle clashes within their hiearchies?
I guess we could allow merging paths indeed
but even so Coq code should be fixed
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
I think allowing it would be nice to us users
and really big projects are likely to use hierarchies of directories anyway
The implementation in
loadpath.ml is kinda weird
it uses a list!
so it just piles on everything? I thought there was some merging logic for sure.
It tries to implement a map using a list
so indeed maybe we should cleanup that
Last updated: Oct 16 2021 at 07:02 UTC