Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / openai/lean-gym issues and pull requests

#32 - Having trouble init_search miniF2F proofs

Issue - State: closed - Opened by Some-random over 1 year ago - 2 comments

#31 - Segmentation fault error

Issue - State: open - Opened by ayush1801 about 2 years ago

#29 - Make scripts fail fast

Pull Request - State: open - Opened by fzyzcjy about 2 years ago

#28 - fail to setup

Issue - State: open - Opened by yxliu0903 over 2 years ago

#27 - How to search a customed theorem with lean-gym?

Issue - State: open - Opened by liebenxj over 2 years ago

#26 - How to integrate lean-gym with python?

Issue - State: open - Opened by venom12138 over 2 years ago - 1 comment

#25 - Accessing the Global Environment

Issue - State: closed - Opened by yangky11 over 2 years ago

#24 - Decreasing Performance

Issue - State: open - Opened by todbeibrot over 2 years ago - 3 comments

#23 - Question about PACT tactic dataset

Issue - State: closed - Opened by wiio12 almost 3 years ago - 8 comments

#22 - Return error when parse failed without exiting.

Pull Request - State: closed - Opened by wiio12 almost 3 years ago - 3 comments

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

Pull Request - State: closed - Opened by spolu almost 3 years ago - 1 comment

#20 - Various fixes and bump mathlib/minif2f

Pull Request - State: closed - Opened by spolu almost 3 years ago

#19 - Remove gptf dependency

Pull Request - State: closed - Opened by spolu about 3 years ago - 2 comments

#18 - Shrink

Pull Request - State: closed - Opened by dselsam about 3 years ago - 4 comments

#17 - Monad

Pull Request - State: closed - Opened by Scikud over 3 years ago - 12 comments

#16 - wip, added tactic to narrow state, tactic to register new lemma

Pull Request - State: closed - Opened by Scikud over 3 years ago

#15 - chore(bump mathlib)

Pull Request - State: closed - Opened by spolu over 3 years ago

#14 - strengthen `validate_proof`

Pull Request - State: closed - Opened by jesse-michael-han over 3 years ago - 2 comments

#13 - Bump miniF2F to v1

Pull Request - State: closed - Opened by spolu over 3 years ago - 1 comment

#12 - bump miniF2F

Pull Request - State: closed - Opened by DyeKuu over 3 years ago

#11 - bump miniF2F

Pull Request - State: closed - Opened by DyeKuu over 3 years ago - 1 comment

#10 - bump mathlib

Pull Request - State: closed - Opened by spolu over 3 years ago - 1 comment

#9 - [repl] tentatively fix dangling metavariable issue

Pull Request - State: closed - Opened by jesse-michael-han over 3 years ago - 1 comment

#8 - In case of error, capture if there is no goals and succeed instead

Pull Request - State: closed - Opened by spolu over 3 years ago - 1 comment

#7 - Proof checks should happen after every tactic

Issue - State: open - Opened by jasonrute over 3 years ago - 7 comments

#6 - Check against the use of `undefined`

Pull Request - State: closed - Opened by spolu over 3 years ago - 5 comments

#5 - Add checks against `sorry` and proof term type mismath

Pull Request - State: closed - Opened by spolu over 3 years ago

#4 - [repl] loop forever using `iterate_until`

Pull Request - State: closed - Opened by jesse-michael-han over 3 years ago - 1 comment

#3 - Support for `init_search` and `clear_search`

Pull Request - State: closed - Opened by spolu over 3 years ago

#2 - [util/tactic] use `expr.reduce_let` in `tactic_hash`

Pull Request - State: closed - Opened by jesse-michael-han over 3 years ago - 1 comment

#1 - [repl] cleanup using state_t instead of explicit state-passing

Pull Request - State: closed - Opened by jesse-michael-han over 3 years ago - 1 comment