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
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: Dec 05 2023 at 12:01 UTC