[Agda] command line type checker vs interactive

[Sergei Meshveliani]

On Thu, 2015-12-31 at 11:01 -0500, Wolfram Kahl wrote:
> 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?


Probably, not.

  > ps la

shows several processes,  emacs  among them, but not  agda.


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

I command 

  > emacs TT.agda

   C-c C-l

"Another command is currently in progress"
appears at the bottom bar.
Then I command

   C-c C-x C-r
   C-c C-l

And the picture is silent, no messages any more, no coloring.

------
Sergei


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