Skip to content

[Merged by Bors] - chore: update the migration script to check for necessary permissions and prefer ssh if possible#25701

Closed
mattrobball wants to merge 5 commits intoleanprover-community:masterfrom
mattrobball:update_migration
Closed

[Merged by Bors] - chore: update the migration script to check for necessary permissions and prefer ssh if possible#25701
mattrobball wants to merge 5 commits intoleanprover-community:masterfrom
mattrobball:update_migration

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 11, 2025

PR summary cd8e597ee1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ check_gh_token_scopes()
+ check_ssh_github_access()
+ get_remote_url(repo_name:

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 12, 2025

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jun 12, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 12, 2025

Merge conflict.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 12, 2025

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 12, 2025
… and prefer ssh if possible (#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
@bryangingechen
Copy link
Copy Markdown
Contributor

bors crashed
bors r+

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Jun 12, 2025

Hmm, this isn't showing up in the bors queue for some reason.
bors r+

edit: Now it works, apparently. Maybe bors crashed was causing the previous message to be ignored? 🤷

mathlib-bors bot pushed a commit that referenced this pull request Jun 12, 2025
… and prefer ssh if possible (#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 12, 2025

Pull request successfully merged into master.

Build succeeded:

  • CI Success

@mathlib-bors mathlib-bors bot changed the title chore: update the migration script to check for necessary permissions and prefer ssh if possible [Merged by Bors] - chore: update the migration script to check for necessary permissions and prefer ssh if possible Jun 12, 2025
@mathlib-bors mathlib-bors bot closed this Jun 12, 2025
vlad902 added a commit to vlad902/mathlib4 that referenced this pull request Jun 12, 2025
* master: (447 commits)
  chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707)
  feat: preserve draft status when migrating PRs to fork (leanprover-community#25777)
  chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669)
  refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204)
  feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564)
  fix: outdated docstring (leanprover-community#25717)
  feat(MeasureTheory): convolution of measures with densities  (leanprover-community#25718)
  feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604)
  feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)
  feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333)
  fix: typo in labels_from_comment.yml (leanprover-community#25727)
  feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
  feat: check that the mathlib options exist (leanprover-community#25687)
  feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818)
  refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693)
  feat: allow contributors to remove labels with comments (leanprover-community#25723)
  chore: disable build.yml and bors.yml on forks (leanprover-community#25722)
  feat: improvements to user_activity_report.py (leanprover-community#25721)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  ...
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
… and prefer ssh if possible (leanprover-community#25701)

The sync step requires the gh token to have particular scopes which don't seem standard. So we now check for them and bail if not there. We also check for successfull ssh access to GitHub and use ssh as the protocol for the remote in this case falling back to https.



Co-authored-by: Kim Morrison <kim@tqft.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants