data.finmap mathlib4#1591

Stream: mathlib4

[Shreyas Srinivas]

Hello Everyone,
I am starting to port data.finmap. In order to avoid merge conflicts, please message here before adding commits to the PR.

[Shreyas Srinivas]

The notation introduced in this line: local notation:arg "⟦" a "⟧" => AList.toFinmap a is causing ambiguities that lean complains about. So I am disambiguating by explicitly inserting Alist.toFinmap

[Arien Malec]

I have a fix for replace & can push doc fixes.

[Shreyas Srinivas]

I wish you had let me know. I have a bunch of work on this PR that I have spent 2 hours on that I have to discard.

[Shreyas Srinivas]

It creates merge conflicts for me

[Shreyas Srinivas]

Plus all my work becomes pointless

[Arien Malec]

We can just roll back. Sorry, should have waited longer

[Shreyas Srinivas]

I would like to place a lock on this PR until 23:30 CET

[Johan Commelin]

@Shreyas Srinivas Note that you can use <time-tabcomplete to write timezone aware times in Zulip.

[Shreyas Srinivas]

ah thanks. I had trouble finding the command for the time. I would like to place a lock on the file until : 2023-01-16T23:30:00+01:00 . If I need an extension, I will place a similar time-bound lock again.

[Shreyas Srinivas]

I'm extending the lock for 2 more hours

[Shreyas Srinivas]

I am still working on this. I will release it within an hour or so, since I need to wrap up for the day anyway.

[Shreyas Srinivas]

I am dropping the lock on this. The definition of liftOn does not seem to carry over from lean3's version. I have left the version of the definition from mathport more or less.

[Shreyas Srinivas]

I lock for 3 hours again. :locked:

[Eric Rodriguez]

Not to say that what you're doing is wrong, Shreyas, but I find it funny that VCS like git was originally designed so locking files didn't have to be an issue, and yet here we are lol

[Mauricio Collares]

Microsoft created both Lean and Visual SourceSafe. Coincidence? I do like the terminology there, though: checking out a file was like checking out a book at the library.

(Also not a reply to Shreyas' message! Today's not the first time I was reminded of VSS)

[Ruben Van de Velde]

Well, git will handle this fine - the trouble starts when multiple people are trying to make roughly the same changes to the same file at the same time

[Shreyas Srinivas]

Ruben Van de Velde said:

Well, git will handle this fine - the trouble starts when multiple people are trying to make roughly the same changes to the same file at the same time

I think this might partly be peculiar to the port effort and the workflow that has been adopted here. The normal git flow would work something like this: People make forks of the repo and push there. Then make a pull request from their repo to the port branch. Whichever pull request passes the tests first gets integrated. This is cleaner from a VCS perspective, but has two disadvantages:

1. CI : I am not sure if github requires a premium account for this, but if it does, then not everyone has premium accounts. I am not sure how to get automated build+test on such a workflow.
2. Competing PRs for the same file : This duplicates effort.

[Shreyas Srinivas]

Lock :locked: extension for 1 hour.

[Arien Malec]

I tend to do atomic commits (commit every fix) and push as soon as I commit to reduce the surface area for any merge issue; it also means there's less to regret if there is something I need to redo. The problem really magnifies with large commits and parallel work.

[Shreyas Srinivas]

I am stuck on def liftOn. It seems to be the key to further fixes.

[Shreyas Srinivas]

In fact I think I'd like to ask for help at this point. So I have pushed the file as it stands now.

[Shreyas Srinivas]

lock lifted

[Shreyas Srinivas]

To my eyes, the :locked: (locked) and :unlocked: (unlocked) emojis look too similar

[Shreyas Srinivas]

To me the difference is observable if I look very closely but not otherwise

[Eric Wieser]

Ruben Van de Velde said:

Well, git will handle this fine - the trouble starts when multiple people are trying to make roughly the same changes to the same file at the same time

In my experience, requests to lock files in git usually come down to some combination of:

• Commits being too non-atomic to make merged easy
• Contributors not having experience with dealing with merge conflicts
• Merge conflict resolution tools doing a really bad job on particular kinds of changes

Note that GitHub supports making PRs against other PR branches; this allows you to try out CI on and share a fix without preventing someone else trying something different. The work duplication problem is still there though.