[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