Add unicode support to the saw-script lexer

[sauclovian-g]

Closes #2042.

[sauclovian-g]

Note that there was some talk about banning non-8-bit characters from SAW strings until the question of how to deal with them in Cryptol strings gets resolved. I don't think there's any real need to do that, so I haven't, because (a) you can do very little with SAW strings anyway and (b) there doesn't seem to be any way to convert between SAW and Cryptol strings. (There's no eval_string or string_to_term functions to match eval_int and int_to_term.)

[RyanGlScott]

LGTM! Worth an addition to the changelog, though.

Note that there was some talk about banning non-8-bit characters from SAW strings until the question of how to deal with them in Cryptol strings gets resolved. I don't think there's any real need to do that, so I haven't

I agree, no need to do so here.

[RyanGlScott]

Indiana would be proud.

[sauclovian-g]

LGTM! Worth an addition to the changelog, though.

Definitely. Completely forgot.

Also, I appear to have accidentally corrected the position spanning behavior for Cryptol fragments and quoted strings, which is why a bunch of the column numbers in test_type_errors changed. (The position for the whole of such objects now includes the end characters as well as the start characters; previously it left off the end characters.) I've checked all the diffs and they're all correct.

(not all the columns are still entirely correct, e.g. the start position for (x : Int) <- "abc" is column 2, not column 1, but that's for some other time)

[sauclovian-g]

Hrm, it doesn't work in the CI (the test that fails is the one that makes sure that non-ascii identifiers work)... I expect this is some kind of locale settings issue.

[sauclovian-g]

Ok, the conclusion from that is that it thinks the default input encoding is ascii and (thus unsurprisingly) forcing read as utf-8 makes the unicode test work. (The extra print I added made assorted other things fail, which isn't important.)

(Edit for clarity: the GitHub UI has dropped the fact that I pushed a test commit at this point and reverted it later.)

[sauclovian-g]

So... given #825, why is anything working this way?

[RyanGlScott]

That is quite baffling, as (AFAIU) GitHub Actions' Ubuntu runners should default to UTF-8. I've confirmed that this is the case when I try printing the locale information in a minimal GitHub Actions workflow, as seen in this CI job:

Locale-derived encoding is UTF-8
Just UTF-8
Just UTF-8
Just UTF-8
Just UTF-8
import "Test.cry";

// we should be able to refer to non-ascii identifiers in imported Cryptol
let pi = {{ π }};

// and we should be able to have our own non-ascii identifiers too
let lá = true;

UTF-8 as far as the eye can see. So why is SAW's integration test CI workflow using ASCII instead? Honestly, I'm really not quite sure... perhaps an earlier step in the job is changing the locale from UTF-8 to ASCII for some reason? (We could try printing out the values of the LANG/LC_ALL environment variables at various steps in the integration_tests job to see if it changes at some point.)

Alternatively, we might consider adopting a policy of always using UTF-8 here. We could do so by defining LANG/LC_ALL to be UTF-8 in the workflow itself (although I worry something might be overriding this somewhere). We could also set the locale from within SAW itself, as suggested in #825 (comment). I don't have a strong opinion on this, so I'm open to your thoughts.

[weaversa]

That is quite baffling, as (AFAIU) GitHub Actions' Ubuntu runners should default to UTF-8. I've confirmed that this is the case when I try printing the locale information in a minimal GitHub Actions workflow, as seen in this CI job:

Locale-derived encoding is UTF-8
Just UTF-8
Just UTF-8
Just UTF-8
Just UTF-8
import "Test.cry";

// we should be able to refer to non-ascii identifiers in imported Cryptol
let pi = {{ π }};

// and we should be able to have our own non-ascii identifiers too
let lá = true;

UTF-8 as far as the eye can see. So why is SAW's integration test CI workflow using ASCII instead? Honestly, I'm really not quite sure... perhaps an earlier step in the job is changing the locale from UTF-8 to ASCII for some reason? (We could try printing out the values of the LANG/LC_ALL environment variables at various steps in the integration_tests job to see if it changes at some point.)

Alternatively, we might consider adopting a policy of always using UTF-8 here. We could do so by defining LANG/LC_ALL to be UTF-8 in the workflow itself (although I worry something might be overriding this somewhere). We could also set the locale from within SAW itself, as suggested in #825 (comment). I don't have a strong opinion on this, so I'm open to your thoughts.

Would the latin-1 work here explain the issue? -- https://github.com/GaloisInc/cryptol/pull/1541/files

[RyanGlScott]

I don't think so. GaloisInc/cryptol#1541 is about ensuring that string values in the Cryptol remote API are encoded as Latin-1 so that they can be represented as valid Cryptol strings (see GaloisInc/cryptol#863). That is an entirely separate issue from what is observed here, which is about the locale that is inherited from the CI environment (and therefore affects how SAW parses things). This part of SAW is entirely independent of Cryptol.

[sauclovian-g]

We still don't know what's going on, but it seems that Cryptol sets the encoding explicitly to UTF-8 as the first thing in its main: https://github.com/GaloisInc/cryptol/blob/9e50047c1c13a1d09bb6d294820e4eb82d902a9b/cryptol/Main.hs#L235 and the conclusion so far is that we should probably do the same in SAW for behavioral consistency. That should also make the CI behave itself.

Meanwhile re #825 it seems that the probable trigger there is printing the SAW banner logo, which the CI doesn't ever do (maybe it should... that's for some other day) so it doesn't hit the problem.

So I'm going to revert my test-push (and force-push it out of existence), then push a patch to set the encoding, and with luck that'll pass the CI and we can move on.