[Agda] command line type checker vs interactive

[Sergei Meshveliani]

On Wed, 2015-12-30 at 10:49 -0500, Wolfram Kahl wrote:
> [..[

> 
> 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.


In my settings,  Ctrl-C Ctrl-c

always reports in the interactive mode 

  "Another command is currently in progress".

And         > agda $agdaLibOpt Foo.agda
does work.

Today I use   Development Agda of December 31, 2015,  ghc-7.10.2,
              Debian Linux.

Standard library is in  
/home/mechvel/agda/stLib/dec31-2015/src/

The file  .emacs  contains

-------------------------------------------------------------------
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

(custom-set-variables
 '(agda2-program-args (quote ("\"-i\"" "\".\"" "\"-i\""
"\"/home/mechvel/agda/stLib/dec31-2015/src\""))))
-------------------------------------------------------------------

The emacs customization is set as

Agda2 Program Args: [Hide Value]
[INS] [DEL] String: "-i"
[INS] [DEL] String: "."                                    
[INS] [DEL] String: "-i"                                      
[INS] [DEL] String: "/home/mechvel/agda/stLib/dec31-2015/src"      
[INS]

(I suspect that each "-i" can be merged with blank and the next line
string).

I have installed Agda by

  > cabal update
  > cabal install
  > agda-mode compile

Year or two ago, similar settings worked.
But this year, it says only  "Another command is currently in progress".

Can people advise, please?

------
Sergei