[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