Add the (very unfinished) rpylean.

[Julian]

This can't be merged yet, as rpylean only supports the NDJSON export format as currently emitted by lean4export's main branch (not the arena_json_output one).

It also obviously fails some tests, as we know it's not correct yet :).

But perhaps putting it here will motivate us to keep going, lka existing already motivated me to get back to it a bit this week.

[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.