[Agda] repeated compilation

[Ulf Norell]

On Fri, Dec 9, 2016 at 11:16 AM, Philipp Hausmann <philipp.hausmann at 314.ch>
wrote:

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


I'm a bit reluctant to pollute the source directory with lots of generated
files (the .agdai files
are bad enough). What we should do is have the compiler put the files in
the project root of
the file being compiled. So module A.B.C in /some/path/A/B/C.agda would
compile to
/some/path/MAlonzo/Code/A/B/C.hs regardless of where the top-level project
is located.

I made a new issue where we can continue the discussion:

https://github.com/agda/agda/issues/2330

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161209/41b61713/attachment.html