Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(geometry/manifold): Some lemmas for smooth functions #7752

Closed
wants to merge 130 commits into from
Closed

[Merged by Bors] - feat(geometry/manifold): Some lemmas for smooth functions #7752

wants to merge 130 commits into from

Conversation

Nicknamen
Copy link
Collaborator

Open in Gitpod

@Nicknamen
recreated the problem
03df6e2
@Nicknamen
Proved that continuous functions are an algebra
80b9cab
@Nicknamen
Merge branch 'master' into continuous_functions_algebra
d8ad078
@Nicknamen
Solving a conflict appeared in sheaves
56d2716
@Nicknamen
Corrected a mistake in the documentation
da64672
@Nicknamen
Solved a DANGEROUS INSTANCE problem
53b8e04
@Nicknamen
Forgot to remove #lint
fee8ca8
@Nicknamen
Making lint happy
dc6197b
@Nicknamen
Trying again to make lint happy
b807d94
@Nicknamen
Algebra structure over continuous bundled functions
4652e8a
@Nicknamen
Trying to merge
20866d7
@Nicknamen
Having problems with the merging
99cee94
@Nicknamen
Updated the code following smooth manifolds PR
ac6c3ba
@Nicknamen
Merge branch 'master' into Lie_groups
c8f1304
@Nicknamen
Merge branch 'master' into continuous_functions_algebra
f31adad
@Nicknamen
Merge branch 'continuous_functions_algebra' into continuous_bundled_map
fd3efc7
@Nicknamen
Added some documentation
a9bdde6
@Nicknamen
Merge branch 'Lie_groups' into smooth_map
1c3e998
@Nicknamen
Begun writing smooth_functions
f91678e
@Nicknamen
Merge branch 'master' into Lie_groups
46af74b
@Nicknamen
Added some documentation
f5abebf
@Nicknamen
Trying to show to Wojtek the excessive memory consumption
5288ed0
@Nicknamen
Merge branch 'master' into continuous_functions_algebra
3f5fa6d
@Nicknamen
Forgot to save files before last commit.
ee83faa
@Nicknamen
Merge branch 'master' into continuous_functions_algebra
37a21d4
@Nicknamen
Merge branch 'continuous_functions_algebra' into has_continuous_mul
629ad00
@Nicknamen
Merge branch 'has_continuous_mul' into continuous_bundled_map
ee812a2
@Nicknamen
Added some further documentation
283dd6e
@Nicknamen
Merge branch 'continuous_bundled_map' into smooth_map
3a3011d
@Nicknamen
Merge branch 'continuous_bundled_map' into Lie_groups
fcb4714
@Nicknamen
Copy link
Collaborator Author

bors merge

@Nicknamen
Copy link
Collaborator Author

I don't know what is going on! Please help!

@Nicknamen Nicknamen added the help-wanted The author needs attention to resolve issues label Jun 9, 2021
@bryangingechen
Copy link
Collaborator

@Nicknamen This is on the bors queue already; it's just taking some time due to downtime and various failures yesterday: https://app.bors.tech/repositories/24316

@Nicknamen
Copy link
Collaborator Author

I don't need to do anything then? Even if they are colored in red in the list you linked?

bors bot pushed a commit that referenced this pull request Jun 10, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
46760cf
@sgouezel sgouezel mentioned this pull request Jun 10, 2021
Closed
@bryangingechen
Copy link
Collaborator

I don't need to do anything then? Even if they are colored in red in the list you linked?

If some action is necessary bors should report back here with a comment like "Build failed" (without saying "Retrying..." at the end). Though sometimes we can figure out before bors that a certain PR can't be merged, e.g. if there's a merge conflict with master or if the build logs of some failed batch point to a PR as a culprit.

@bors
Copy link

bors bot commented Jun 10, 2021

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

bors bot pushed a commit that referenced this pull request Jun 10, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
078a38f
@bors
Copy link

bors bot commented Jun 11, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jun 11, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
2b11c28
@bors
Copy link

bors bot commented Jun 11, 2021

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Jun 11, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
83e62c9
@bors
Copy link

bors bot commented Jun 11, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jun 11, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
3d91631
@bors
Copy link

bors bot commented Jun 11, 2021

Build failed (retrying...):

@Nicknamen Nicknamen closed this Jun 11, 2021
@leanprover-community leanprover-community locked and limited conversation to collaborators Jun 11, 2021
@Nicknamen Nicknamen reopened this Jun 11, 2021
@leanprover-community leanprover-community unlocked this conversation Jun 11, 2021
bors bot pushed a commit that referenced this pull request Jun 12, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
9f700a2
@bors
Copy link

bors bot commented Jun 12, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jun 12, 2021
@Nicknamen
feat(geometry/manifold): Some lemmas for smooth functions (#7752)
f9935ed
@bors
Copy link

bors bot commented Jun 12, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(geometry/manifold): Some lemmas for smooth functions [Merged by Bors] - feat(geometry/manifold): Some lemmas for smooth functions Jun 12, 2021
@bors bors bot closed this Jun 12, 2021
@bors bors bot deleted the smooth_preliminary branch June 12, 2021 17:11
@Nicknamen Nicknamen added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed help-wanted The author needs attention to resolve issues labels Jul 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@Nicknamen @bryangingechen @sgouezel @gebner