Adding mechanism for skipping up-to-date files

[viktorcsimma]

Now, agda2hs skips every Agda file for which the corresponding Haskell file is newer than the .agdai file.

For this, I had to replace the moduleFileName function from Render.hs and I chose Compile/Utils.hs; is that OK or should we put it into a different module?

I've also tested it for custom --compile-dir-s. I don't know whether test files for this feature could be easily implemented in the current framework (although it's true that I have not thought about it much).

[omelkonian]

Could you please describe a scenario that the original behaviour is re-compiling unnecessarily?

That way, we might try to add a suitable unit test to also keep us honest.

[jespercockx]

I'm not convinced why this is safe to do. In particular, if a COMPILE AGDA2HS pragma on a record type has been changed from a regular pragma to a class pragma or an unboxed pragma then this has an effect on how Agda modules importing this file are compiled.

[viktorcsimma]

@omelkonian an example looks like this:

In ~/Downloads/agda2hs-skips, there are two Agda files.

A.agda:

module A where

f : {a : Set} -> a -> a
f x = x
{-# COMPILE AGDA2HS f #-}

B.agda:

module B where

open import A

g : {a : Set} -> a -> a
g = f
{-# COMPILE AGDA2HS g #-}

I compiled them with agda2hs -o hs/ B.agda about a week ago. But let's issue the command again:

csimma@csimma-ZenBook:~/Downloads/agda2hs-skips$ agda2hs -o hs/ B.agda
Writing hs/A.hs
Writing hs/B.hs
csimma@csimma-ZenBook:~/Downloads/agda2hs-skips$ ls -l hs/
insgesamt 8
-rw-rw-r-- 1 csimma csimma 37 márc  10 00:00 A.hs
-rw-rw-r-- 1 csimma csimma 49 márc  10 00:00 B.hs
csimma@csimma-ZenBook:~/Downloads/agda2hs-skips$ ls -l *.agda
-rw-rw-r-- 1 csimma csimma 76 márc   3 18:03 A.agda
-rw-rw-r-- 1 csimma csimma 89 márc   3 18:03 B.agda

So it rewrote both, even though neither of them has changed.

[viktorcsimma]

@jespercockx

I'm not convinced why this is safe to do. In particular, if a COMPILE AGDA2HS pragma on a record type has been changed from a regular pragma to a class pragma or an unboxed pragma then this has an effect on how Agda modules importing this file are compiled.

Actually, that is true... then what about recompiling all modules that depend on a changed one, too? That way, we could skip at least the ones that don't depend on anything that has changed.

[viktorcsimma]

@jespercockx

I'm not convinced why this is safe to do. In particular, if a COMPILE AGDA2HS pragma on a record type has been changed from a regular pragma to a class pragma or an unboxed pragma then this has an effect on how Agda modules importing this file are compiled.

Actually, that is true... then what about recompiling all modules that depend on a changed one, too? That way, we could skip at least the ones that don't depend on anything that has changed.

As I can see, it even knows that now. Consider the last example: if you change A.agda (and only that), Agda will re-typecheck both A.agda and B.agda. And since the change dates of the .agdai files seem to be used, agda2hs also recompiles both.

So I think it should be safe even in this state.