search

openai / lean-gym

Apache License 2.0
167 stars 30 forks source link

Do not trace with run_tac but do trace otherwise + fix #21

Closed spolu closed 2 years ago

spolu commented 2 years ago

cc @dselsam

spolu commented 2 years ago

(we need to keep the error trace for the top-level run_tactic'' calls to get back fatal errors)