[Agda] type check cost for `open'

[Sergei Meshveliani]

On Sat, 2015-08-15 at 14:58 -0400, Jacques Carette wrote:
> 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!


Thank you for help!

Here is the test close to minimal:

************************************* OverIntegralRing-1.agda ****

open import Function        using (id; _∘_; _$_; flip; case_of_)
open import Relation.Binary using () renaming (Decidable to Decidable₂)

-- of my application --
open import Structures0 using (module Magma; module UpMagma)
open import Structures3 using (module IntegralRing; UpIntegralRing; 
                                              module UpIntegralRing) 
import OverIntegralRing-0 
 
------------------------------------------------------------
module OverIntegralRing-1 {α α=} (upIR : UpIntegralRing α α=)
                   (_∣?_ : let Mg = UpIntegralRing.*magma upIR
                           in  Decidable₂ $ Magma._∣_ Mg 
                   )
  where
  foo =  _∣?_

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

*******************************************************************

30 sec  take the `Skipping' messages for 19 files,
and  11 sec  takes checking  OverIntegralRing-1.agda.

After uncommenting the last `open', I interrupt type checking after 30
minutes. 
Also I cannot test of whether it is ever going to type-check: 
there is not enough memory/time. 

I start to suspect a bug in the argument value transmission between the
two above parametric modules.

Regards,

------
Sergei


> 
> 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
> 
>