Stream: Coq devs & plugin devs

Topic: LoadPath library organization


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

view this post on Zulip Gaëtan Gilbert (May 27 2021 at 17:25):

it may make sense to move names or a subset of it to clib

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC