Zulip Chat Archive

Stream: general

Topic: olean artifacts for PRs from other repos?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 12:18 UTC