Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add New Rule Builder: Tactic Generator #70

Closed
wants to merge 37 commits into from
Closed

Add New Rule Builder: Tactic Generator #70

wants to merge 37 commits into from

Commits on Sep 12, 2023

  1. Finish a RuleTac and a RuleBuilder to run neural network under the ho… 

    …od, along with up/downstream parts
    @Peiyang-Song
    Peiyang-Song committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    35dd673 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2023

  1. Bump to LeanInfer 2.0.0, simplify additional installation steps

    @Peiyang-Song
    Peiyang-Song committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    5919da4 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2023

  1. Bump to LeanInfer v0.0.4

    @Peiyang-Song
    Peiyang-Song committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    03fd2aa View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2023

  1. Add script builder for neural

    @Peiyang-Song
    Peiyang-Song committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    8d1adba View commit details
    Browse the repository at this point in the history

  2. Bump to LeanInfer v0.0.7

    @Peiyang-Song
    Peiyang-Song committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    e34adc4 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2023

  1. Add Aesop-LeanInfer readme

    @Peiyang-Song
    Peiyang-Song authored Sep 23, 2023
    Configuration menu
    Copy the full SHA
    3bc8350 View commit details
    Browse the repository at this point in the history

  2. Separate Aesop-LeanInfer readme from original Aesop

    @Peiyang-Song
    Peiyang-Song authored Sep 23, 2023
    Configuration menu
    Copy the full SHA
    ad2b3e8 View commit details
    Browse the repository at this point in the history

  3. Create Aesop-README.md

    @Peiyang-Song
    Peiyang-Song authored Sep 23, 2023
    Configuration menu
    Copy the full SHA
    9d410b5 View commit details
    Browse the repository at this point in the history

  4. Add build check example

    @Peiyang-Song
    Peiyang-Song committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    2cdbed4 View commit details
    Browse the repository at this point in the history

Commits on Sep 25, 2023

  1. Link update

    @Peiyang-Song
    Peiyang-Song authored Sep 25, 2023
    Configuration menu
    Copy the full SHA
    1804f21 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2023

  1. Add exception handling and fix specific-tactic bug

    @Peiyang-Song
    Peiyang-Song committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    2671f5e View commit details
    Browse the repository at this point in the history

  2. Rename package

    @Peiyang-Song
    Peiyang-Song committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    abe4b7b View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Remove or suggested by the model: fake proofs

    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    2e9134f View commit details
    Browse the repository at this point in the history

  2. Detect when part of tactic is sorry or admit

    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    1ef6a4a View commit details
    Browse the repository at this point in the history

  3. Increase number of candidate sequences to 64

    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    100fcd3 View commit details
    Browse the repository at this point in the history

  4. Add reminder of LeanInfer cloud build not working

    @Peiyang-Song
    Peiyang-Song authored Sep 28, 2023
    Configuration menu
    Copy the full SHA
    de4d756 View commit details
    Browse the repository at this point in the history

  5. detect sorries

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    002ceca View commit details
    Browse the repository at this point in the history

  6. lake update

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    a86552e View commit details
    Browse the repository at this point in the history

  7. restore states

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    1abe960 View commit details
    Browse the repository at this point in the history

  8. bump to leanprover/lean4:v4.2.0-rc1

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    5ea54ad View commit details
    Browse the repository at this point in the history

  9. rollback to v4.0.0

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    5ddb1a3 View commit details
    Browse the repository at this point in the history

  10. Merge pull request #1 from Peiyang-Song/Kaiyu-LeanInfer-dev 

    Kaiyu lean infer dev
add detection for hidden sorry/admit
    @Peiyang-Song
    Peiyang-Song authored Sep 28, 2023
    Configuration menu
    Copy the full SHA
    874d274 View commit details
    Browse the repository at this point in the history

  11. Disable timeout

    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    a25763f View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/peiyang-LeanInfer-dev' into peiy… 

    …ang-LeanInfer-dev
    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    4dfb047 View commit details
    Browse the repository at this point in the history

  13. minor fix

    Kaiyu Yang committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    0dc1f4a View commit details
    Browse the repository at this point in the history

  14. Minor fix to get rid of PANIC

    @Peiyang-Song
    Peiyang-Song committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    4fb28bc View commit details
    Browse the repository at this point in the history

  15. Merge pull request #2 from Peiyang-Song/Kaiyu-LeanInfer-dev 

    minor fix
    @Peiyang-Song
    Peiyang-Song authored Sep 28, 2023
    Configuration menu
    Copy the full SHA
    3442b8e View commit details
    Browse the repository at this point in the history

  16. Merge pull request #3 from Peiyang-Song/peiyang-LeanInfer-dev 

    Peiyang lean infer dev
    @Peiyang-Song
    Peiyang-Song authored Sep 28, 2023
    Configuration menu
    Copy the full SHA
    6fce70e View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2023

  1. Merge branch 'peiyang-LeanInfer'

    Kaiyu Yang committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    73186b1 View commit details
    Browse the repository at this point in the history

  2. simplify

    Kaiyu Yang committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    ee63cbe View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2023

  1. use LLM-generated scores

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    f1977a4 View commit details
    Browse the repository at this point in the history

  2. use the tactic rule builder

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    7669ebc View commit details
    Browse the repository at this point in the history

  3. further simplify

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    744bae6 View commit details
    Browse the repository at this point in the history

  4. clean

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    76375b4 View commit details
    Browse the repository at this point in the history

  5. leanprover/lean4:v4.2.0-rc1

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    c238fd6 View commit details
    Browse the repository at this point in the history

  6. clean

    Kaiyu Yang committed Oct 7, 2023
    Configuration menu
    Copy the full SHA
    76de841 View commit details
    Browse the repository at this point in the history

  7. Merge pull request #4 from Peiyang-Song/refactor 

    Refactor
    Kaiyu Yang authored Oct 7, 2023
    Configuration menu
    Copy the full SHA
    4bc99ff View commit details
    Browse the repository at this point in the history