[Agda] weird behavior with large records

Chris Casinghino ccasin at cis.upenn.edu
Wed Jun 2 20:02:56 CEST 2010


Hi Andrés and gallais,

Since neither of you can reproduce the error and I have a workaround,
perhaps it is not so important.  However, to answer this question:

> What is the output in the *ghci* buffer?

In this buffer, I see:


relude Agda.Interaction.GhciTop> ioTCM
"/home1/c/ccasin/crap/FSets.agda" (Just "/tmp/agda2-mode15173qKo") (
cmd_load "/home1/c/ccasin/crap/FSets.agda"
["/home1/c/ccasin/work/agda/libs/lib-0.3/src", "."] )
agda2_mode_code (agda2-status-action "")
Checking FSets (/mnt/castor/seas_home/c/ccasin/crap/FSets.agda).
Skipping Level (/home1/c/ccasin/work/agda/libs/lib-0.3/src/Level.agdai).
...
Skipping Algebra (/home1/c/ccasin/work/agda/libs/lib-0.3/src/Algebra.agdai).
Skipping Data.List (/home1/c/ccasin/work/agda/libs/lib-0.3/src/Data/List.agdai).
*** Exception: stack overflow
Prelude Agda.Interaction.GhciTop> ioTCM
"/home1/c/ccasin/crap/FSets.agda" Nothing ( cmd_goals
"/home1/c/ccasin/crap/FSets.agda" )
agda2_mode_code (setq agda2-response '())
Prelude Agda.Interaction.GhciTop>


That stack overflow must be the problem.  I'm not sure what could
cause it - the file doesn't seem to be so big as to chew through that
much memory, and if it works for you an infinite loop seems unlikely.
I'm not sure how to see or adjust the size of the stack available to
agda.

--Chris


More information about the Agda mailing list