Generated JSON data does not contain any link to the sources of the packages.

[Zimmi48]

This is quite unfortunate as it does not allow to solve the issue that was raised in this thread: https://coq.discourse.group/t/coqhammer-1-1-1-for-coq-8-9/327.

The CoqGym (@yangky11) people crawled the Coq package index to get the URLs of packages.
Now they could obtain exactly the same results by doing cat coq-packages.json | jq '.[][1].versions[0].homepage', which is already an improvement.
However, it doesn't solve their bug which is to confuse the homepage of a package and the repository URL. It just happened that this confusion gave them correct results in most cases, but not for instance for math-classes and corn (as remarked by @spitters).

Would it be doable to add more meta-information to reflect, both the repository as declared in the opam meta-data, but also the URL of sources, which is defined there as well?

[ejgallego]

Now that you mention the CoqGym use case, this is indeed an open problem in the upstream OCaml / OPAM world, you have the dune-universe repositories but a solution for a coherent view on the package world has still not been developed AFAICT. There are some issues lurking around tho.

[maximedenes]

Would it be doable to add more meta-information to reflect, both the repository as declared in the opam meta-data, but also the URL of sources, which is defined there as well?

Yes, I plan to add all the necessary metadata. In fact, we may want to generate OPAM and Nix packages from the metadata at some point (so they should contain URLs to the source, build instructions, etc).

For now, the JSON data contains only what is needed by the web interface (I wanted to achieve separation between the website and the package index).

[spitters]

Has there been any progress on this? I'm curious about CoqGym/coq_hammer.

[maximedenes]

I personally won't have time to work on it before September, I'm afraid.

[spitters]

@maximedenes It's September ;-)
It would be nice to provide Coq hammer with some better data.

[maximedenes]

Working on it now.

[maximedenes]

It seems that a few packages do not use the standard src attribute to point to their source. For example, paco uses http: https://github.com/coq/opam-coq-archive/blob/ba1715ee0406795a003de50b9abaa95ae5d91398/released/packages/coq-paco/coq-paco.4.0.0/opam#L34

I couldn't find a documentation of the allowed attributes, so I'm adding support only for src for now. I'd be happy to receive a documentation pointer, though. @Zimmi48 do you happen to know what's allowed in these files?

[palmskog]

@maximedenes from the OPAM manual the allowed attributes are:

"One of src: <string> or archive: <string>, specifying the URL where the package can be downloaded from. When using HTTP or FTP, this should be an archive. The older alternative field names http:, local:, git:, hg: and darcs: are deprecated, prefer explicit URLs."

So basically http is allowed but deprecated.

[maximedenes]

Ah, thanks a lot! I guess I'll support the two non-deprecated names. Will update my PR.

[Zimmi48]

We could also do a pass on the repository to fix all the deprecated fields...