[Agda] type check cost for `open'

[Jacques Carette]

I would try a variety of experiments, the first one being

open OverIntegralRing-0 upIR _∣?_ using ()

to see if just that is enough to trigger the problem.  I would also 
comment out all the other opens, to see if they somehow create 
definitions which 'interfere'.  Then I would try each part of your using 
string, aka

        (_∣'?_; *cancel-nz; *cMon-NZ; *upCMon-NZ; IsPrime; prime→≉0;
         Factorization; IsPrime-nz→IsPrime; IsPrime→IsPrime-nz)

one at a time, to see if there is a main culprit.

And then report back, I know I am curious!

Jacques

On 2015-08-15 2:46 PM, 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