Manage the command line options of Apia with the ".apia" files.

[jonaprieto]

This new feature helps to avoid writing in your command line every single value option that you often use or you probably gonna use the next n times.

For instance, if you use metis as your favorite ATP, consider add it to the .apia file:

# ~/.apia
atp: ["metis"]

Now, try it! all the possible configuration options are available. Check apia --help.

[asr]

I got the following error:

$ make install-bin
$ make agda_apia_changed
...
shelltest --color --precise \
                  test/succeed/non-conjectures/non-conjectures.test
:test/succeed/non-conjectures/non-conjectures.test:1: [Failed]
...
:test/succeed/non-conjectures/non-conjectures.test:5: [Failed]
...
         Test Cases  Total      
 Passed  7           7          
 Failed  2           2          
 Total   9           9          
make[1]: *** [non_conjectures] Error 1

[asr]

The files in src/data shouldn't be hidden files.

[asr]

Please add lower and upper bounds for the library dependencies in apia.cabal.

[asr]

How can a user knows about the new functionality implemented in this PR?

[jonaprieto]

Just pending a new section in the README about .apia files.

[asr]

Note that your PR didn't pass the CI test.

[asr]

I run fix-whitespace and hlint before creating a commit. See the instructions in the new HACKING.md file.

[asr]

Running make hlint I got the following problems:

src/Apia/Defaults.hs:344:16: Suggestion: Redundant $
Found:
  doesFileExist $ dotapia
Why not:
  doesFileExist dotapia

src/Apia/Defaults.hs:345:3: Warning: Use when
Found:
  if not ishomeapia then
    do dotapiatemplate <- getDataFileName "apia_template.yml"
       copyFile dotapiatemplate dotapia
    else return ()
Why not:
  Control.Monad.when (not ishomeapia) $
    do dotapiatemplate <- getDataFileName "apia_template.yml"
       copyFile dotapiatemplate dotapia

2 hints
make: *** [hlint] Error 1

[asr]

I just added the HLint test to Travis.

[jonaprieto]

I got this:

hlint --color=never \
              --cpp-file=dist/build/autogen/cabal_macros.h \
              --cpp-include=src/Apia/ \
              src/
src/Apia/Translation.hs:85:8: Error: Parse error: role
Found:
    toAFor ∷ TPTPRole → QName → Definition → T AF
  > toAFor role qName def = do
      let ty ∷ Type
          ty = defType def

src/Apia/TPTP/Files.hs:124:24: Error: Parse error: role
Found:
    agdaOriginalTerm ∷ QName → TPTPRole → Text
  > agdaOriginalTerm qName role =
      "% The Agda term was:\n"
      +++ "% Name: " +++ (T.pack . prettyShow . qnameToConcrete) qName +++ "\n"

2 hints
Makefile:469: recipe for target 'hlint' failed

I don't know what is wrong.

[asr]

I don't know what is wrong.

You are using an old version of HLint (see the Makefile for the required version).

[asr]

I run fix-whitespace and hlint before creating a commit

I also added the fix-whitespace test to Travis.

[asr]

Which is the function of the src/data/apia.yml file? That is, why is it necessary both .yml files?

[jonaprieto]

With apia.yml we set the global default options. With apia_template.yml, we set the user default options.

[asr]

I see. Why not to use the same file + the difference between both files?

[asr]

Create a different PR for commits https://github.com/asr/apia/pull/34/commits/ec38aa1ec7e8b6c07ba9fc21c90873560694fb5d and https://github.com/asr/apia/pull/34/commits/b43eb7e5806a1182f65f46d03b90d42b9f5f6033 please.

[jonaprieto]

The difference is basically the comments in the YAML, thinking in the final user. So, Do you want to change it? Use one file is ok for me.

[asr]

Please use one file and append the comments for the final user.

[asr]

Thinking again about the .apia file, this file shouldn't be installed by default. If the user run apia without installing this file and without using the --atp option, apia should generate error.

"At least you need to specified one ATP"

[asr]

FYI, I added the following tests to Travis:

  - make generated_all
  - make non_conjectures
  - make errors
  - make type_check_notes
  - make ATPs="e" prove_notes

[jonaprieto]

With last test you added to Travis I'll fail with .apia feature unless you add to Travis the ATP by default.

λ ~/apia/ master* make generated_all
make generated_fol_theorems
make[1]: Entering directory '/home/jonaprieto/apia'
rm -r -f /tmp/apia
make generated_fol_theorems_aux
make[2]: Entering directory '/home/jonaprieto/apia'
Comparing test/succeed/fol-theorems/Agda/InternalTerms/DefTerm1.agda
apia: At least you need to specify one valid ATP
Makefile:95: recipe for target 'test/succeed/fol-theorems/Agda/InternalTerms/DefTerm1.generated_fol_theorems' failed
make[2]: *** [test/succeed/fol-theorems/Agda/InternalTerms/DefTerm1.generated_fol_theorems] Error 1
make[2]: Leaving directory '/home/jonaprieto/apia

Then, I suggest that after install Apia, in .travis.yml add something like echo "atp: [\"e\"]" > ~/.apia. I got this error because you had E as a default ATP, and now with my last modification. There is no default ATP.

[asr]

Thanks for not install the .apia file by default. Remember to update the README.

[asr]

You can fix make generated_all on Travis using something like

make APIA="apia --atp=e --check" generated_all

[asr]

In a fresh clone of your PR, I got the error you pointed out above. You can fix the error by replacing in the Makefile

APIA = dist/build/apia/apia --check

by

APIA = dist/build/apia/apia --check --atp=e

The above change also fix the current Travis error on make generated_all.

[asr]

Please note the Travis doesn't send (email) notifications on pull requests.

[jonaprieto]

Please, look at this. The output errors after run make agda_apia_changed https://gist.github.com/jonaprieto/6899cbcdc2ca928aa96fc10b039301cb the Makefile is https://gist.github.com/jonaprieto/671a566879f7d48f3f006a11e9fcafa2

[asr]

Please, look at this. The output errors after run make agda_apia_changed

I fixed (in master) the problem by 5bee895.

[asr]

Thanks for implementing this feature.