search

UU-ComputerScience / uhc

136 stars 21 forks source link

Unexpected "GRIN ByteCode location names not in scope" #77

Open phile314 opened 8 years ago

phile314 commented 8 years ago

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: https://github.com/agda/agda/issues/1879

asr commented 8 years ago

I could reproduce the error in the OP using UHC 1.1.9.4. Any ideas?

atzedijkstra commented 8 years ago

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

On 23 May 2016, at 10:45, Andrés Sicard-Ramírez notifications@github.com wrote:

I could reproduce the error in the OP using UHC 1.1.9.4. Any ideas?

— You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub

atzedijkstra commented 8 years ago

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?