Emilio Jesús Gallego Arias (May 27 2021 at 15:07): Emilio Jesús Gallego Arias (May 27 2021 at 15:07):Hi folks, I'm gonna try to finish the PR adding a library so common tools can handle in a central way loadpaths and other stuff such as locating files, PR #14059 https://github.com/coq/coq/pull/14059 is more or less ready [just need to tweak the API a bit], however loadpath code requires taking a choice regarding DirPath.t.
As of today, DirPath.t does belong to coq.kernel, so coq.loadpath could depend on it, unfortunately this is not OK for a few tools such as coqdep or coqdoc which have no reason to link to the kernel. There are a few different options, and I am not sure what would be the best. Moreover, DirPath does depend on Id and a few other routines such as Pp, but that's easier to fix.
So I wonder what to do... a possibility would be just to introduce a coq.dirpath (or coq.identifiers) library, which can be then depended upon by the rest, however I don't like this a lot as Loadpath should actually own the DirPath data type [as i assume we won't expose the internals as it is now], so I dunno.
Any ideas?
cc: @Pierre-Marie Pédrot @Gaëtan Gilbert @Enrico Tassi @Théo Zimmermann @Matthieu Sozeau
Gaëtan Gilbert (May 27 2021 at 17:25):it may make sense to move names or a subset of it to clib
Emilio Jesús Gallego Arias (May 28 2021 at 00:09):Yup, will try something to get at least the duplicated code in one place, but I'm afraid it will take a few iterations to get right
Last updated: Dec 05 2023 at 12:01 UTC