[Agda] type check cost for `open'

[Sergei Meshveliani]

False alarm! 
I am sorry.

I have got used to that the computer has  16 Gb RAM.
But in reality it had                     12 Gb.

Because a couple of days ago it has been opened, a bit unluckily, as 
it occurs. 
Now I look more attentively at the `top' output on memory, and see 12
Gb.
This is why these strange problems with the `open' performance and
swapping were visible when I tried  -M10G  or more  
(also even frightening Segmentation fault appeared when I tried 
-M13 -H13 !). 

Now, it is returned to  16 Gb,  and I set -M14G without getting
swapping, and Agda works as expected.

---------------------
But generally, the project is growing, and the threaten of overfilling
16 Gb still remains.
Splitting to small modules takes effort, and most often does not look
natural. For example, a considerable import and `open' environment is
partly repeated.
And I do not expect that it would get into 8 Gb even with maximal module
splitting. 

May be, the future  --sharing  will help, I do not know.

Regards,

------
Sergei



On Sat, 2015-08-15 at 22:46 +0400, Sergei Meshveliani wrote:
> People,
> 
> I have a problem of the  type check cost for the `open' declaration.
> 
> The project consists of about 20 files:
> 
>   Foo1.agda ... Foo18, OverIntegralRing-0.agda, OverIntegralRing-1.agda.
> 
> It is for               Agda 2.4.2.3.
> The machine is of       16 Gb RAM,  3 GHz.
> Type checking is under  -M13G -H13G
> 
> (-A1G does not effect essentially).
> 
> The first 19 files are type-checked in 1-2 hours,
> and I take this as "Anyway, it is done. let us type-check the next and
> see".
>  
> OverIntegralRing-0.agdai  has  12 Mb size.
> Other .agdai files have         4 Mb on average.
> 
> There arises a question of type-checking  OverIntegralRing-1.agda.
> This file is as follows:
> 
> 
> ************************************** OverIntegralRing-1.agda **
> open import Level using ...
> ...
> open import Relation.Binary using ...
> ...
> open import Data.Nat using (ℕ; suc)
> 
> -- of DoCon-A --
> open import Structures0 using (module Magma; module UpMagma)
> ...
> open import Structures3 using (module IntegralRing; UpIntegralRing; 
>                                                 module UpIntegralRing) 
> open import Factorization.FtMonoid using 
>                                    (module OfCancellativeCommMonoid)
> import OverIntegralRing-0   --
>  
> -------------------------------------------------------------
> module OverIntegralRing-1 {α α=} (upIR : UpIntegralRing α α=)
>                    (_∣?_ : let Mg = UpIntegralRing.*magma upIR
>                            in  Decidable₂ $ Magma._∣_ Mg 
>                    )
>   where
>   open UpIntegralRing upIR using (...)
>                 renaming (Carrier to C; *upCommutativeMonoid to *upCMon)
>   open IsEquivalence isEquivalence using () 
>                   renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)
>   open EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)
>   open UpMagma *upMagma using (_∣_; _∤_; ∣cong₁; ∣cong₂; ∤cong₁)
>                                                 renaming (_~asd_ to _~_)
>   open UpMonoid *upMonoid using (_^_; ^1=id; ∣trans)
>   open CommutativeSemigroup *commutativeSemigroup using (bothFactors∣)
>   open MonoidLemmata *upMonoid     using (^cong₁; x∣x; x^2≈xx)
>   open RingLemmata   upRing        using (0*; ∣nonzero→≉0)
>   open Ring1Lemmata  upRingWithOne using (∣1→≉0; 0^suc) 
> 
> {- -- expensive 
>   open OverIntegralRing-0 upIR _∣?_ using                       
>        (_∣'?_; *cancel-nz; *cMon-NZ; *upCMon-NZ; IsPrime; prime→≉0; 
>         Factorization; IsPrime-nz→IsPrime; IsPrime→IsPrime-nz)
> -}
> *******************************************************************
> 
> And that is all:  
> only open several modules imported from previous files.
> 
> 1. It is type-checked in  41 sec,  with  .agdai  of ~ 900 Kb
>    (the smallest .agdai).
> 
> 
> 2. Uncomment the last `open'.
> Then  30 min  is not enough to type-check. Many Gb are allocated.
> 
> Giving  14 Gb  leads to swapping, this slows down the process greatly
> (I expect that on a 32 Gb machine and under -M24G it will type-check in 
> 1 minute).
> 
> I need to program several functions in this environment.
> But this very environment fails to type check on a 16 Gb machine.
> 
> The are two functions set under  NO_TERMINATION_CHECK
> -- this pragma will be removed after certain `panic' is fixed in Agda.
> Probably, this pragma does not increase the type check cost
> (can it?).
> 
> Is something wrong in the Agda implementation approach?
> (a real sharing, the normal form interpreter ... I do not know).
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>