-dcore-lint error in simplifier phase 0 when profiling

[wkahl]

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  frelindb@chalmers.se
  * 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-7.0.0.20101029, installed in this sequence:

zlib-0.5.2.0
xhtml-3000.2.0.1
mtl-1.1.0.2.WK
regex-base-0.93.2
regex-posix-0.94.2
syb-0.1.0.3
haskell-src-1.0.1.3
QuickCheck-2.1.1.1
utf8-string-0.3.6
bytestring-0.9.1.7
haskeline-0.6.2.3
binary-0.5.0.2

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

[wkahl]

build log exhibiting core lint error

[wkahl]

Agda patch for GHC-7 compilation

[wkahl]

I configured Agda with the following command:

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

[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...

Simon

[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...

[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.

Simon

[wkahl]

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

Building Agda apparently includes compiling

dist/build/Agda/Syntax/Parser/Parser.hs

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.

[wkahl]

Actually,

dist/build/Agda/Syntax/Parser/Parser.hs

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

dist/build/Agda/Syntax/Parser/Parser.hs

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

  build-depends:
                    syb == 0.1.*

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

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

Wolfram

[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.

Simon

[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:

zlib-0.5.2.0
xhtml-3000.2.0.1
transformers-0.2.2.0
mtl-2.0.1.0
syb-0.2.2
cpphs-1.11
haskell-src-exts-1.9.6
QuickCheck-2.4.0.1
utf8-string-0.3.6
bytestring-0.9.1.7
binary-0.5.0.2
haskeline-0.6.3.2

Each of these has been installed with:

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

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

darcs get --lazy http://code.haskell.org/Agda

In a build directory for this:

ghc --make Setup
./Setup configure --prefix=/usr/local/packages/ghc-7.0.1 -p \
                  --ghc-options="-dcore-lint"
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!)

Wolfram

[wkahl]

build log using ghc-7.0.1, exhibiting core lint error

[simonmar]

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.

[igloo]

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