Opened 9 years ago

Closed 8 years ago

#4462 closed bug (fixed)

-dcore-lint error in simplifier phase 0 when profiling

Reported by: wkahl Owned by:
Priority: normal Milestone: 7.4.1
Component: Compiler Version: 7.0.1 RC1
Keywords: profiling, simplifier, core-lint Cc:
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: Compile-time crash Test Case: Agda (darcs, current)
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


I am getting another core-lint error when compiling Agda with profiling (error message attached).

This is with the darcs version of Agda, up to the following changes:

Mon Nov  1 13:18:39 EDT 2010
  * Fixed issue 355

I applied one additional patch (attached below) and bumped version limits in Agda.cabal to get it to compile (and removed -Werror).

I have the following packages installed in my GHC-, installed in this sequence:


(Some of these have trivial edits (mostly .cabal version limit bumps) to compile.)

Attachments (3)

2010-11-01_ghc- (13.2 KB) - added by wkahl 9 years ago.
build log exhibiting core lint error
2010-11-01_GHC7_signatures.patch (12.7 KB) - added by wkahl 9 years ago.
Agda patch for GHC-7 compilation
build-2010-11-25.log.bz2 (17.2 KB) - added by wkahl 9 years ago.
build log using ghc-7.0.1, exhibiting core lint error

Download all attachments as: .zip

Change History (16)

Changed 9 years ago by wkahl

build log exhibiting core lint error

Changed 9 years ago by wkahl

Agda patch for GHC-7 compilation

comment:1 Changed 9 years ago by wkahl

I configured Agda with the following command:

./Setup configure -p --prefix=/usr/local/packages/ghc- --ghc-options="-dcore-lint -rtsopts"

comment:2 Changed 9 years ago by simonpj

Of course this should not happen. Does it happen when you are not profiling?

I believe it'll run ok if you switch off Core Lint. Does it?

Looks like there a bit of a setup cost to reproducing this...


comment:3 Changed 9 years ago by wkahl

Without profiling, it compiles with -dcore-lint and runs apparently not worse than with GHC-6.12.3. (Some success, some segfaults, no RTS errors yet.)

With profiling and without -dcore-lint, it compiles okay, and even compiling agda-executable (in src/main) configured with -dcore-lint compiles okay.

I am sorry about the setup cost! It is admittedly high also for me: I am doing this kind of experiments since I guess that you are not too keen on looking into run-time errors with GHC-6.12.3 unless I can say that they are still there at least with 7.0.

I consider part of the setup cost to be due to “design decisions” in cabal; see for example cabal ticket 725. In short, I think that these cabal policies put a big stumbling block in the way of anybody who wants to “just try things out with HEAD”, unless they don't use any non-GHC packages, of course...

Perhaps Simon M still has the setup from ticket:4265 around...

comment:4 Changed 9 years ago by simonpj

I'm utterly swamped at the moment. It sounds as if this is a bug, but not a show-stopping bug, so we can make a release despite it.

I'm a bit pertubed by your "some success, some segfaults" statement. GHC should never segfault unless you are using unsafeCoerce or the FFI.


comment:5 Changed 9 years ago by wkahl

GHC should never segfault unless you are using unsafeCoerce or the FFI.

Building Agda apparently includes compiling


which seems to be generated by the Agda compiler and therefore consists largely of unsafeCoerce, but I could not find where it is called, and in any case, by Agda's behaviour I do not think it is parsing while it crashes on me.

Agda works somewhat like ghc --make, and on the first attempt to typecheck something complex I almost certainly get a crash, but not necessarily on the second attempt, which uses the .agdai files the first attempt created. I have not yet started to try to delete these for reproduction, but I am currently concentrating on crashes that reproduce directly, and preferably with more information than just a segfault. With the latter aspect, I haven't been successful with GHC-7 yet, but I have a reproducible segfault that apparently still is a segfault (second attempt running right now) with the binary compiled with -debug.

With ghc-6.12.3 I have been more successful, and I just submitted ticket:4472 so that you can at least see that.

comment:6 Changed 9 years ago by wkahl



