CRLF in string literals

Stream: lean4

[Kyle Miller]

Could someone who uses Windows open up VS Code, create a new Lean file, and check the following?

First:
Mario Carneiro said:

Quick question for any windows users: are .lean files using CRLF or LF most of the time? (It says one of the two in the bottom right when the lean file is open.)

Second, if it's CRLF, does this print 1 or 2 for you?

#eval "
".length

[Sebastien Gouezel]

It was LF by default for me (and the answer to your code block was 1). I switched by hand to CRLF, and now the answer is 2.

[Kyle Miller]

Thanks -- that's good to have confirmation that CRLF mode does make a length-2 string.

I'm only curious now if there are any Windows users out there that work with Lean in CRLF mode.

[Kyle Miller]

I wonder if we should follow Rust's lead here (issue and PR) and normalize CRLF -> LF when reading Lean files?

I see Lake already has such a normalization function (docs#Lake.crlf2lf) that's used when computing file hashes. Maybe there could be an alternative to IO.FS.readFile that does CRLF -> LF normalization that the Lean frontend uses.

In addition to making the #eval example above always output 1, this would help in, for example, #guard_msgs in std, where docstrings are compared to generated output. It turns out it doesn't handle files in CRLF mode, but if the docstring were pre-translated to normalize to LF's (along with the rest of the file) then it would just work.

[Sebastian Ullrich]

FileMap.ofString would probably be a good point in the pipeline to do this transformation