olean artifacts for PRs from other repos?

Stream: general

[Scott Morrison]

Is it true that CI only builds downloadable oleans for PRs that come from local branches on the leanprover-community repo, and that PRs from peoples' forks don't generate downloadable oleans?

[Scott Morrison]

I'd hoped to have oleans for #2083 when I checked it out, but they don't seem to be there even though CI liked it.

[Rob Lewis]

Yes, this is true. But note that CI isn't building the tip of the branch that you made the PR from, it's building a merge commit with master. So you wouldn't get oleans anyway.

[Scott Morrison]

Oh.. I thought somehow in the last few days I was successfully getting oleans from azureedge for PRs that I was looking at. Maybe I was over optimistic.

[Rob Lewis]

If the PR is coming from a leanprover-community branch, you'll get oleans, since CI will build the branch as well.