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.

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

Prove Call/Result Structure #1

Open
traeger opened this issue Jul 27, 2019 · 0 comments
Open

Prove Call/Result Structure #1

traeger opened this issue Jul 27, 2019 · 0 comments
Labels
enhancement New feature or request

Comments

@traeger
Copy link
Collaborator

traeger commented Jul 27, 2019

Rewrite our current Problem/ProblemVariant prover call from:

  • ProveProcess deriving Process
  • ProveScheduler deriving ThreadedProcessExecuter

to

  • a new Prover class-
    • defining how a prover (e.g. Leo) is called
    • proving a method prove(problem, timeout, **prover_call_kwargs) to get a related prover call with optional additional parameter to start call the underlaying prover
  • a new ProverCall class:
    • managing its own szsStatus, result parsing, stdout, stderr, timer
    • derivable for each supported TheormProver and TestSetup which is implemented:
    • using concurrent.Process, s.t. it supports termination and concurrent execution using run(), timer?
  • the ProverCall can be used directly in the main-thread using a wait() pattern
  • or used in a multitheaded environment s.t. a ProveScheduler
  • ProblemVariant:
    • ProverCall is introduced as member
    • process, szsStatus, and such is removed

This should provide a good theorem-prover-call abstraction which may be used in any serial, concurrent or parallel environment.

Reminder:

  • the package structure needs be reworked
    • concurrent -> utils.concurrent
    • new ProverCall and its derivations -> prover
@traeger traeger added the enhancement New feature or request label Jul 27, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant