[Merged by Bors] - feat: do not modify the working tree when running start_port.sh #2598
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This means that it always succeeds, even if a port has already happened. It also prevents it from clobbering local changes.
eric-wieser
force-pushed
the
eric-wieser/better-start-port.sh
branch
from
195c48e
to
84b1c2c
Compare
bors bot
pushed a commit
that referenced
this pull request
Mar 4, 2023
This means that it always succeeds, even if a port has already happened. It also prevents it from clobbering local changes.
The new behavior is:
```sh
# this file is ported
$ scripts/start_port.sh Mathlib/Algebra/Algebra/Basic.lean
Checking out a new branch in a temporary working tree
Downloading latest version from mathlib3port
Applying automated fixes
Successfully created initial commits:
* 865bcb6d automated fixes
* 72c365f7 Initial file copy from mathport
* 43748fcf feat: port Algebra.Algebra.Basic
WARNING: this file has already been ported!
To continue anyway with a fresh port, you can run
git checkout 865bcb6d548e990a7214a3a168389f731a975aa8 -b port/Algebra.Algebra.Basic-again
```
```sh
# this file is in progress
$ scripts/start_port.sh Mathlib/Algebra/Algebra/Operations.lean
Checking out a new branch in a temporary working tree
Downloading latest version from mathlib3port
Applying automated fixes
Successfully created initial commits:
* 66beceb7 automated fixes
* 209e1206 Initial file copy from mathport
* 250226b3 feat: port Algebra.Algebra.Operations
WARNING: The file is already in the process of being ported in mathlib4#2568.
To continue anyway with a fresh port, you can run
git checkout 66beceb792782206d6fdf60822bffcb14779c2b0 -b port/Algebra.Algebra.Operations-<some-suffix>
```
```sh
# this file is not ported
$ scripts/start_port.sh Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Checking out a new branch in a temporary working tree
Downloading latest version from mathlib3port
Applying automated fixes
Successfully created initial commits:
* 93e0eb94 automated fixes
* d57e8e8f Initial file copy from mathport
* 6716afb6 feat: port Algebra.Algebra.Subalgebra.Basic
Checking out a new port/Algebra.Algebra.Subalgebra.Basic branch from 93e0eb94e59146036141385b0a94cef93dd9ffc7
M Mathlib.lean
Switched to a new branch 'port/Algebra.Algebra.Subalgebra.Basic'
After pushing, you can open a PR at:
https://github.com/leanprover-community/mathlib4/compare/port/Algebra.Algebra.Subalgebra.Basic?expand=1&title=feat:+port+Algebra.Algebra.Subalgebra.Basic&labels=mathlib-port
```
The approach here is taken from https://github.com/ion1/git-plumbing-create-commit/blob/master/git-plumbing-create-commit
This mostly makes #2249 obsolete.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
eric-wieser
commented
Mar 4, 2023
Comment on lines
-71
to
-72
| (echo "import $mathlib4_mod" ; cat Mathlib.lean) | LC_ALL=C sort | uniq > Mathlib.lean.tmp | ||
| mv -f Mathlib.lean.tmp Mathlib.lean |
There was a problem hiding this comment.
Oops, I somehow lost these lines in the change.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This means that it always succeeds, even if a port has already happened. It also prevents it from clobbering local changes.
The new behavior is:
The approach here is taken from https://github.com/ion1/git-plumbing-create-commit/blob/master/git-plumbing-create-commit
This mostly makes #2249 obsolete.