[ refactor ] ScopedSnocList: Swap `Scope` on `SnocList` (Phase 2)

[GulinSS]

Introduces the actual swap of List on SnocList for Scope.

Should this change go in the CHANGELOG?

• [ ] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[GulinSS]

@spcfox prepared a report of building packages.

TLDR; all builds reached complete step of compilation. 🎉

[GulinSS]

@mjustus @gallais

Kindly asking for the review! 🙏

[gallais]

Be aware that it may take a while!

Next week is the TYPES conference The week after that is the CALCO/MFPS joint conferences

We may be able to meet after that but then annual leave may kick in (I'll be away late June to early July).

[GulinSS]

@gallais a reminder at the middle/end of July probably after annual leave

[gallais]

We're meeting tomorrow for a first go at this PR.

[GulinSS]

@gallais @mjustus

should we solve these conflicts or better wait the review?

[mjustus]

I think solving merge conflicts later is the better approach. We tend to do some refactoring during review (e.g. PR #3593) when we spot opportunities that are too tempting to ignore but those shouldn't be too difficult to merge. I am sure Guillaume and I can help resolving conflicts once we are done reviewing.

EDIT: wrong PR number.

[GulinSS]

hm, I've tried to track the changes but this commit is unclear for me. Could you put more info there?

@gallais @mjustus

[gallais]

That last one is ongoing changes that are not thematically linked beyond being part of the review as a whole. We reset the commit before each new session, moving pure refactoring commits past it and then add it back on with all the stuff we've accumulated during the day to it.

[GulinSS]

@gallais @mjustus

FYI Not-so-trivial rebase may occur here

[spcfox]

FYI Not-so-trivial rebase may occur here

I can help with that

[GulinSS]

@gallais @mjustus

Might be better to merge current refactor progress "as is"?

[gallais]

The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while.

[GulinSS]

The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while.

I mean I could take the branch, make a rebase, and finally propose all these changes to merge at this pr. What do you think?

[GulinSS]

I've collected commits from https://github.com/mjustus/Idris2/commit/3578f703cc66160aca0a07526744a41f3797f49c, then added holes to make it compilable as is to see the needed surface to fix. Applied trivial fixes. Working on filling holes.

[GulinSS]

@mjustus @gallais

I've rolled out your refactor intentions over the full codebase and now it compiles just fine, see CI. Actually it only compiles now, not work. My next steps are focused on coming back the working state.

Howbeit I noted that your refactor ideas are a very delicious and at same time pretty accurate. I think while I am busy on coming back working state (that's why I moved this issue to Draft state again) it would be perfect if you would come with more.

I know your time is limited but the deal is to get more your ideas and implement them by my hands as I can.

cc @buzden

[GulinSS]

Short list of all test errors ATM:

idris2/basic/basic055
base/data_bits001
contrib/list_alternating
chez/channels008
chez/chez004
chez/integers
chez/chez032
chez/chez027
refc/buffer
refc/integers
refc/strings
node/node024
node/node004
node/integers

Unfortunately, I am unable to reproduce them locally. crush.Dockerfile.txt

But locally my list of bad tests are:

chez/channels009
chez/channels008
chez/futures001

Continue digging.