[Agda] repeated compilation

Andreas Abel abela at chalmers.se
Fri Dec 9 11:03:31 CET 2016


GHC might decide to recompile if you give it different options then the 
first time.

GHC options present:

 >    agda -c $agdaLibOpt +RTS...-RTS $agdaGHC_opt TypeCheckAll.agda

GHC options absent:

 >  > agda -c $agdaLibOpt Test1.agda

On 09.12.2016 10:36, Sergei Meshveliani wrote:
> People,
>
> my application library is type-checked and compiled by
>
>    agda -c $agdaLibOpt +RTS...-RTS $agdaGHC_opt TypeCheckAll.agda
>
> This reports "Checking" and "Compiling" messages for each module of
> application except tests.
> Then I command
>
>  > cd demoTest
>  > agda -c $agdaLibOpt Test1.agda
>
> And it issues the "Compiling" messages for all the modules that have
> been compiled earlier. Like this:
>
>   [ 96 of 120] Compiling MAlonzo.Code.List.Multiset0
>   (MAlonzo/Code/List/Multiset0.hs, MAlonzo/Code/List/Multiset0.o)
>
> Does it really recompile them? Has this a reason?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list