[Agda] RE: agda coredump

[Sivaram Gowkanapalli]

Hello,

I have narrowed down the coredumps to be caused by the usage of show.

open import Data.Nat.Show using (show)
fromString : String → Colist Char
fromString = fromColist ∘ toCostring

main = (putStrLn ∘ fromString) (show 0) -- coredumps
main = (putStrLn ∘ fromString) ("0") -- does not coredump

though C-c C-n in emacs on main, shows the output for both commands.

Thanks


From: sivaramreddy at hotmail.com
To: agda at lists.chalmers.se
Subject: agda coredump
Date: Thu, 24 Mar 2011 15:10:14 -0400
























Hello,

The attached source file coredumps when I execute it from shell as "./mylist", where as the term "main" seems to work fine in emacs and it shows the output in emacs as:

putStrLn
(Foreign.Haskell._∷_ 'l'
 (.Foreign.Haskell.♯-0 'l'
  (.Data.Colist.♯-2 'l'
   (.Data.List.List._∷_ 'e'
    (.Data.List.List._∷_ 'n'
     (.Data.List.List._∷_ 'g'
      (.Data.List.List._∷_ 't'
       (.Data.List.List._∷_ 'h'
        (.Data.List.List._∷_ ' '
         (.Data.List.List._∷_ 'o'
          (.Data.List.List._∷_ 'f'
           (.Data.List.List._∷_ ' '
            (.Data.List.List._∷_ 'l'
             (.Data.List.List._∷_ 'i'
              (.Data.List.List._∷_ 's'
               (.Data.List.List._∷_ 't'
                (.Data.List.List._∷_ ':'
                 (.Data.List.List._∷_ ' '
                  (.Data.List.List._∷_ '0' .Data.List.List.[])))))))))))))))))))

my versions are: 

┌─(~/dev/apps/haskell/agda/learn)─────────────────────────────────────────────────────────────────────────────────────────────────────────────────(pts/1 at firefox)─┐
ghc -v
Glasgow Haskell Compiler, Version 7.0.2.20110316, for Haskell 98, stage 2 booted by GHC version 6.12.3
Using binary package database: /home/j/.ghc/lib/ghc-7.0.2.20110316/package.conf.d/package.cache
Using binary package database: /home/j/.ghc/i386-linux-7.0.2.20110316/package.conf.d/package.cache
hiding package Agda-2.2.10 to avoid conflict with later version Agda-2.2.11
hiding package syb-0.2.2 to avoid conflict with later version syb-0.3
hiding package xmonad-contrib-0.9.2 to avoid conflict with later version xmonad-contrib-0.10
hiding package xmonad-0.9.2 to avoid conflict with later version xmonad-0.10
wired-in package ghc-prim mapped to ghc-prim-0.2.0.0-6bf7b03ebc9c668817e4379b6796c0c2
wired-in package integer-gmp mapped to integer-gmp-0.2.0.3-91607778cf3ae8f3948a50062b4f8479
wired-in package base mapped to base-4.3.1.0-cf5fbbf5ccbd0475ad054efbb121340e
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.5.0.0-f0c8f015e470d561d64a578434331367
wired-in package dph-seq not found.
wired-in package dph-par not found.
Hsc static flags: -static
*** Deleting temp files:
Deleting: 
*** Deleting temp dirs:
Deleting: 
ghc: no input files
Usage: For basic information, try the `--help' option.
┌─(~/dev/apps/haskell/agda/learn)─────────────────────────────────────────────────────────────────────────────────────────────────────────────────(pts/1 at firefox)─┐
ghc-pkg list -v | grep -i agda
    Agda-2.2.10 (Agda-2.2.10-63be3f8749c7ebfb7d87b08fb5483c8c)
    Agda-2.2.11 (Agda-2.2.11-e2c6a5deeb94eddc4a90b96a521ea4e5)
┌─(~/dev/apps/haskell/agda/learn)─────────────────────────────────────────────────────────────────────────────────────────────────────────────────(pts/1 at firefox)─┐
agda --version
Agda version 2.2.10
┌─(~/dev/apps/haskell/agda/learn)─────────────────────────────────────────────────────────────────────────────────────────────────────────────────(pts/1 at firefox)─┐
./mylist
zsh: segmentation fault (core dumped)  ./mylist

Please let me know if you want the core file.

Thanks
Siva
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110324/95fe9a21/attachment-0001.html