making pull requests

Stream: new members

[Frederick Pu]

So do I need to reclone the repo so that i can actually submit pull requests? Because right now I have my own fork of mathlib4

[Eric Wieser]

You can do git remote add upstream https://github.com/leanprover-community/mathlib4.git I think

[Eric Wieser]

Then push your branch to upstream instead of origin

[Frederick Pu]

I get: error: remote upstream already exists.

[Eric Wieser]

Oh excellent, then probably you're already set up

[Frederick Pu]

Yeah but the upstream repo is my forked one so when I submit a PR is says no changes detected

[Eric Wieser]

Can you show the output of git remote -v?

[Frederick Pu]

upstream https://github.com/leanprover-community/mathlib4.git (fetch)
upstream https://github.com/leanprover-community/mathlib4.git (push)

[Frederick Pu]

so ig it works

[Frederick Pu]

How do I submit a PR through command line?

[Eric Wieser]

git push upstream yourbranchname -u

[Frederick Pu]

Also my PR got rejected cause of this error: s

Label PR and report count

1s

1Run actions/github-script@v5

45(node:1701) [DEP0005] DeprecationWarning: Buffer() is deprecated due to security and usability issues. Please use the Buffer.alloc(), Buffer.allocUnsafe(), or Buffer.from() methods instead.

46(Use node --trace-deprecation ... to show where the warning was created)

47RequestError [HttpError]: Resource not accessible by integration

48 at /home/runner/work/_actions/actions/github-script/v5/dist/index.js:4560:21

49 at processTicksAndRejections (node:internal/process/task_queues:96:5)

50 at async eval (eval at callAsyncFunction (/home/runner/work/_actions/actions/github-script/v5/dist/index.js:4888:16), <anonymous>:18:3)

51 at async main (/home/runner/work/_actions/actions/github-script/v5/dist/index.js:4943:20) {

52 status: 403,

53 response: {

54 url: 'https://api.github.com/repos/leanprover-community/mathlib4/issues/12071/labels',

55 status: 403,

56 headers: {

57 'access-control-allow-origin': '*',

58 'access-control-expose-headers': 'ETag, Link, Location, Retry-After, X-GitHub-OTP, X-RateLimit-Limit, X-RateLimit-Remaining, X-RateLimit-Used, X-RateLimit-Resource, X-RateLimit-Reset, X-OAuth-Scopes, X-Accepted-OAuth-Scopes, X-Poll-Interval, X-GitHub-Media-Type, X-GitHub-SSO, X-GitHub-Request-Id, Deprecation, Sunset',

59 connection: 'close',

60 'content-encoding': 'gzip',

61 'content-security-policy': "default-src 'none'",

62 'content-type': 'application/json; charset=utf-8',

63 date: 'Thu, 11 Apr 2024 19:56:22 GMT',

64 'referrer-policy': 'origin-when-cross-origin, strict-origin-when-cross-origin',

65 server: 'GitHub.com',

66 'strict-transport-security': 'max-age=31536000; includeSubdomains; preload',

67 'transfer-encoding': 'chunked',

68 vary: 'Accept-Encoding, Accept, X-Requested-With',

69 'x-accepted-github-permissions': 'issues=write; pull_requests=write',

70 'x-content-type-options': 'nosniff',

71 'x-frame-options': 'deny',

72 'x-github-api-version-selected': '2022-11-28',

73 'x-github-media-type': 'github.v3',

74 'x-github-request-id': '2042:C4078:FF6427:18BBD0B:66184066',

75 'x-ratelimit-limit': '5000',

76 'x-ratelimit-remaining': '4974',

77 'x-ratelimit-reset': '1712865728',

78 'x-ratelimit-resource': 'core',

79 'x-ratelimit-used': '26',

80 'x-xss-protection': '0'

81 },

82 data: {

83 message: 'Resource not accessible by integration',

84 documentation_url: 'https://docs.github.com/rest/issues/labels#add-labels-to-an-issue'

85 }

86 },

87 request: {

88 method: 'POST',

89 url: 'https://api.github.com/repos/leanprover-community/mathlib4/issues/12071/labels',

90 headers: {

91 accept: 'application/vnd.github.-preview+json',

92 'user-agent': 'actions/github-script octokit-core.js/3.5.1 Node.js/16.20.2 (linux; x64)',

93 authorization: 'token [REDACTED]',

94 'content-type': 'application/json; charset=utf-8'

95 },

96 body: '{"labels":["new-contributor"]}',

97 request: { agent: [Agent], hook: [Function: bound bound register] }

98 }

99}

100Error: Unhandled error: HttpError: Resource not accessible by integration

Complete job

0s

[Eric Wieser]

Regarding the error: @Damiano Testa, it looks like the new contributor tool is welcoming new contributors with an error message!

[Eric Wieser]

Eric Wieser said:

git push upstream yourbranchname -u

Are you sure you did this?

[Frederick Pu]

yes

[Eric Wieser]

Can you show the terminal output it produced? (and run it again if needed)

[Eric Wieser]

Your branch is dual_geo, right? Supposedly you haven't pushed anything yet to upstream

[Frederick Pu]

Screenshot-2024-04-11-164031.png

[Eric Wieser]

It's usually good practice to pick a branch name that includes your username

[Eric Wieser]

Otherwise there's a risk you're clobbering someone elses work

[Frederick Pu]

ok, how do I change my branch name?

[Eric Wieser]

You can run git checkout -b FrederickPu/dual_geo to create a new branch that starts with your current changes

[Eric Wieser]

Then git push upstream FrederickPu/dual_geo -u

[Frederick Pu]

Screenshot-2024-04-11-164342.png

[Frederick Pu]

works now I think

[Eric Wieser]

I just closed your old PR, #12071; please click that link in the CLI output to create one that will behave correctly :)

[Eric Wieser]

(also in future, try to paste code rather than images)

[Damiano Testa]

Eric Wieser said:

Regarding the error: Damiano Testa, it looks like the new contributor tool is welcoming new contributors with an error message!

Why is CI so hard! I'm hoping that this was just because the PR was made from a fork instead of a branch...

[Notification Bot]

95 messages were moved here from #general > Is there any code or division of DualNumbers? by Eric Wieser.