[Agda] command line type checker vs interactive

[Wolfram Kahl]

Sergei,

> I mean to report explicitly _all_ the places which are highlighted
> yellow in the interactive checker (mainly they are related to "unsolved
> metas").
> 
> [...]
>
> This ids for  Development Agda of December 18 (ghc-7.8.3).
> It reports
> "Expected a visible argument, but found a hidden argument ...",
> which report looks like a bug in Agda (see README.agda).

A real error like this is, in the interactive view,
often surrounded by unresolved metas that Agda
didn't even try to resolve before it encountered the error ---
I doubt that it would be useful to report those.

No matter whether interactively or using the command line,
I recommend that you comment out the error location
and everything after it,
and try to typecheck the remaining module to see whether
there are real unsolved metas.


Wolfram


P.S.: The only place in Emacs customisation for Agda2
  that nowadays still needs customisation as far as I can see
  is ``Agda2 Program Args'', where I currently have the
  following:

   Agda2 Program Args:
INS DEL String: --no-sharing
INS DEL String: +RTS
INS DEL String: -K256M
INS DEL String: -H10G
INS DEL String: -M10G
INS DEL String: -A1G
INS DEL String: -RTS
INS DEL String: -i
INS DEL String: .
INS DEL String: -i
INS DEL String: /usr/local/packages/Agda-2.4.3.17/lib/std-lib/src
INS


The last line needs to be adapted every time I re-start emacs
with a different path for agda.

I have a shell script ``agdalib'' in the same path as agda
(for each version) which in this case contains

  echo /usr/local/packages/Agda-2.4.3.17/lib/agda-stdlib/src

--- is there a way to put something like ``$(agdalib)'' into the Emacs
customisation?


P.P.S: If you change the Agda version in Agda.cabal, don't forget to change
  it also in src/agda/src/data/emacs-mode/agda2-mode.el before installation.