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

Run corpus of TLA+ syntax tests in simple pass/fail manner #159

Merged
merged 28 commits into from
Nov 4, 2024
Merged

Run corpus of TLA+ syntax tests in simple pass/fail manner #159

merged 28 commits into from
Nov 4, 2024

Commits on Oct 15, 2024

  1. Basic round-trip parse unit test 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    6de51d5 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. Syntax corpus files copied by dune build 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    52c8a4a View commit details
    Browse the repository at this point in the history

  2. Basic parsing of test file format 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    76b0b24 View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2024

  1. More structured parsing of all test files 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    88ff8ed View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2024

  1. Show syntax_test datastructure using ppx_deriving 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    5fc1074 View commit details
    Browse the repository at this point in the history

  2. Parse test attributes 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    8789325 View commit details
    Browse the repository at this point in the history

  3. Split corpus file parsing logic into separate file 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    e44b1c2 View commit details
    Browse the repository at this point in the history

  4. Added documentation to syntax corpus file parser 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    cb43c6a View commit details
    Browse the repository at this point in the history

  5. Parse expected test output using sexplib 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    d6a7a84 View commit details
    Browse the repository at this point in the history

  6. Send corpus tests into parser 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    e0ea1c4 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2024

  1. Update test corpus, print failures 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    5be306b View commit details
    Browse the repository at this point in the history

  2. Accumulate test run summary 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    3b47b05 View commit details
    Browse the repository at this point in the history

  3. Isolate failing syntax test cases 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    5a9a76d View commit details
    Browse the repository at this point in the history

  4. Encode failing tests; assert on test failure 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    a80c1e4 View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2024

  1. Added documentation to syntax corpus test file 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    4476a32 View commit details
    Browse the repository at this point in the history

  2. Simplified test control logic 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    7af9882 View commit details
    Browse the repository at this point in the history

  3. Accumulate test summaries in place 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    0bde78d View commit details
    Browse the repository at this point in the history

  4. Use List.partition for parsing test header 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    93c084a View commit details
    Browse the repository at this point in the history

  5. Add test deps to dune-project 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    ee66bed View commit details
    Browse the repository at this point in the history

  6. Disambiguated parser tests filename 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    a8b5f6a View commit details
    Browse the repository at this point in the history

  7. Formalized test filter predicate 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    9a8d99d View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. Added syntax tests for \forall and \exists 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    894bd9c View commit details
    Browse the repository at this point in the history

  2. Tag test failures with github issues 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    7fd6b9b View commit details
    Browse the repository at this point in the history

  3. Added failing test for parameterized refinement in subscript 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    7ab6f54 View commit details
    Browse the repository at this point in the history

  4. Added failing tests for implicit proof names 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    1da7b5b View commit details
    Browse the repository at this point in the history

  5. Added test for proof level changes terminating jlists 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    0cc1d87 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. Added failing parse tests from SANY 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    86a046e View commit details
    Browse the repository at this point in the history

Commits on Oct 31, 2024

  1. Added syntax tests for tuples 

    Signed-off-by: Andrew Helwer <[email protected]>
    @ahelwer
    ahelwer committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    8a9533b View commit details
    Browse the repository at this point in the history