<div dir="ltr">Hi,<br><div><br>`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.<br><br></div><div>I'm guessing you meant `other-extensions: StrictData`.<br><br></div><div>Regards,<br></div><div>Reid Barton<br></div><div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 19, 2016 at 10:16 PM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
I know this isn't a convenient issue report because the "test case"<br>
isn't easily reproducible. Since I don't understand the issue, I don't<br>
know how to create a smaller test case, sorry.<br>
<br>
My OS is Ubuntu 12-04 (64 bits) and I'm using the following programs:<br>
<br>
Agda master branch on commit<br>
<br>
<a href="https://github.com/agda/agda/commit/181a954a40b137c8deb1df801a8ee55fdbc19116" rel="noreferrer" target="_blank">https://github.com/agda/agda/commit/181a954a40b137c8deb1df801a8ee55fdbc19116</a><br>
<br>
GHC ghc-8.0 branch on commit<br>
<br>
<a href="https://git.haskell.org/ghc.git/commit/a96933017470d03a1c9414c9c90dfd5c0f0903ed" rel="noreferrer" target="_blank">https://git.haskell.org/ghc.git/commit/a96933017470d03a1c9414c9c90dfd5c0f0903ed</a><br>
<br>
$ cabal --version<br>
cabal-install version 1.23.0.0<br>
compiled using version 1.23.1.0 of the Cabal library<br>
<br>
(compiled with GHC 7.10.3)<br>
<br>
$ alex --version<br>
Alex version 3.1.7, (c) 2003 Chris Dornan and Simon Marlow<br>
<br>
$ happy --version<br>
Happy Version 1.19.5 Copyright (c) 1993-1996 Andy Gill, Simon Marlow<br>
(c) 1997-2005 Simon Marlow<br>
<br>
After adding `extensions: StrictData` to Agda.cabal, I'm getting the<br>
following errors:<br>
<br>
$ cabal install<br>
...<br>
Installing library in<br>
/home/asr/.cabal/lib/x86_64-linux-ghc-8.0.0.20160316/Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU<br>
Installing executable(s) in /home/asr/.cabal/bin<br>
Generating Agda library interface files...<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Primitive!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Bool!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Char!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Coinduction!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Equality!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Float!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.FromNat!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.FromNeg!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.FromString!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck <a href="http://Agda.Builtin.IO" rel="noreferrer" target="_blank">Agda.Builtin.IO</a>!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck <a href="http://Agda.Builtin.Int" rel="noreferrer" target="_blank">Agda.Builtin.Int</a>!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.List!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Nat!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Reflection!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Size!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Strict!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.String!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.TrustMe!<br>
agda: Internal Happy error<br>
<br>
CallStack (from HasCallStack):<br>
error, called at templates/GenericTemplate.hs:288:17 in<br>
Agda-2.5.0-8eDdWzYvIFd4CKBTUUP6kU:Agda.Syntax.Parser.Parser<br>
WARNING: Failed to typecheck Agda.Builtin.Unit!<br>
Registering Agda-2.5.0...<br>
cabal: Leaving directory '.'<br>
Installed Agda-2.5.0<br>
<br>
Best,<br>
<span class=""><font color="#888888"><br>
--<br>
Andrés<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</font></span></blockquote></div><br></div></div></div>