Hi,

`extensions: StrictData` turns on the StrictData extension for all modules in the program. So every field of every data type defined in every module is made strict. Is that really what you wanted? For a large, complicated program like Agda, It seems about as likely to work as just passing the program into an ML compiler unmodified. Your errors are a typical example: note they are runtime errors from a generated happy parser, which probably does something like initializing a record with (error "Internal Happy error") and then trying to update it with record update syntax.

I'm guessing you meant `other-extensions: StrictData`.

Regards,
Reid Barton

On Sat, Mar 19, 2016 at 10:16 PM, Andrés Sicard-Ramírez <asr@eafit.edu.co> wrote:
Hi,

I know this isn't a convenient issue report because the "test case"
isn't easily reproducible. Since I don't understand the issue, I don't
know how to create a smaller test case, sorry.

My OS is Ubuntu 12-04 (64 bits) and I'm using the following programs:

Agda master branch on commit

  https://github.com/agda/agda/commit/181a954a40b137c8deb1df801a8ee55fdbc19116

GHC ghc-8.0 branch on commit

  https://git.haskell.org/ghc.git/commit/a96933017470d03a1c9414c9c90dfd5c0f0903ed

  $ cabal --version
  cabal-install version 1.23.0.0
  compiled using version 1.23.1.0 of the Cabal library

(compiled with GHC 7.10.3)

  $ alex --version
  Alex version 3.1.7, (c) 2003 Chris Dornan and Simon Marlow

  $ happy --version
  Happy Version 1.19.5 Copyright (c) 1993-1996 Andy Gill, Simon Marlow
(c) 1997-2005 Simon Marlow

After adding `extensions: StrictData` to Agda.cabal, I'm getting the
following errors:

  $ cabal install
  ...
  Installing library in
  /home/asr/.cabal/lib/x86_64-linux-ghc-8.0.0.20160316/Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU
  Installing executable(s) in /home/asr/.cabal/bin
  Generating Agda library interface files...
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Primitive!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Bool!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Char!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Coinduction!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Equality!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Float!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.FromNat!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.FromNeg!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.FromString!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.IO!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Int!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.List!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Nat!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Reflection!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Size!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Strict!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.String!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.TrustMe!
  agda: Internal Happy error

  CallStack (from HasCallStack):
    error, called at templates/GenericTemplate.hs:288:17 in
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser
  WARNING: Failed to typecheck Agda.Builtin.Unit!
  Registering Agda-2.5.0...
  cabal: Leaving directory '.'
  Installed Agda-2.5.0

Best,

--
Andrés
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs