Add the (very unfinished) rpylean.

[Julian]

It still fails some quite basic tests but if you're ok with that being shown as-is (and it motivating us to keep going to get them passing) I think it's functionally ready to be added.

[nomeata]

I had a look at the build failure and pushed to master a fix to the flake file.

[Julian]

Ah thanks, I had just done the same :)

[Julian]

OK I think we now pass all the tests, even though there's still plenty missing:

⊙  uv run lka.py run                                                                                                                                                                                                                                                            julian@Airm
Skipping 10 checker(s) that weren't built: always-accept, always-decline, always-reject, lean-pr-10565, lean4lean, mini, nanoda, official-nightyl, official, parse-only
Running rpylean on tutorial/02_badDef... [rejected, 7 ms]
Running rpylean on tutorial/01_basicDef... [accepted, 6 ms]
Running rpylean on tutorial/09_levelComp1... [accepted, 6 ms]
Running rpylean on tutorial/04_dependentType... [accepted, 6 ms]
Running rpylean on tutorial/10_levelComp2... [accepted, 6 ms]
Running rpylean on tutorial/13_tut06_bad01... [rejected, 6 ms]
Running rpylean on tutorial/11_levelComp3... [accepted, 6 ms]
Running rpylean on tutorial/14_levelComp4... [accepted, 6 ms]
Running rpylean on tutorial/15_levelComp5... [accepted, 6 ms]
Running rpylean on tutorial/03_arrowType... [accepted, 6 ms]
Running rpylean on tutorial/18_inferVar... [accepted, 7 ms]
Running rpylean on tutorial/16_imax1... [accepted, 6 ms]
Running rpylean on tutorial/05_simpleLambda... [accepted, 6 ms]
Running rpylean on tutorial/17_imax2... [accepted, 6 ms]
Running rpylean on tutorial/08_nonTypeType... [rejected, 6 ms]
Running rpylean on tutorial/19_defEqLambda... [accepted, 7 ms]
Running rpylean on tutorial/06_betaReduction... [accepted, 6 ms]
Running rpylean on tutorial/07_betaReduction2... [accepted, 6 ms]
Running rpylean on tutorial/12_levelParams... [accepted, 6 ms]
Running rpylean on tutorial/20_peano1... [accepted, 6 ms]
Running rpylean on tutorial/21_peano2... [accepted, 6 ms]
Running rpylean on tutorial/22_peano3... [accepted, 6 ms]

============================================================
Summary:
============================================================
  accepted: 19
  rejected: 3

which probably means it's time to try and help write a few more tests as soon as I figure out what we're missing next.

[nomeata]

I think the next step in the tutorial is inductive types, right? Or do you mean more tests for the fragment without inductive types first?

[Julian]

Depending on what precisely you think the sequence should be -- for example, I know that rpylean does not do anything at all with mutual definitions and theorems (we just check the first one and ignore all the rest of them). I would think that should go later but the way the new export format is laid out (which overall is clearly a big improvement as I got to delete lots of code) one needs to confront mutual defs, theorems and inductives immediately in the parser at least, because everything is represented as an array, including non-mutual versions of things.

But yeah I suspect some inductive type tests would be great to have next!

[nomeata]

There are no mutual definitions! (As long as you only care about the safe subset and decline any unsafe definitions, which I think is totally fine for a checker)

The parser format is a but unfortunate in that respect, see discussion at leanprover/lean4export#14 (review)

If you only care about safe declarations then it's ok to flatten these arrays during parsing.

[nomeata]

BTW, on this branch I have been busy writing more and more tests (inductives, projections):
https://github.com/leanprover/lean-kernel-arena/commits/joachim/tutorial-inductives/

That branch is using the 3.1.0 export format. Feel free to include that branch in your work here, and let me know if you found these tests useful or if you found something to be missing.

[Julian]

Going to take this out of draft now that 3.1.0 is on master, not because rpylean is done :) but I think at least now it's runnable here -- the tests you're adding are super helpful! I'll try to leave further comments on anything specific in them when I get more time to actually try to get them to pass, but yeah thanks for all of the efforts here it's making it a lot easier to write one!

[nomeata]

Does that mean you want this to be merged as is? Or sit here?

(Maybe update the PR description accordingly)

[Julian]

Updated the description. What I meant was I think it can be merged now and then I can come back with more PRs to update its version later if you're happy to have it shown as failing a portion of the tests, I know there are other "not totally real" checkers shown (like always-reject) so at least we pass some :)