[Agda] repeated compilation

[Philipp Hausmann]

If I recall correctly, Agda compiles everything in the current working 
directory inside ./MAlonzo. This also
applies to included Agda files or libraries, so Agda doesn't see the 
already existing Haskell files in yourlib/MAlonzo
if you compile a test program in another directory. One workaround is to 
copy the MAlonzo folder from your library
into the current working directory:

cp -r MAlonzo demoTest/MAlonzo

Maybe MAlonzo should instead put the generated *.hs files next to the 
agda/agdai files?


Philipp

On 12/09/2016 11:03 AM, Andreas Abel wrote:
> 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
>>
>
>