Warnings referring to source locations in Cryptol prelude are big, ugly and not reproducible

[brianhuffman]

I was thinking of adding a regression test for #568, but it doesn't really work because the expected output has a warning with unpredictable content. For example, here's what I got this time:

Cryptol> ~ 0x4 where complement x = x
[warning] at <interactive>:1:13--1:23
    This binding for complement shadows the existing binding from
    (at /var/folders/hf/g8kjlj3x4cz05819qsk684_c0000gp/T/Cryptol5521-0.cry:109:11--109:21, complement)
0xb

Next time I start cryptol and run this, I'll get a different temporary file name; if someone else runs it, they'll probably get a completely different temporary directory too.

Maybe it would be better to clean up the printing of locations from the cryptol prelude, or to have a special way of printing them.

[yav]

Once we do renaming earlier, we could also enforce that the built-in syntax always refers to the definitions from the Prelude, so this would be less of an issue.

Still, I wonder if as a first step we change the messages to print the module name instead of the file name?

[brianhuffman]

As of b1edb9e, built-in syntax does always refer to the definitions from the Prelude; I just ran into this problem trying to add a regression test.

Also, I've definitely seen this kind of warning message in other places. For example, in user code that reuses a common name like sum, etc.

[brianhuffman]

As far as changing the message to print the module name instead: I think the filename is generally useful, so that the user can load the file and look at the particular line. It's just not as useful when the filename is a randomly generated temp file.

Do we have a recommended way for users to load up and view (a copy of) the Cryptol prelude in an editor? The warning message should help users do whatever the recommended way is to do that.