[Agda] Seg-fault

[Serge D. Mechveliani]

On Mon, Oct 15, 2012 at 12:00:06PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-13 21:32, Serge D. Mechveliani wrote:
>> I have programmed the  merge sorting function  for a list over any
>> DecTotalOrder,
>> with the result record including a proof for orderedness.
>>
>> It is compiled for the RTS options, and run with  +RTS -M... -RTS.
>> For a certain large list over Nat, it finishes for  -M700m and 900m,
>> but runs into  Segmentation fault  for 800m.
>
> That's interesting. Please report this on the bug tracker.
>


This is  issue 716.

See there the attached archive.
This is for 
 Agda-2.3.0 + MAlonzo + lib-0.6,
 Debian Linux, 
 2 Gb RAM,
 Intel(R) Pentium(R) 4 Mobile  

Files:  readme.txt
        Main.agda    
        OrdL.agda       -- two sorting functions
        Constants.agda  -- exports  ordListCounter : Bin,  this is needed 
                        -- to avoid a long compilation time normalization

Compilation:   agda -c --ghc-flag=-rtsopts $agdaLibOpt Main.agda 
,
where  $agdaLibOpt  defines the residence of the  lib-0.6  files.

Running:    ./Main +RTS -M1600m -RTS
            ./Main 

But I failed to reproduce Seg-fault on another Linux machine (of 1 Gb RAM). 
So, I wonder whether the effect is hardware specific, or Linux version
specific.

readme.txt  also has a couple of a beginner questions, I shall be grateful 
to people for advices.

Thanks, 
Sergei.