Issue using StrictData
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
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
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
Hi,
On 19 March 2016 at 21:46, Reid Barton
`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.
I was aware of it.
Is that really what you wanted?
No really. I added the extension just out curiosity.
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.
Thanks you for the explanation. Best, -- Andrés
participants (2)
-
Andrés Sicard-Ramírez -
Reid Barton