[Agda] command line type checker vs interactive

[Sergei Meshveliani]

On Thu, 2015-12-31 at 10:38 -0500, Andrés Sicard-Ramírez wrote:
> On 31 December 2015 at 09:30, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > Year or two ago, similar settings worked.
> > But this year, it says only  "Another command is currently in progress".
> 
> Which is the output of
> 
>   $ type agda
> 
> ?
 
  "agda is /home/mechvel/.cabal/bin/agda"


> After loading (C-c C-l) the file
> 
> postulate
>   Foo : Set
> 
> 
> which is the content in the Emacs buffers *Messages* and *agda2*?
> 

--*Messages* -------------------------------------------

("emacs" "TT.agda")
Loading 00debian-vars...done
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...
Loading debian-ispell...
Loading /var/cache/dictionaries-common/emacsen-ispell-default.el
(source)...done
Loading debian-ispell...done
Loading /var/cache/dictionaries-common/emacsen-ispell-dicts.el
(source)...done
Loading /etc/emacs/site-start.d/50dictionaries-common.el (source)...done
Loading /etc/emacs/site-start.d/50git-core.el (source)...done
Loading /etc/emacs/site-start.d/50latex-cjk-common.el (source)...
Loading cjk-enc...done
Loading /etc/emacs/site-start.d/50latex-cjk-common.el (source)...done
Loading /etc/emacs/site-start.d/50latex-cjk-thai.el (source)...done
Loading /etc/emacs/site-start.d/50thailatex.el (source)...done
Loading /home/mechvel/.cabal/share/x86_64-linux-ghc-7.10.2/Agda-2.5/emacs-mode/agda2.el (source)...done
For information about GNU Emacs and the GNU system, type C-h C-a.
Loading quail/latin-ltx...done
Starting agda process `agda'.
(No changes need to be saved)
agda2-abort-if-in-progress: Another command is currently in progress
(if a command has been aborted you may want to restart Agda)
----------------------------------------------------------------

-- *agda2* -----------------------

Process Agda2 exited abnormally with code 1
IOTCM "/home/mechvel/doconA/0.04/source/TT.agda" NonInteractive Indirect
( Cmd_load_highlighting_info
"/home/mechvel/doconA/0.04/source/TT.agda" )
----------------------------------