[Agda] command line type checker vs interactive

[Wolfram Kahl]

On Thu, Dec 31, 2015 at 06:30:16PM +0400, Sergei Meshveliani wrote:
> In my settings,  Ctrl-C Ctrl-c
> 
> always reports in the interactive mode 
> 
>   "Another command is currently in progress".

Is Agda stiill running?
I use htop ( http://hisham.hm/htop/ ) in a separate terminal (tab),
most of the time with ``SORT-BY: MEM'' which puts the Agda
process on top soon after start-up.

If Agda crashed, the Emacs mode does not notice,
and you just have to ``Kill and restart Agda   C-c C-x C-r''
and then ``Load   C-c C-l'' again.


Hope this helps!

Wolfram


P.S.:

> 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 suggest that you time an Agda run on some single big module
 or reasonably big (sub-)development without and with RTS options
 like (on your 16G machine)

    +RTS -S -H10G -M10G -A1G -RTS

 to see whether it really makes no difference for you ---
 I would be quite surprised.

 The -S is there only to see how busy the garbage collector is
 and how close to the heap limit Agda is operating;
 the -A makes garbage collection ``less nervous'' and for
 my developments end up saving quite some time.
)