The features of proof-general doesn't seem to be "browsable" in epkg.

[erikmd]

dear @tarsius, dear all,

after the merge of ProofGeneral/PG#627,
I ran epkg-update to see if the license change was updated in epkg accordingly.
And, yes 👍

But meanwhile, I've noticed that several features that are part of proof-general are not browsable/clickable,

cf. the following screenshot obtained with GNU Emacs 26.1 on GNU/Linux Debian:

Would you have an idea/explanation of this (minor) issue?

[tarsius]

You can only view libraries that have already been installed. Did you use borg to install this package and did you try restarting Emacs?

[erikmd]

No, I didn't use borg, I use a regular MELPA + use-package install (basically, with this .emacs)

So I was especially using M-x epkg-list-packages to benefit from its detailed metadata (not for installing the package)

Thus at first, I was puzzled to see that some features are "detected", and other not…

[erikmd]

But I guess that when you said

You can only view libraries that have already been installed.

You also meant that requiring the features (or opening a buffer attached to the corresponding features) should mark them as "browsable".

And, indeed, it seems there is no "issue" actually 😅

[erikmd]

After opening a coq.v file and reloading the buffer, I get this:

So thanks for your feedback! I guess we can mark the question as closed :)