Wrong behaviour when using an `.apia` file

[asr]

Given the following files

$ cat ~/.apia 
atp: [e]

$ cat NoTheorem.agda
module NoTheorem where

postulate
  D   : Set
  _≡_ : D → D → Set
  a b : D

postulate foo : a ≡ b
{-# ATP prove foo #-}

I'm getting the output

apia --atp=vampire NoTheorem.agda
Proving the conjecture in /tmp/NoTheorem/8-foo.fof
Vampire 0.6 (revision 903) *did not* prove the conjecture
E 1.9 Sourenee *did not* prove the conjecture
apia: the ATP(s) did not prove the conjecture in /tmp/NoTheorem/8-foo.fof

@jonaprieto why Apia is calling E if I only used the --atp=vampire option?

[jonaprieto]

I think that it is happening because of the line 134 in Options.hs and because the defaults are built first than option values from the command line. Then, it is appending.

atpOpt name opts = Right opts { optATP = nub $ optATP opts ++ [name] }

[asr]

A default option should be rewriting by an explicit command line option.

[asr]

Thanks for fixing the issue. I'll add a test case later.

[asr]

@jonaprieto I assigned both this issue.

[asr]

TODO: Test case.

[asr]

After the fix I'm getting

$ make errors
...
 :test/fail/errors/errors.test:37: [Failed]

Expected stdout: ""
Got stdout:      "Proving the conjecture in /tmp/test/fail/errors/NoTheorem/17-foo.fof\nE 1.9 Sourenee *did not* prove the conjecture\n"
Expected stderr: "apia: at least you need to specify one ATP\n"
Got stderr:      "apia: the ATP(s) did not prove the conjecture in /tmp/test/fail/errors/NoTheorem/17-foo.fof\n"

I'll fix the test-suite.