Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
GulinSS wants to merge 7 commits into
base: main
Choose a base branch
from
Open

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

GulinSS wants to merge 7 commits into from
+3,254 −2,653

Conversation

@GulinSS
Copy link
Contributor

@GulinSS GulinSS commented Mar 19, 2025 •
edited
Loading

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 GulinSS mentioned this pull request Mar 19, 2025
Closed
1 task
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from 2a9fa0b to b68532b Compare March 24, 2025 17:15
@GulinSS GulinSS mentioned this pull request Mar 25, 2025
Open
@GulinSS
Copy link
Contributor Author

GulinSS commented Mar 25, 2025 •
edited
Loading

@spcfox prepared a report of building packages.

TLDR; all builds reached complete step of compilation. 🎉

@GulinSS GulinSS mentioned this pull request Apr 3, 2025
Merged
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch 4 times, most recently from bed6788 to ff61ad5 Compare April 21, 2025 13:29
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from ff61ad5 to 9367788 Compare May 12, 2025 11:42
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from 9367788 to 5278b55 Compare June 3, 2025 07:20
@GulinSS GulinSS marked this pull request as ready for review June 3, 2025 07:22
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from 33f2799 to 749fa54 Compare June 5, 2025 07:16
@GulinSS
Copy link
Contributor Author

GulinSS commented Jun 5, 2025 •
edited
Loading

@mjustus
@gallais

Kindly asking for the review! 🙏

@gallais
Copy link
Member

gallais commented Jun 5, 2025

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 GulinSS force-pushed the scoped-snoc-list-swap branch from 749fa54 to c128cdf Compare July 8, 2025 07:25
@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from c128cdf to cf57ff6 Compare July 17, 2025 13:45
@GulinSS
Copy link
Contributor Author

GulinSS commented Jul 22, 2025

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

@gallais
Copy link
Member

gallais commented Jul 29, 2025

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

@GulinSS
Copy link
Contributor Author

GulinSS commented Aug 8, 2025 •
edited
Loading

@gallais
@mjustus

should we solve these conflicts or better wait the review?

@mjustus
Copy link
Collaborator

mjustus commented Aug 8, 2025 •
edited
Loading

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
Copy link
Contributor Author

GulinSS commented Aug 19, 2025

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

@gallais
@mjustus

@gallais
Copy link
Member

gallais commented Aug 20, 2025

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
Copy link
Contributor Author

GulinSS commented Aug 26, 2025

@gallais
@mjustus

FYI Not-so-trivial rebase may occur here

@spcfox
Copy link
Contributor

spcfox commented Aug 26, 2025

FYI Not-so-trivial rebase may occur here

I can help with that

@GulinSS
Copy link
Contributor Author

GulinSS commented Sep 4, 2025 •
edited
Loading

@gallais
@mjustus

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

@gallais
Copy link
Member

gallais commented Sep 4, 2025

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
Copy link
Contributor Author

GulinSS commented Sep 4, 2025 •
edited
Loading

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?

@gallais gallais mentioned this pull request Oct 17, 2025
Draft
2 tasks
@GulinSS
Copy link
Contributor Author

GulinSS commented Oct 31, 2025

I've collected commits from mjustus@3578f70, then added holes to make it compilable as is to see the needed surface to fix. Applied trivial fixes. Working on filling holes.

@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch 5 times, most recently from 7470b35 to 3ba6e08 Compare January 4, 2026 13:58
@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 4, 2026

@gallais
@mjustus

We are completely ready.

@dunhamsteve dunhamsteve mentioned this pull request Jan 7, 2026
Open
1 task
@Matthew-Mosior
Copy link
Contributor

Matthew-Mosior commented Jan 7, 2026 •
edited
Loading

@GulinSS

Would you be opposed to considering updating to v10.0.0 for Chez and Racket? #3704 requires at least v10.0.0 to make use of the fx*/wraparound function (#3704 optimizes Chez, Racket and Gambit BitsXY operations using fixnums).

@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026 •
edited
Loading

Would you be opposed to considering updating to v10.0.0 for Chez and Racket?

@Matthew-Mosior

Sure, I will try update Chez and Racket to minimal version which support fixnums and see how it will affect the build process.

@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026 •
edited
Loading

Some experiments with time measurements.

Time to build this branch by a compiler which are at the main (11 attempts):

real user sys user + sys
250,426 230,586 13,449 244,035
238,694 222,482 9,713 232,195
256,586 239,546 10,157 249,703
250,233 232,546 10,641 243,187
261,402 243,578 10,781 254,359
239,748 225,282 8,428 233,71
229,52 215,358 8,179 223,537
245,785 231,464 8,295 239,759
238,167 224,073 8,121 232,194
243,716 229,335 8,31 237,645
246,774 232,511 8,13 240,641

Actually we use user + sys as a time measurement to exclude time of locking. So, we are interested in CPU-time, not real one. Also we are going to use user and sys time as a sum per line because different attempt might select different routes to execute system calls.

Average time = 239.177
SD = 8.705

Time to build this branch by a compiler which is compiled from this branch (11 attempts):

real user sys user + sys
244,773 230,275 8,528 238,803
232,398 218,261 8,239 226,5
227,865 213,734 8,171 221,905
225,595 211,144 8,452 219,596
226,323 211,932 8,357 220,289
228,049 213,582 8,351 221,933
231,204 216,316 8,629 224,945
230,859 216,807 8,11 224,917
239,344 224,496 8,623 233,119
229,391 215,142 8,232 223,374
229,239 214,248 8,605 222,853 
Average time = 225.294
SD = 5.791

