New tasks: PORTING.md

Stream: iris-lean

[Markus de Medeiros]

I read through the Iris source code and made a list of tasks corresponding to each Rocq file in PORTING.md. This is a great place to look for new things to work on, or to check up on if your favorite feature has been ported yet.

I will still make GitHub issues for the highest priority and most accessible tasks!

[Markus de Medeiros]

@Michael Sammler @Zongyuan Liu I left the proofmode and big op sections alone, if you want to summarize the status of things there feel free

[Shreyas Srinivas]

I have a numbers PR pending for a while

[Shreyas Srinivas]

I have some mid February deadlines. I will get to it after that

[Markus de Medeiros]

Don't worry about it, I'll just finish it this afternoon :)

[Shreyas Srinivas]

It's this one : https://github.com/leanprover-community/iris-lean/pull/67

[Shreyas Srinivas]

Anytime you see

simp_all
rw [...]

That's my copium for not having simp_rw at hand

[Zongyuan Liu]

The wiki page is open now. Do we want to move it?

[Markus de Medeiros]

I have no opinions on this, feel free to do it if you think it's a good idea

[Bas Spitters]

Good idea @Markus de Medeiros I have just ported some benchmarks from rocq stdlib to math-comp. It works very well. Some main challenges are getting the proper imports.

[Michael Sammler]

Thanks for creating the PORTING document! I thought briefly about moving it to the wiki, but maybe it is better to leave it in the main repo for now, since this way people can directly mark things as done when they create a PR.
I filled in the missing porting information about the proof mode.

[Alex Bai]

In PORTING.md, it claims a lot of stuff is generalized MonoNumbers.lean. Is that file anywhere?

[Markus de Medeiros]

"generalize" is future tense. Since numbers.v generalizes both of the underlying CMRA's, I think mono_nat.v and mono_Z.v should also generalize to one file, or at least we should try to do that.