[Agda] `making' application

[mechvel at scico.botik.ru]

On 2021-04-21 23:07, mechvel at scico.botik.ru wrote:
> 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).


A small stand alone example is in

   http://www.botik.ru/pub/local/Mechveliani/inAgda/makeInAgda.zip

Can you, please, try (with Agda-2.6.1, MAlonzo, lib-1.6)
the commands

  > unzip makeInAgda.zip
  > agda $adgaLibOpt -c TypeCheckAll.agda          (I)
  > agda $adgaLibOpt -c Nat/NatTest.agda           (II)

?

(II) continues to compile things, while I expected that everything is 
compiled by (I).
And it ends with

  /home/mechvel/inAgda/checkAllTest/real/MAlonzo/Code/Nat/NatTest.hs:1:1: 
error:
      The IO action ‘main’ is not defined in module 
‘MAlonzo.Code.Nat.NatTest’
    |
  1 | {-# LANGUAGE EmptyDataDecls, EmptyCase, ExistentialQuantification,
    | ^

Then I comment out the two imports in TypeCheckAll which deal with 
`main':

  module TypeCheckAll where
  open import ForTests
  import Structures-I
  import Int.I
  import Int.I
  -- import Nat.NatTest
  -- import Int.IntTest

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

And remove MAlozo/ and all *.agdai.

Now, (I) and (II) make the needed executable.
But the part (II) includes a long compilation of many modules.

Is this possible to `make' the project so that the first command to do 
almost everything,
so that the next command for making  Nat/NatTest  is done fast?

Thanks,

------
Sergei

  _