is generated by Happy, and Cabal invokes Happy, without asking, and without opportunity to override, with -agc. I have manually regenerated


with -ag, and see, as expected, the same segfaults (and the same core-lint error).

I have the following times to segfault:

Common RTS flags:

+RTS     -C0 -i0 -K64M -M12G -H12G -S
Binary      Additional flags   Time       Alloc Sum
agda                           17min     870,907,904,328
agda_debug                     27min     870,907,904,288
agda_prof  +RTS      -xc       49min   1,138,794,235,424
agda_debug +RTS -DS           656min     870,907,945,760

-xc unfortunately gives no cost-center stack for the segfault. But there are 20 exceptions in these runs, generating 403kBytes of additional output.

The allocation sums are calculated by adding up the first column of the +RTS -S output, and are all constant across several runs. (The -DS runs were with the old parser; the two fast runs both allocated 870,907,945,760 bytes with the old parser.)

Agda links with Haskeline, but that is not used in my kind of invocation. The only other potentially suspicious part seems to be

                    syb == 0.1.*

for which I have syb- Do you think that syb is worth investigating for this?

Do you have any other ideas what I could do to locate this segfault?


comment:7 Changed 9 years ago by igloo

Milestone: 7.0.2

comment:8 Changed 9 years ago by simonpj

I'm not sure how to progress this.

Agda itself is written in Haskell and should run flawlessly.

I believe that what Agda does is to translate Agda programs into Haskell programs that are littered with unsafeCoerce and use GHC to compile those. GHC wasn't intended for tha, so it wouldn't be suprising if something goes wrong.

Finally, profiling is somehow implicated with your Lint error.

I'm inlined to suggest that you get help from the Agda folk to help narrow down where the problem is. I really don't know where to start.


comment:9 Changed 9 years ago by wkahl

First of all, since the unsafeCoerce calls in dist/build/Agda/Syntax/Parser/Parser.hs were generated by Happy, and Happy can be persuaded not to generate them, there are no unsafeCoerce calls left in Agda. There is also no Agda-generated code in Agda (I originally was mistaken, since I never would have suspected that Happy does such a thing), so, for the original core-lint error, it does not matter what Agda does.

I have been able to reproduce that original error with 7.0.1, with the following packages, all fresh from hackage and installed in the given order:


Each of these has been installed with:

rm -rf $P
tar xzf $P''.tar.gz
cd $P
ghc --make Setup
./Setup configure --prefix=/usr/local/packages/ghc-7.0.1 -p \
./Setup build
./Setup haddock
./Setup install
cd ..

For GHC-7, we need the current Agda development version from darcs:

darcs get --lazy

In a build directory for this:

ghc --make Setup
./Setup configure --prefix=/usr/local/packages/ghc-7.0.1 -p \
alex -g -o dist/build/Agda/Syntax/Parser/Lexer.hs src/full/Agda/Syntax/Parser/Lexer.x
happy -ag -o dist/build/Agda/Syntax/Parser/Parser.hs src/full/Agda/Syntax/Parser/Parser.y
time ./Setup build -v > build-2010-11-25.log 2>&1

(Cabal hardwires -agc for happy, so we need to call happy ourselves preemptively.)

build-2010-11-25.log will be attached.

(I will open a separate ticket for my segfaults if I find out more about them. Sorry for distracting from the original problem on this ticket!)


Changed 9 years ago by wkahl

Attachment: build-2010-11-25.log.bz2 added

build log using ghc-7.0.1, exhibiting core lint error

comment:10 Changed 9 years ago by igloo


comment:11 Changed 8 years ago by igloo


comment:12 Changed 8 years ago by simonmar

difficulty: Unknown
Status: newinfoneeded

Please could you try this with GHC 7.4 - profiling has been overhauled and many bugs have been fixed, it's quite likely that it works now.

comment:13 Changed 8 years ago by igloo

Resolution: fixed
Status: infoneededclosed

No response from submitter, so optimistically assuming this is fixed. Please reopen if not.

Note: See TracTickets for help on using tickets.