jonaprieto / online-atps Goto Github PK

We need to have available the option to request ATPs synchronize or not.

I suggest only test the latest minor version of each major version.

Stop the verification process if some ATP finds a positive answer, that is, the problem results to be a theorem.

The user gives a name of atp like "online-vampire" and the method must return the corresponding data type SystemATP.

getByNameSystemATP :: String -> IO SystemATP

> getByNameSystemATP "online-e"
SystemATP
  { sysKey         = "online-e"
  , sysName        = "E---2.0"
  , sysVersion     = "2.0"
  , sysTimeLimit   = "60"
  , sysTransform   = "none"
  , sysFormat      = "tptp:raw"
  , sysCommand     = "eprover -s --cpu-limit=%d %s"
  , sysApplication = "Prover and model finder, for FOF CNF"
  }

After process arguments from command line map toLower in each optATP name.

Using GHC 7.6.3 I got the following error:

$ cabal install
...
src/OnlineATPs/Consult.hs:165:39: Not in scope: `<$>'

Blocking asr/apia#68.

We want to use onlineatps as an executable. At the beginning, the prototype should accepts a filepath, the atp name and optionally a version for the atp.

$ onlineatps ./basic-1.fof --atp=online-e

The name of atp should not have the prefix "online":

$ onlineatps ./basic-1.fof --atp=e

After read .onlineatps , fill the record ATP with the keys of ATPs that it found in that file.

λ ~/onlineatps/src/ master* touch .onlineatps
λ ~/onlineatps/src/ master* runghc Main.hs ~/onlineatps/examples/basic.tptp --atp=e
Main.hs: UnexpectedEvent {_received = Just EventStreamEnd, _expected = Just EventDocumentStart}

If the file doesn´t exist, print another message.

$ onlineatps basic.tptp --atp=vampire
onlineatps: basic.tptp: openFile: does not exist (No such file or directory)

Using GHC 8.4.2 I get the following error:

$ cabal install
Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] trying: online-atps-0.1.1 (user goal)
[__1] next goal: base (dependency of online-atps)
[__1] rejecting: base-4.11.1.0/installed-4.1... (conflict: online-atps =>
base>=4.6.0.1 && <4.11)
[__1] rejecting: base-4.11.0.0, base-4.10.1.0, base-4.10.0.0, base-4.9.1.0,
base-4.9.0.0, base-4.8.2.0, base-4.8.1.0, base-4.8.0.0, base-4.7.0.2,
base-4.7.0.1, base-4.7.0.0, base-4.6.0.1, base-4.6.0.0, base-4.5.1.0,
base-4.5.0.0, base-4.4.1.0, base-4.4.0.0, base-4.3.1.0, base-4.3.0.0,
base-4.2.0.2, base-4.2.0.1, base-4.2.0.0, base-4.1.0.0, base-4.0.0.0,
base-3.0.3.2, base-3.0.3.1 (constraint from non-upgradeable package requires
installed instance)
[__1] fail (backjumping, conflict set: base, online-atps)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: base, online-atps

We want to catch the first positive answer given by atp from a list of atps. This should be done asyncronize.

The common user may not know the correct spelling of the atp.
The method can have the type:

suggestSystemATPs :: String -> [SystemATPs]

> suggestSystemATP "ampire"
["online-vampire", "online-vampire2", "online-fampire"]

The method must resolve the list even if the string given by the user doesn't have the prefix "online-".

send all output to text files in a directory

Use Doc type for messages

Incorporate this feature to the code base. Most of the job is already done.

partial implementation:
https://gist.github.com/jonaprieto/19d412c6025c4a073716690e36f246e6

yaml:
https://gist.github.com/jonaprieto/d9d8211b63291660dc0883f8e93941f0

Attacks the problem against the all ATP available. The --fof flag should be useful.

It seems that the dependency on the cpphs library is unnecessary.

Nowadays, a final user can not modify the settings to send the form data to SystemOnTPTP.
We want the user can be free and modify whatever he need.

defaultSystemOnTPTP = SystemOnTPTP
  {
    optAutoMode              = "-cE"
  , optAutoModeSystemsLimit  = "3"
  , optAutoModeTimeLimit     = "300"
  , optCompleteness          = False
  , optCorrectness           = False
  , optCPUPassword           = ""
  , optFORMULAEProblem       = ""
  , optFormulaURL            = ""
  , optIDV                   = False
  , optNoHTML                = "1"
  , optProblemSource         = "FORMULAE" --"TPTP"
  , optQuietFlag             = "-q01" --q2
  , optReportFlag            = "-q0"
  , optSoundness             = False
  , optSubmitButton          = "RunSelectedSystems"
  , optSystemInfo            = False
  , optSystemOnTSTP          = False
  , optSystems               = [ defaultOnlineATP ]
  , optTPTPProblem           = "" --AGT001+1"
  , optTSTPData              = False
  , optUPLOADProblem         = ""
  , optX2TPTP                = False
}

We are talking that the user can choice the output mode, send the cpupassword, turnoff the flag tstp as many others.

By default, onlineatps send a POST per each ATP that user uses. So, we should have the chance that the user use all ATPs at once. It could slow down the waiting time certainly.

Add a new option --check-theorem. This option is especially thinking for Apia program. Actually, Apia only required if the input file is a theorem or not. But other people may or may not interest only on this.

Given the defaults options in Defaults.hs.
A response gives something like:

"% SZS start RequiredInformation\n% Congratulations - you have become a registered power user
 of SystemOnTPTP, at IP address 181.137.110.96.\n% Please consider donating to the TPTP project
- see www.tptp.org for details.\n% When you donate this message will disappear.\n% If you do not
 donate a random delay might be added to your processing time.\n% SZS end
RequiredInformation\nE---2.0   system information being retrieved\nE---2.0's non-default 
parameters being retrieved\n    -t none\n    -f tptp:raw\n    -x eprover -s --cpu-limit=%d %s\nE--
-2.0's AGT001+1 does not need preparation\nE---2.0   being executed on AGT001+1 using 
/home/tptp/Systems/E---2.0/eprover -s --cpu-limit=60 '/home/tptp/TPTP-
v6.4.0/Problems/AGT/AGT001+1.p'\nRESULT: AGT001+1 - E---2.0 says Theorem - CPU = 0.01 WC = 0.03 \nOUTPUT: AGT001+1 - E---2.0 says Assurance - CPU = 0.01 WC = 0.03 \n"

We need a method to check if the response above is Ok or the prover couldn't prove the conjecture. The output suggest check with isInfixOf "ATP says Theorem" in the same line after "RESULT:" . The name of this method should be the same as Apia use for local atps.

Nowadays, I can use getResponseSystemOnTPTP with any problem from the TPTP library using a descriptor of the problem. The user must have the chance to use his own tptp problem.
The method should have the type:

getResponseWithFileTPTP :: SystemOnTPTP -> FilePath -> String

The above method should modify the variable of type SystemOnTPTP with optProblemSource, and , optUPLOADProblem. And the use the standard method getResponseSystemOnTPTP .

getResponseWithFileTPTP :: SystemOnTPTP -> FilePath -> String
getResponseWithFileTPTP spec file = getResponseSystemOnTPTP $ spec 
     {  optProblemSource ="FileUpload" ,  optUPLOADProblem=file }

Using GHC 7.8.4 I got the following error:

$ cabal install
...
src/OnlineATPs/Consult.hs:161:39: Not in scope: ‘<$>’
cabal: Leaving directory '.'
Failed to install onlineatps-0.1.0
cabal: Error: some packages failed to install:

Blocking asr/apia#68.

Nowadays, I filter the ATP with deal FOF. But also we may want to use other logics.
I need a flag for FOF.

$ onlineatps --list-atps --fof

Using GHC 7.10.3 I got the following error:

$ cabal install
...
src/OnlineATPs/Consult.hs:19:18:
    Could not find module ‘Control.Monad.IO.Class’
    It is a member of the hidden package ‘transformers-0.4.2.0@trans_GZTjP9K5WFq01xC9BAGQpF’.
    Perhaps you need to add ‘transformers’ to the build-depends in your .cabal file.
    Use -v to see a list of the files searched for.

Today I had a similar issue with Apia. I fixed the problem in asr/apia@dc89203.

Running online-atps --list-atps, I got

[Vampire]
  application: For TF0 FOF CNF
  key: online-vampire
  version: 4.1


[Vampire]
  application: For TF0_CSA TF0_SAT FOF_CSA FOF_SAT CNF_SAT
  key: online-vampire
  version: SAT-4.1

but using the --version-atp option I got:

$ online-atps --version-atp=vampire
Vampire---SAT-4.1

Why the version 4.1 of Vampire isn't reported?