[Agda] multiple compilation

[Serge D. Mechveliani]

On Fri, Apr 05, 2013 at 02:52:24PM +0200, Nils Anders Danielsson wrote:
> On 2013-04-04 20:28, Serge D. Mechveliani wrote:
> >1) What precisely is this command for running GHC ?
> >
> >Is it
> >   cd  <where AlgTest.agda resides>
> >   remove  ./AlgTest,  *.hi, *.o  files  of the application
> >   ghc -O -o /home/mechvel/doconA/0.01/source/demoTest/AlgTest -Werror
> >     -i/home/mechvel/doconA/0.01/source/demoTest -main-is MAlonzo.Code.AlgTest
> >     /home/mechvel/doconA/0.01/source/demoTest/MAlonzo/Code/AlgTest.hs
> >     --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
> >?
> 
> I think this should work.
> 
> >2) How to see  stderr ?
> 
> In Bash:
> 
>   <cmd> 1> log.stdout 2> log.stderr


And in  tcsh ?  (I use tc shell).

All right, I did the following.

(1)   agda -c ... AlgTest.agda

It has passed the type check and reported  "... Compilation error:"
(as above).

(2) remove  ./AlgTest,  *.hi, *.o  files  of the application.

(3)  
  ghc -O -o /home/mechvel/doconA/0.01/source/demoTest/AlgTest -Werror
      -i/home/mechvel/doconA/0.01/source/demoTest -main-is 
      MAlonzo.Code.AlgTest
      /home/mechvel/doconA/0.01/source/demoTest/MAlonzo/Code/AlgTest.hs
      --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns

And it succeeds, links the result.
So, I cannot locate the error.

Also I do not precisely know what to do in order to guarantee this
"... Compilation error:" at the next  "agda -c"  command.
Usually it suffices to update with a dummy the currently developed file. 
But not always.

Again: this is          under  Debian Linux + ghc-7.4.1,  
but this is not visible under  Debian Linux + ghc-7.6.2.

Meanwhile, I repeat (under ghc-7.4.1) the  `agda -c'  command, and this 
helps.

Regards,

------
Sergei