Well, 239.177s - 225.294s = 13.883s but need to check it at least by Welch:

t ~= 4.40
v ~= 17.40
p ~= 0.0003

So, really, the compiler with applied our Snoc refactor is totally no slower than its origin version at main branch ATM: p << 0.05.

@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026 •
edited
Loading

@Matthew-Mosior

I see no 10 version of Racket here: https://download.racket-lang.org/releases/. Will 9.x work?

It seems that https://docs.racket-lang.org/reference/fixnums.html states that it should be present at 9.x already.

@Matthew-Mosior
Copy link
Contributor

Matthew-Mosior commented Jan 8, 2026 •
edited
Loading

@Matthew-Mosior

I see no 10 version of Racket here: https://download.racket-lang.org/releases/. Will 9.x work?

Yep, that will work (I think I conflated the necessary Chez Scheme version (v10.0.0) and Racket version (v7.9 and above).

@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from 3ba6e08 to 20a8850 Compare January 8, 2026 16:48
@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026

@Matthew-Mosior at first attempt it works for 10.0.0 but I am going to try a mutex fix for directory operations with pinning 10.3.0.

@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch 2 times, most recently from 9b2e4b7 to 75c1a7d Compare January 8, 2026 18:04
@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026 •
edited
Loading

A trivial approach does not work. Going to rollback to a solution with pinned 10.0.0.

It works!

GulinSS and others added 7 commits January 9, 2026 00:03
@GulinSS
[ support ] Add thread safety to directory operations
2948d89 
Add pthread mutex to DirInfo structure to protect against concurrent
access when reading directory entries. This fixes "Cannot allocate memory"
errors that occurred due to thread safety issues with readdir.

The deprecated readdir_r function is no longer used, so we implement
proper mutex locking around readdir calls instead. Mutex is initialized
when opening a directory and destroyed when closing it.

- Add pthread.h include for mutex operations
- Initialize mutex in idris2_openDir with error handling
- Add mutex lock/unlock around idris2_nextDirEntry
- Destroy mutex in idris2_closeDir
@GulinSS
[ ci ] Pin macOS dependencies
7d9bc14 
- Pin Node.js installation from latest to version 24 for consistency (version 24 is currently the latest)
- Pin Chez Scheme installation to specific version 10.3.0 (10.x is required by coming idris-lang#3704)
- Add pinned Racket installation via Homebrew cask to run Racket backend tests on macOS
@GulinSS @mjustus
[ refactor ] replace showSep and join by Data.String.joinBy
d905dc0 
Co-authored-by: Justus Matthiesen <[email protected]>
@GulinSS
[ refactor ] Introduce NestedNames.empty
48ab094
@GulinSS
[ refactor, linearity ] Optimize erased variable tracking with VarSet
5f4a92b 
Replace List-based tracking of erased variables with specialized VarSet type for improved performance. Changes include:

- Update getErased function in Env.idr to return VarSet instead of List
- Modify linear check functions to use VarSet operations throughout
- Add elemNat helper for efficient natural number lookups in VarSet
- Use VarSet.empty constant instead of empty lists
- Apply proper weakening operations with varSetWeaken interface

This improves efficiency of linearity checking by using specialized set operations instead of list traversals.
@GulinSS
[ refactor ] ScopedSnocList: Swap Scope on SnocList (Phase 2)
a7cd792 
+ Cherry-picked refactor from #16

Co-authored-by: Viktor Yudov <[email protected]>

fix
@mjustus @GulinSS
[ refactor ] ScopedSnocList: Review-flavoured squashed refactor
09c6d74 
- generalised lookup
- define resolveRef as the weakening of findBound, add missing cases to substName
- define underBinders, fix argument order
- added underBinderz, more GenWeakenable instances
- complete refactors regarding swapping inner/outer
- change constructor argument representation from Scope to List Name

Co-authored-by: Justus Matthiesen <[email protected]>
@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 8, 2026

It seemed to work fine with mutex and chez 10.3.0.

@dunhamsteve thanks for the pointing!

@GulinSS GulinSS force-pushed the scoped-snoc-list-swap branch from 109335e to 09c6d74 Compare January 8, 2026 21:06
Matthew-Mosior added a commit to Matthew-Mosior/Idris2 that referenced this pull request Jan 8, 2026
@Matthew-Mosior
Updating .github/workflows/ci-idris2-and-libs.yml to match idris-lang…
9b071c2 
…#3513.
@Matthew-Mosior
Copy link
Contributor

Matthew-Mosior commented Jan 9, 2026 •
edited
Loading

I tried the .github/workflows/ci-idris2-and-libs.yml from this PR in #3704, and it appeared that a few of the checks fail?

@GulinSS
Copy link
Contributor Author

GulinSS commented Jan 9, 2026 •
edited
Loading

@Matthew-Mosior I responded there about your CI pipeline. It seemed to me you tried not only my changes but with something else, so, the issue might be at something else.

Matthew-Mosior added a commit to Matthew-Mosior/Idris2 that referenced this pull request Jan 9, 2026
@Matthew-Mosior
Trying to update .github/workflows/ci-idris2-and-libs.yml to idris-la…
45a5005 
…ng#3513 (again).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@GulinSS @gallais @mjustus @spcfox @Matthew-Mosior