Issue using StrictData
Reid Barton
rwbarton at gmail.com
Sun Mar 20 02:46:13 UTC 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 <asr at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160319/b280f99f/attachment.html>
More information about the ghc-devs
mailing list