Zulip Chat Archive

Stream: general

Topic: olean artifacts for PRs from other repos?

Scott Morrison (Mar 04 2020 at 19:25):

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 (Mar 04 2020 at 19:26):

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 (Mar 04 2020 at 19:27):

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 (Mar 04 2020 at 19:28):

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 (Mar 04 2020 at 19:29):

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

Last updated: Aug 03 2023 at 10:10 UTC