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