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

Fix-ups for "significant proof checking refactoring" #48

Merged
merged 21 commits into from
Nov 26, 2024
Merged

Fix-ups for "significant proof checking refactoring" #48

merged 21 commits into from
Nov 26, 2024

Commits on Nov 15, 2024

  1. Refactor SessionState & highlight vulnerabilities

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    f70deac View commit details
    Browse the repository at this point in the history

  2. Restructure theorem rankers, add comments

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    5b5abb1 View commit details
    Browse the repository at this point in the history

  3. Remove redundant null-checks for theorem proof

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    e64f491 View commit details
    Browse the repository at this point in the history

  4. Make code style of parsedTypes.ts consistent

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    1d158bc View commit details
    Browse the repository at this point in the history

  5. Format code

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    66d0d43 View commit details
    Browse the repository at this point in the history

  6. Use ProofGoal instead of Goal<PpString>

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    16831af View commit details
    Browse the repository at this point in the history

  7. Implement getFirstGoalOrThrow wrapper properly

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    ca16531 View commit details
    Browse the repository at this point in the history

  8. Improve code style of coq-lsp tests

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    34d48f3 View commit details
    Browse the repository at this point in the history

  9. Introduce withTextDocument wrapper

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    8b3a621 View commit details
    Browse the repository at this point in the history

  10. Fix imm submodule commit

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    8abe2eb View commit details
    Browse the repository at this point in the history

  11. Introduce with-coq-lsp wrappers, dispose client correctly

    @GlebSolovev
    GlebSolovev committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    ea7805b View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2024

  1. Fix SessionState bugs, improve its code style

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    b0c20a4 View commit details
    Browse the repository at this point in the history

  2. Fix coq-lsp usage in legacy benchmarks, refactor args

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    da02a28 View commit details
    Browse the repository at this point in the history

  3. Prevent legacy benchmarks from creating empty report on start

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    1cc6ffd View commit details
    Browse the repository at this point in the history

  4. Fix coq-lsp usage at parsing stage of benchmarks

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    649402d View commit details
    Browse the repository at this point in the history

  5. Document CoqLspClient invariants

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    729153b View commit details
    Browse the repository at this point in the history

  6. Improve CoqProofChecker code style

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    09f914a View commit details
    Browse the repository at this point in the history

  7. Fix bugs in internal signatures of benchmarks 

    Caused by recent refactoring
    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    a129ca9 View commit details
    Browse the repository at this point in the history

  8. Move abort utils into core

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    78dd974 View commit details
    Browse the repository at this point in the history

  9. Structure extension directory

    @GlebSolovev
    GlebSolovev committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    7c3d5d6 View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2024

  1. Support abort signal set-up in coq-lsp client wrappers 

    Pass abort signal into coq-lsp client correctly in benchmarks
    @GlebSolovev
    GlebSolovev committed Nov 17, 2024
    Configuration menu
    Copy the full SHA
    3a8ffc2 View commit details
    Browse the repository at this point in the history