Re: Issue using StrictData

19 Mar 2016

      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 
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/a96933017470d03a1c9414c9c90dfd5c0f090...
$ 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