Kaiyu Yang comments

Results 70 comments of


                                            Kaiyu Yang

DojoInitError: Cannot find the *.ast.json file for Theorem

I'm not sure what's happening for the `CommSemiring.toSemiring_injective` example and will take a more detailed look when I have a chance (likely a few weeks later).

Error fetching results: CalledProcessError(1, 'lake env lean --threads 16 --run ExtractData.lean')

Do you have a minimal script for reproducing the error using the latest version of LeanDojo (no LeanUniverse)?

Error fetching results: CalledProcessError(1, 'lake env lean --threads 16 --run ExtractData.lean')

> It seems like it's because `Std.HashMap.find?` has been deprecated in Lean. and "ExtactData.lean" include such a fuction. open it and listen to Lean InfoView, changing the "find" to "get"...

RayTaskError when tracing the latest mathlib4

The error seems to be caused by recent Lean/mathlib upgrades. I'll let you know after it's fixed.

RayTaskError when tracing the latest mathlib4

I just fixed it in the `main` branch (please try) and will release a new version after running unit tests.

lean_dojo_repl not working

will take a look when I have a chance (hopefully next week)

lean_dojo_repl not working

I believe this is related to https://github.com/lean-dojo/LeanDojo/issues/211 and will not be solved anytime soon.

How to parallelize when testing?

Glad to hear that you've managed to reproduce the experiment! Unfortunately, this project was five years ago, and I'm no longer able to actively maintain it.

Fix(typing): mypy errors

Thanks! I'll be able to take a look next week.

Fix(typing): mypy errors

Sorry I've been swamped recently but will take a look when I get a chance!