[Agda] `making' application

[mechvel at scico.botik.ru]

People,

I have an application of many .agda modules, and need to design a 
command
that type-checks and also compiles all of them (with MAlonzo).

I try
   > agda $adgaLibOpt -c TypeCheckAll.agda,          (I)

where TypeCheckAll.agda is

----------------------------------------
module TypeCheckAll where
open import ForTests
import M1
import dir1/M2
...
import dir3/Test1
import dir4/Test2

main : Main
main = run (putStrLn "done")
----------------------------------------

The above  ForTests  reexports things by
   open import IO public using (Main; IO; run; putStrLn),

and Test1 and Test2 import these from ForExport
(ForExport exports "everything" to organize output in this application, 
in addition to things of IO).

And the following files define the `main' function in them:
dir3/Test1.agda, dir4/Test2.agda, TypeCheckAll.agda.

(the first two run examples for demo-and-test).

The problem is that I need a single command (or may be, two commands)
that type-checks and compiles all the above files.
So that when, after things are `made', and one loads the chosen test 
like

   > agda $adgaLibOpt -c dir3/Test1.agda             (II)

no time-consuming complilation must happen
(because all the .o files are ready), and  ./Test1  is created fast for 
running.

In my various attempts to fix it, either (II) causes a long second 
session of compilation
or (II) reports an error about  MAlonzo/Code...main.hs,
or (I) reports "no main function",
...
Can anybody, please, advise on how to arrange this?

Thanks,

------
Sergei