QPF ?

Stream: general

[Jacques Carette]

@Jeremy Avigad @Mario Carneiro @Simon Hudon I am extremely interested in your work on QPF - but it seems that progress has stalled?

(Full disclosure: I think that Species is an even better way of doing this, but I'd definitely take QPF over mere algebraic types. And these are, of course, intimately related, with the pros/cons of each still to be figured out.)

[Patrick Massot]

There are also mathlib PRs on this topic.

[Simon Hudon]

Still in progress. I'm arranging a compiler for simple datatypes and I have extension for indexed datatypes. Both are PRs and work in progress

[Jacques Carette]

I found #3332 and #3638 - are there more?

[Jacques Carette]

Oh, and I see that it links to #3317, which was merged.

[Simon Hudon]

And #3748 which still needs to be cleaned up. It's the compiler

[Simon Hudon]

I've been breaking up the project into multiple PRs to make it easier to review. And if you have time to review PRs, it might be closer to your interest than to those of most contributors here

[Jacques Carette]

Thanks - lots of reading material.

[Simon Hudon]

Don't hesitate to reach out if you have any questions

[Jacques Carette]

I don't know about my competence wrt reviewing though. I don't know Lean [though I'm learning just enough to read it.] But if asking lots of questions about why you did X or Y counts as a review, I can do some of that.

[Jacques Carette]

Is there a document that outlines the Lean community conventions on doing reviews?

[Jacques Carette]

And I take it that the place to ask questions is indeed here?

[Johan Commelin]

Jacques Carette said:

Is there a document that outlines the Lean community conventions on doing reviews?

There are our code styleguides, but that's about it. We're pretty laid back about reviews. All comments are welcome. Maintainers have the final decision.

[Simon Hudon]

But if asking lots of questions about why you did X or Y counts as a review, I can do some of that.

It's usually very useful feedback. It helps me see what is unclear from an outside observer.

Is there a document that outlines the Lean community conventions on doing reviews?

https://leanprover-community.github.io/contribute/index.html is the closest we have I think

[Johan Commelin]

See the links at the top of https://leanprover-community.github.io/contribute/index.html for the guidelines

[Simon Hudon]

Also, there's a stream here #PR reviews that we use for discussing specific PRs

[Jacques Carette]

Oh no, another stream to follow. Sigh.

[Patrick Massot]

I think you can discuss QPF with Simon as much as you want in this topic, you don't need another stream.