[Agda] type check cost

[Sergei Meshveliani]

But I recall now of  --sharing.

Probably, it is appeared in  Development Agda of October 8,  
is it?
I try 

  agda $agdaLibOpt +RTS -M..G -RTS --sharing  Goal.agda    

, and it reports

--------------------
 /home/mechvel/doconA/0.04/reports/costRep-oct8-2015/Nat0.agda:143,1-20
I'm not sure if there should be a case for the constructor s≤s,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  suc m ≟ n
  suc n₁ ≟ 0
when checking the definition of ≤0→≡
--------------------

Nat0.agda  is in the very beginning of the code, that is referred below.

The function is 

  ≤0→≡ : ∀ {n} → n ≤ 0 → n ≡ 0
  ≤0→≡ z≤n =  PE.refl

Without --sharing, it is type-checked.

Is this a bug?

Regards,

------
Sergei



On Sun, 2015-10-11 at 22:08 +0400, Sergei Meshveliani wrote:
> Nils wrote on October 7
> 
> > During the last Agda meeting we implemented some optimisations that
> > might be useful for you. However, AFAIR they have not been released yet.
> > I suggest that you try the development version of Agda.
> 
> 
> Thank you. I have tested  Development Agda of October 8, 2015  
> 
> on type-checking of a certain DoCon-A-oct8-2015-reduced,
> with comparing it to 
>                      Agda 2.4.2.4.
> 
> 1) It takes  1.8  times less space in type checking this example than  
>    Agda 2.4.2.4 takes.
> 
> 2) Its maximal performance 
>    (achieved for  space > 13 Gb for Agda-oct8,  > 17 Gb for Agda 2.4.2.4)
>    is  2 times higher. 
> 
> 3) For  -M12G,  it type-checks in 448 sec. on a  3 GHz machine.
> 
> 
> The code and README.agda  are in 
>      
>     http://www.botik.ru/pub/local/Mechveliani/agdaNotes/costRep-oct8-2015.zip
> 
> Still, the situation is as follows.
> 
> DoCon-A-oct8-2015 is obtained by un-commenting numerous function implementation 
> that are `postulated' in DoCon-A-oct8-2015-reduced,
> and development Agda still needs more than 16 Gb to type check DoCon-A-oct8-2015
> in 30 minutes.
> The project is close to being stuck.
> 
> [..]