Andrew Wells

In my experience the "Unable to sample any valid states for goal tree" usually happens when I set my transform incorrectly for grasping an object. So I have the gripper...

Sorry for my poor python code. Any suggestions to make it more idiomatic are appreciated.

When working on this, I ran into an issue where the tactics seem to be duplicated. For example: `.lake/build/bin/repl < test/all_tactics.in` Output: ``` {"tactics": [{"tactic": "have t := 37", "proofState":...

Dug into this a bit more. Adding `let tactics := tactics.take (tactics.length / 2)` to `REPL/Main.lean` gives close to the expected output. Unfortunately, the proof states for the repeated tactics...

I played around a bit and it seems applying this patch to Lean would be sufficient to restore the previous behavior: In `/src/Lean/Elab/Frontend.lean` ``` - let st ← IO.processCommandsIncrementally inputCtx...

In all the examples I've looked at `trees` will be empty with the above code. I tried keeping `trees := ...` unchanged and adding a deduplication step based on the...

I made some more changes to the REPL and have https://github.com/andrewmw94/lean4repl/commit/52b0c28cc5f4a1d4387a5f1b1c82dd4e0cd47e0f which seems to mostly work except when two commands have the same start and end locations (as in the...

Looks like that works (with a small change to the REPL). Thanks!

I'll update this PR once https://github.com/leanprover/lean4/pull/5763 is in nightly. I ran the tests locally with 4.12 + the patch above, and the only weird thing is `Expected output file test/H20231214.expected.out...