-
Notifications
You must be signed in to change notification settings - Fork 385
[ refactor ] ScopedSnocList: Preparing for the long jump (Phase 1) #3512
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.
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
base: main
Are you sure you want to change the base?
Conversation
Core idea is to split the process of transition from List-based Context on SnocList-based Context on 2 phases: 1. Apply a refactor which does not make any transition (even no observable changes for Idris users) actually but prepare the code for future update. 2. Roll out the transition with limited code changes invasion because it was partially done at the step before. Co-authored-by: Viktor Yudov <[email protected]>
a8c6014
to
f7bc725
Compare
Thanks for that. FYI we (including at least @mjustus & me) are planning to do a big code review |
@gallais much appreciate! 😇 |
@gallais, @mjustus shy reminder about the review and its importance! 🙏 We are going to make further steps of adding parts from Yaffle when this PR and its companion will succeed. All this is a refactor which is important but these steps actually are preparations for something which can be added to the change log . And this step is scheduled to start the development after these 2 phases. So, moving forward here is a corner stone to unlock further Idris improvements. All this is clear for invited people just it seemed important to explicitly emphasize at the message due of questions at Discord group. |
We went through about a 3rd of the files. There a semantic issues (e.g. some lists of values being |
@gallais any news would be very appreciate! We are in progress of porting other parts from It would be nice if you can put a link to PR/commits/branch/anything where we might participate during the review process. If it is needed of course. |
Ping @mjustus We haven't had the opportunity to have another meeting yet. And with |
f7bc725
to
3decb09
Compare
Pinned for watching: https://github.com/mjustus/Idris2/tree/scoped-snoc-list-preparing-review |
e5faef5
to
34ebbf0
Compare
We met up today (thanks Justus for your hospitality!) and we've made good progress. |
34ebbf0
to
c3a8909
Compare
I have pushed your current state to branch snoc-list-preparing-force-pushed on my copy of the repository and am about to revert this branch to f7bc725 because it was getting too difficult reviewing a moving target with large merge conflict. |
c3a8909
to
f7bc725
Compare
Core idea is to split the process of transition from List-based Scope on SnocList-based Scope on 2 phases: