Good first issues for new contibutors?

Stream: iris-lean

[Michael Sammler]

Hi, I am wondering what the status of iris-lean is and in particular, what parts of it would be good to contribute to for someone who is interested in working with Iris in lean? Is there is list of things that need to be ported or something similar?

[Shreyas Srinivas]

@Markus de Medeiros is the main person pushing this forward

[Shreyas Srinivas]

He has a plan for the port in his blog

[Shreyas Srinivas]

And there is the task list here :

[Shreyas Srinivas]

#iris-lean > Next steps @ 💬

[Shreyas Srinivas]

this was the post I think : https://www.markusde.ca/pages/eileen.html

[Shreyas Srinivas]

Fwiw, I have some spare time on my hands, now that my work on the equational theories project is at its last stages, so I would also like to join.

[Markus de Medeiros]

Hi Michael! We've ported iProp, so the next major step is to upgrade some of the tactics so that we can start doing some of the proofs inside the logic (iris-lean is missing iApply and iMod). If you really want to take a look then be my guest, otherwise I plan to start making a plan to port those parts of mosel next weekend.

Out of curiosity, are you looking for tasks for yourself, or for someone else? I've also been in contact with Ralf and Max about a student at ETH who might want to help the effort. As for more introductory tasks, there are plenty of CMRA's that we have not yet ported, and would introduce someone new to Iris as a whole. There is also the challenge of porting the language hierarchy, which @Quang Dao was working on at one point. Of course, there will also be plenty of things to port inside the logic once we get the tactics working.

[Markus de Medeiros]

I can come up with a list of CMRA's that are incomplete today if that would be useful to you (or Shreyas)

[Shreyas Srinivas]

Fwiw, I think the github project approach we used at ETP might be a good way to keep up with progress on this. We just have to setup the project and borrow the CI scripts from there. It's useful to keep track of what's done and what remains.

[Markus de Medeiros]

Anything that might help organize this project is cool with me! Mario is in control of the GitHub so you ask him about this

[Michael Sammler]

Thanks for this status update! I am mainly asking since I will have two interns starting in June who will likely do something with Iris and Lean and having some beginner issues would be nice for them to get to know the code base.

Shreyas Srinivas said:

Fwiw, I think the github project approach we used at ETP might be a good way to keep up with progress on this. We just have to setup the project and borrow the CI scripts from there. It's useful to keep track of what's done and what remains.

Having something for tracking open issues and who is working on them would be great! This would make it a lot easier when the interns start and need things to work on.

[Michael Sammler]

I guess you refer to this? https://github.com/users/teorth/projects/1 I think having something like this for Iris Lean would be great. How tricky would it be to set that up?

[Shreyas Srinivas]

Yeah

[Shreyas Srinivas]

That was my idea

[Shreyas Srinivas]

It’s not too difficult now that we know what works

[Shreyas Srinivas]

And have all the CI scripts ready

[Shreyas Srinivas]

Only a repository maintainer can set them up though

[Shreyas Srinivas]

It’s basically a reverse ticket system.

[Michael Sammler]

I found this for explaining how the system works: https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md

@Mario Carneiro What do you think about having something like this for Iris lean?

Alternatively, one could just a more lightweight approach where one just works with issues directly instead of having a project and the automatic claiming setup. I guess iris lean will be on a bit of a smaller scale than ETP.

[Mario Carneiro]

I think iris-lean is not at the stage where we need a heavyweight task setup. We rarely have more than one person working at a time to begin with

[Mario Carneiro]

I think issues will be fine

[Shreyas Srinivas]

Yeah I wrote the initial version of that. Basically the key difference between using plain GitHub issues and this is that it collects the big tasks together and gives maintainers control over issues and helps avoid overlaps.

[Shreyas Srinivas]

And lets people work in peace on the tasks they pick without worry of overlap.

[Mario Carneiro]

If we get multiple people working in parallel on iris-lean, the main concern will be that while it's easy to find a task, the list of tasks is maybe a bit linear right now so the chance of overlap is high

[Mario Carneiro]

Having issues and posting claims as comments on the issues should be more than sufficient for this

[Mario Carneiro]

or alternatively, using zulip threads here

[Michael Sammler]

Mario Carneiro said:

If we get multiple people working in parallel on iris-lean, the main concern will be that while it's easy to find a task, the list of tasks is maybe a bit linear right now so the chance of overlap is high

I think there might be a few orthogonal directions, like more cmra combinators, proof mode, heaplang, ... But I have to say that I don't really have an overview at the moment of what the state is and what people are working on. Would it be possible to create issues for the main points that are open at the moment?
This would be very useful to get an overview.

[Mario Carneiro]

indeed I think there is a fair amount of fanout but because there are some obvious things that are important and missing people will be drawn to that without some kind of claiming system

[Michael Sammler]

Indeed, I agree. A claiming system would be very useful I think, even if it is very low tech (e.g. comments on issues).

[Shreyas Srinivas]

Then it is advisable to use the ticket system

[Shreyas Srinivas]

It automates the claiming process

[Shreyas Srinivas]

It also attaches PRs to the corresponding issues and moves them automatically to the review queue when it is ready

[Markus de Medeiros]

Michael Sammler said:

I am mainly asking since I will have two interns starting in June who will likely do something with Iris and Lean and having some beginner issues would be nice for them to get to know the code base.

Exciting! I assume you're also in touch with Ralf about this.

[Markus de Medeiros]

For now, I'll just make some issues for the features that could be implemented without any overlap. This is probably overdue haha.

[Shreyas Srinivas]

Sounds good. I found last time that it’s easiest for new contributors if the issues are byte-sized.

[Shreyas Srinivas]

Do you have a standard reference we are following. I recall from mastodon that there might be some divergence from the rocq version of iris to simplify design and adopt lessons from later work.

[Mario Carneiro]

We're making some minor changes on the fly but for the most part the roadmap is to do the things in iris master branch

[Markus de Medeiros]

Yes. Main Iris has also started generalizing some things to the transfinite case--I'm assuming we just want to skip this for now?

[Mario Carneiro]

oh really? I thought that was still contentious

[Mario Carneiro]

IIUC it has tradeoffs, it's not just a generalization

[Markus de Medeiros]

Well, they're generalizing it piece by piece, and I think they've only merged the parts that are straight generalizations. CMRA's for example are paramaterized by a type of step indices.

[Mario Carneiro]

I don't mind merging those generalizations, in general I think things are easier for people looking at one small piece of the system if we keep things similar

[Mario Carneiro]

I guess it's possibly also a simplification insofar as the exact nature of that indexing type almost never matters

[Michael Sammler]

I think it would be nice to port the generalized version since that would make it easier to support transfinite stepindexing in the future. For reference, this is the Iris MR: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/888

[Mario Carneiro]

There are a lot of versions of iris going around. I would like to avoid having the same decision paralysis as iris by just deferring to them regarding all of those "big MRs that have a paper written about them"

[Mario Carneiro]

i.e. we will follow suit when the MR is merged and not before

[Michael Sammler]

:+1: (For clarification, the MR I linked was merged already, but there are other MRs related to transfinite Iris that are not merged yet.)

[Markus de Medeiros]

I've added a handful of issues to the repo, all of which are mutually disjoint and should be good for new contributors :)