GitHub dependency support

Stream: lean4

[Eric Wieser]

It turns out that it's possible to teach GitHub how to read the lake manifest as part of a CI step, as described at https://docs.github.com/en/code-security/supply-chain-security/understanding-your-software-supply-chain/using-the-dependency-submission-api. It would be neat if someone (maybe at the FRO?) could prototype a GitHub action that does this; perhaps it would enable usage with dependabot or similar

[Eric Wieser]

Ah, looks like dependabot is not accepting new ecosystems

[Eric Wieser]

But dependency info would still be neat

[Henrik Böving]

Eric Wieser said:

Ah, looks like dependabot is not accepting new ecosystems

I mean if we really want to we could fork dependabot right?

[Eric Wieser]

I'm not sure to what extent dependabot relies on being first party

[Yakov Pechersky]

One can run a forked image of dependabot specialized to a language they don't support. Then, in a custom gh workflow, one runs the custom image and executes the API calls against the repo on one's own CI machines.