[Agda] re-checking

Sergei Meshveliani mechvel at botik.ru
Mon Oct 3 21:09:27 CEST 2016


People,
I have files  M1.agda, M2.agda, M3.agda  which are already type-checked
(in Development Agda of September 16, 216),
and apply
    > agda $agdaLibOpt M4.agda,

where M4 imports previous modules.
Agda reports
 Skipping M1
 Skipping M2
 Skipping M3
 Checking M4 
 Finished M4 ...

Then I apply  
     > agda $agdaLibOpt M5.agda,

where M5 imports previous modules.

And most of the files that were earlier reported as `Skipping' are now
reported as `Checking'.
And have not touched M1, M2, M3.
How can this happen?

Regards,

------
Sergei





More information about the Agda mailing list