Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding mechanism for skipping up-to-date files #300

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

viktorcsimma
Copy link
Contributor

@viktorcsimma viktorcsimma commented Mar 3, 2024

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).

@viktorcsimma viktorcsimma marked this pull request as ready for review March 3, 2024 17:12
@omelkonian
Copy link
Contributor

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
Copy link
Member

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
Copy link
Contributor Author

viktorcsimma commented Mar 9, 2024

@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
Copy link
Contributor Author

@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
Copy link
Contributor Author

viktorcsimma commented Apr 9, 2024

@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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants