Zulip Chat Archive
Stream: mathlib4
Topic: Data.Set.Pairwise
Moritz Doll (Dec 23 2022 at 00:08):
@Frédéric Dupuis and zeramorphic you have a race-condition: mathlib4#1176 and mathlib4#1175
Moritz Doll (Dec 23 2022 at 00:09):
@Sky Wilshaw = zeramorphic it seems
Sky Wilshaw (Dec 23 2022 at 00:30):
Oh wow, I guess we both started working on the file at the same time - I checked the open PRs but there wasn't anything at the time!
Sky Wilshaw (Dec 23 2022 at 00:39):
Our branches are almost the same, but we made some different choices in naming convention: for lemmas like
Pairwise (Disjoint on fun c => cond c a b) ↔ Disjoint a b
I chose pairwise_disjoint_on_bool, and Frédéric chose pairwiseDisjoint_on_bool - I think that mine is correct because PairwiseDisjoint isn't the hypothesis. Additionally, there's a panic in mathlib4#1176 on line 68(ish) that doesn't occur on my copy (probably due to a difference in capitalisation). I also golfed some of the unnecessary uses of Set. before lemma names in invocations of simp etc.
Sky Wilshaw (Dec 23 2022 at 00:40):
I did have some incorrect names later in the file that Frédéric did correctly - I've fixed all of them that I saw on my PR mathlib4#1175.
Frédéric Dupuis (Dec 23 2022 at 00:46):
Oh! Yeah, we must have worked on it at the same time.
Frédéric Dupuis (Dec 23 2022 at 00:48):
For pairwise_disjoint_on_bool I hesitated a bit, and I went with pairwiseDisjoint_on_bool since there are similar lemmas lower down that are in the PairwiseDisjoint namespace.
Sky Wilshaw (Dec 23 2022 at 00:48):
I don't know why the panic happened in this file (it also crashed my VS Code language server) but changing Injective to injective fixed it. It's strange to me that something like that caused the language server to completely crash.
Frédéric Dupuis (Dec 23 2022 at 00:48):
Yes, this looks like a bug.
Frédéric Dupuis (Dec 23 2022 at 00:49):
Let's use your PR since you already started "merging" the two.
Sky Wilshaw (Dec 23 2022 at 00:51):
Ok, great. I've copied through a lot of your naming changes. There are a couple of other small aesthetic changes I made to the file as well, feel free to take a look over and revert any of them! I tend to prefer _x rather than _ for example, if there's additionally a hypothesis hx or something else referencing the name x.
Johan Commelin (Dec 23 2022 at 05:01):
Hmm, sorry for that race condition.
Johan Commelin (Dec 23 2022 at 05:02):
#port-status is updated every 30 mins. So there is actually quite a window for such race conditions.
Moritz Doll (Dec 23 2022 at 05:26):
running the port status script by hand makes race conditions very unlikely, but I think in this case it was almost exactly at the same time. If this happens more frequently (which I honestly doubt) we might have consider returning to a long list with manually claiming files
Johan Commelin (Dec 23 2022 at 05:27):
Agreed, let's hope it is indeed rare.
Kevin Buzzard (Dec 23 2022 at 08:54):
Another possibility is that when people start on new files they announce it on this stream. Note that it would also occasionally happen with the old system too.
Ruben Van de Velde (Dec 23 2022 at 09:02):
I'd suggest people run the new script and then push immediately. That way you're guaranteed that github will tell you off if that branch already exists
Ruben Van de Velde (Dec 23 2022 at 09:39):
But not push to master, of course
Riccardo Brasca (Dec 23 2022 at 09:40):
Well, I tried to to exactly this and of course I pushed to master. I am a little bit confused, since VS Code was showing the new branch, but the usual button I use to push did it on master.
Ruben Van de Velde (Dec 23 2022 at 09:44):
Odd
Riccardo Brasca (Dec 23 2022 at 09:48):
image.png
This is my VS code after running the script (I was on master before). It is on the new branch, but if I click on the button it pushes to master, as indicated (I didn't notice it before).
Eric Wieser (Dec 23 2022 at 09:48):
Can you show the full terminal output from running the script?
Riccardo Brasca (Dec 23 2022 at 09:49):
./scripts/start_port.sh Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ set -o pipefail
+ MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
+ PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ TMP_FILE=start_port_tmp.lean
+ mathlib4_path=Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ echo Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ tr / .
++ basename Mathlib.Order.ConditionallyCompleteLattice.Basic.lean .lean
+ mathlib4_mod=Mathlib.Order.ConditionallyCompleteLattice.Basic
+ mathlib3port_url=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Order/ConditionallyCompleteLattice/Basic.lean
+ curl --silent --show-error -o start_port_tmp.lean https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Order/ConditionallyCompleteLattice/Basic.lean
++ grep '^! .*source module '
++ sed 's/.*source module \(.*\)$/\1/'
+ mathlib3_module=order.conditionally_complete_lattice.basic
+ curl --silent --show-error https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ grep -F 'order.conditionally_complete_lattice.basic: '
+ grep mathlib4#
++ dirname Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ mkdir -p Mathlib/Order/ConditionallyCompleteLattice
+ mv start_port_tmp.lean Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ git fetch
+ branch_name=port/Order.ConditionallyCompleteLattice.Basic
+ git checkout -b port/Order.ConditionallyCompleteLattice.Basic origin/master
La branche 'port/Order.ConditionallyCompleteLattice.Basic' est paramétrée pour suivre la branche distante 'master' depuis 'origin'.
Basculement sur la nouvelle branche 'port/Order.ConditionallyCompleteLattice.Basic'
+ git add Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ git commit -m 'Initial file copy from mathport'
[port/Order.ConditionallyCompleteLattice.Basic e732abe0] Initial file copy from mathport
1 file changed, 1484 insertions(+)
create mode 100644 Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ sed -i 's/Mathbin\./Mathlib\./g' Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ echo 'import Mathlib.Order.ConditionallyCompleteLattice.Basic'
+ cat Mathlib.lean
+ LC_ALL=C
+ sort
+ mv -f Mathlib.lean.tmp Mathlib.lean
+ git add Mathlib.lean Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+ git commit -m 'Mathbin -> Mathlib; add import to Mathlib.lean'
[port/Order.ConditionallyCompleteLattice.Basic b9b71d3a] Mathbin -> Mathlib; add import to Mathlib.lean
2 files changed, 5 insertions(+), 4 deletions(-)
Riccardo Brasca (Dec 23 2022 at 09:49):
sorry for the french...
Ruben Van de Velde (Dec 23 2022 at 09:50):
git checkout -b port/Order.ConditionallyCompleteLattice.Basic origin/master
La branche 'port/Order.ConditionallyCompleteLattice.Basic' est paramétrée pour suivre la branche distante 'master' depuis 'origin'.
That sounds suspicious
Eric Wieser (Dec 23 2022 at 09:51):
What does git branch --unset-upstream port/Order.ConditionallyCompleteLattice.Basic do?
Eric Wieser (Dec 23 2022 at 09:52):
I suspect adding that line to the script would solve the problem
Riccardo Brasca (Dec 23 2022 at 09:52):
No output
Eric Wieser (Dec 23 2022 at 09:52):
Ok, but is vscode now not offering a push to master?
Eric Wieser (Dec 23 2022 at 09:52):
You might need to refresh the UI somehow, vscode doesn't know when you run command line things
Riccardo Brasca (Dec 23 2022 at 09:55):
It now says "publish branch", that is the expected behavior I guess
Eric Wieser (Dec 23 2022 at 09:55):
So the correct fix is either to add the --unset-upstream command as I do above (edit: or the equivalent --no-track at creation time), or have the script just push the branch immediately to the right place, at which point it can correct the tracking reference to the right one
Eric Wieser (Dec 23 2022 at 09:57):
Johan Commelin (Dec 23 2022 at 10:02):
@Eric Wieser Thanks for that fix!
Eric Wieser (Dec 23 2022 at 10:13):
It might still be worth having it immediately push the branch, but then the script needs to learn to handle cases where someone else already pushed the same branch, so I left that for a follow-up
Eric Wieser (Dec 23 2022 at 10:14):
We might want to disable force-pushes for port/* branches to avoid people accidentally cloberring each other's work
Johan Commelin (Dec 23 2022 at 10:31):
Does github support that? If so, sounds like a good idea.
Ruben Van de Velde (Dec 23 2022 at 10:40):
Eric Wieser said:
It might still be worth having it immediately push the branch, but then the script needs to learn to handle cases where someone else already pushed the same branch, so I left that for a follow-up
Well, the only thing the script needs to do is error, which git will do by default :)
Eric Wieser (Dec 23 2022 at 10:51):
It needs to detect the error and explain what went wrong, otherwise people will claim there is a bug in the script :)
Sky Wilshaw (Dec 23 2022 at 19:41):
Johan Commelin said:
Hmm, sorry for that race condition.
No need to apologise - from what I can tell, we both started making our PRs so close to each other that even updating #port-status every time a branch was created might even be too slow! I think the solution with the new script looks very useful.
Last updated: Dec 20 2023 at 11:08 UTC