search

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

Error when using the `--with-e` option #82

Closed asr closed 7 years ago

asr commented 7 years ago

For example, the command

$ apia --atp=metis --with-metis=xxx Foo.agda

correctly generates the error

apia: the ‘xxx’ command associated with Metis does not exist

but replacing metis by e the generated error is

$ apia --atp=e --with-e=xxx Foo.agda
apia: xxx: readCreateProcess: runInteractiveProcess: exec: does not exist (No such file or directory)
asr commented 7 years ago

@jonaprieto, can you reproduce this issue?

jonaprieto commented 7 years ago

Yes.

asr commented 7 years ago

Thanks!