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
As of today,
DirPath.t does belong to
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.
cc: @Pierre-Marie Pédrot @Gaëtan Gilbert @Enrico Tassi @Théo Zimmermann @Matthieu Sozeau
it may make sense to move names or a subset of it to clib
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: Jun 09 2023 at 08:01 UTC