Repository navigation
Unexpected "GRIN ByteCode location names not in scope" #77
Description
When compiling the Agda Standard library, I get the following UHC compilation error:
[124/238] Compiling Core Agda.Relation.Binary.Product.Pointwise (Agda/Relation/Binary/Product/Pointwise.bcr) Compilation error: Grin to ByteCode (Internal) GRIN ByteCode location names not in scope: Agda.Relation.Binary.Product.Pointwise.x141_@UNQ_@195_@FFE_@nl.uu.agda.fresh-local-name
I have looked at the corresponding UHC Core file, and the code there looks fine to me.
Pointwise.tcr.txt
The core dump uses a slightly different pretty printer for the names, but searching for x141
should yield the interesting occurences.
If I compile using -O0, everything works fine and the produced binary executes successfully. Omitting the -O0 option, the above error happens. I don't have a minimal example, the code triggering this depends on 124 other Agda modules. I also don't have a Haskell file triggering this. I tested using UHC 1.1.9.3.
Related Agda issue: agda/agda#1879
Activity
asr commentedon May 23, 2016
I could reproduce the error in the OP using UHC 1.1.9.4. Any ideas?
atzedijkstra commentedon May 23, 2016
I have not yet looked into this (and have less time doing so coming weeks...). My usual way of finding out where it goes wrong is to build variant 99 (make 99/ehc;make 99/ehclib; install/bin/99/ehc --help # look for "dump") which allows dumping of intermediate core/grin transformation stages. Usually something goes wrong there. It is then a matter of finding out where Core/Grin is still correct and is transformed to something incorrect (as the front end code generation is not used in this issue). I suspect there will be a erroneous code float.
A
atzedijkstra commentedon Aug 21, 2016
The given .tcr file is not parseable. In general the full dump language is richer than what the parser for .tcr files accepts. Could you provide a .bcr file, i.e. a binary dump?