[Agda] multiple compilation

Serge D. Mechveliani mechvel at botik.ru
Thu Apr 4 20:28:45 CEST 2013


On Thu, Apr 04, 2013 at 03:38:08PM +0200, Nils Anders Danielsson wrote:
> On 2013-03-30 19:39, Serge D. Mechveliani wrote:
> >This is not reported. The last report line is exactly this:
> >------------------
> >Compilation error:
> >------------------
> 
> What happens if you run GHC manually? Does GHC produce an error message?
> Is this printed on stderr or stdout?


In Debian Linux + ghc-7.4.1,

I remove  *.agdai, *.hs, *.hi, *.o  files of my application
(and do not touch files made from Standard library)
and command

    agda -c -v 2 $agdaLibOpt AlgTest.agda  > & log

This prints to the file  ./log  (I format this output a bit):

-------------------------------------------------------------------------
...
...
Relation.Nullary.Negation : no compilation is needed.
Relation.Unary : no compilation is needed.
Compiling ResidueI in /home/mechvel/doconA/0.01/source/ResidueI.agdai to 
 /home/mechvel/doconA/0.01/source/demoTest/MAlonzo/Code/ResidueI.hs
Calling:
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

[ 1 of 98] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[ 3 of 98] Compiling MAlonzo.Code.Level 
             ( MAlonzo/Code/Level.hs, MAlonzo/Code/Level.o )
[ 4 of 98] Compiling MAlonzo.Code.Function 
             (MAlonzo/Code/Function.hs, MAlonzo/Code/Function.o )
[40 of 98] Compiling MAlonzo.Code.Nat2 
                          ( MAlonzo/Code/Nat2.hs, MAlonzo/Code/Nat2.o )
[44 of 98] Compiling MAlonzo.Code.DPrelude 
                   ( MAlonzo/Code/DPrelude.hs, MAlonzo/Code/DPrelude.o )
[46 of 98] Compiling MAlonzo.Code.Algebra 
                   ( MAlonzo/Code/Algebra.hs, MAlonzo/Code/Algebra.o )
[56 of 98] Compiling MAlonzo.Code.List2 
          ( MAlonzo/Code/List2.hs, MAlonzo/Code/List2.o )
[57 of 98] Compiling MAlonzo.Code.AlgClasses1 
                 ( MAlonzo/Code/AlgClasses1.hs, MAlonzo/Code/AlgClasses1.o )
[58 of 98] Compiling MAlonzo.Code.AlgClasses2 
                 ( MAlonzo/Code/AlgClasses2.hs, MAlonzo/Code/AlgClasses2.o )

Compilation error:
--------------------------------------------------------------------


> Is this printed on stderr or stdout?

I see this in  ./log.   Is this  stdout ?


> What happens if you run GHC manually? Does GHC produce an error message?

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
?

2) How to see  stderr ?

Thanks,

------
Sergei


More information about the Agda mailing list