lake errors

Stream: general

[Bolton Bailey]

I ran into this while trying to get duper to run. I'm not sure exactly what's going on, but it seems like lake should not throw an error and then tell me to rerun the same command.

boltonbailey@starlight drafting % lake update duper
warning: drafting: package 'Duper' was required as 'duper'
mathlib: running post-update hooks
error: dependency 'duper' not in manifest; use `lake update duper` to add it
error: mathlib: failed to fetch cache
boltonbailey@starlight drafting % lake update duper
warning: drafting: package 'Duper' was required as 'duper'
mathlib: running post-update hooks
error: dependency 'duper' not in manifest; use `lake update duper` to add it
error: mathlib: failed to fetch cache
boltonbailey@starlight drafting %

[Jon Eugster]

Does lake update -R Duper help?

[Jon Eugster]

or actually, is it that you just need to write require Duper ... instead of require duper ...?

[Bolton Bailey]

Jon Eugster said:

or actually, is it that you just need to write require Duper ... instead of require duper ...?

Yes, that seems to have fixed it :thanks:

[Bolton Bailey]

Nevertheless, I still think that the error message here just can't be right, so I think that should be fixed too, if it's not too hard.

[Jon Eugster]

Bolton Bailey said:

Nevertheless, I still think that the error message here just can't be right, so I think that should be fixed too, if it's not too hard.

absolutely. But at least the first line is a warning saying something useful:

warning: drafting: package 'Duper' was required as 'duper'

[Bolton Bailey]

Hmm yeah ok, perhaps I would have gotten it from that if I were a bit more experienced with lake.

[Mario Carneiro]

cc: @Mac Malone

[Mac Malone]

@Mario Carneiro I am not quite sure how to fix this. I guess the warning should just be an error?

[Mario Carneiro]

the warning message could be a bit more explicit about what went wrong and how to fix it

[Mac Malone]

Regardless, @Bolton Bailey would you mind making this an issue on leanprover/lean4?

[Mario Carneiro]

package 'X' was required as 'Y' makes sense in hindsight but it is hard to interpret for someone who does not know the lake DSL

[Mac Malone]

@Mario Carneiro If you want to PR a fix, I'd appreciate it.

[Mario Carneiro]

do we have multiline string literals yet?

[Kim Morrison]

Coming tomorrow. :-)

[Mac Malone]

@Mario Carneiro We have string gaps now (lean4#2821), but I honestly find string appending prettier than that. Escaping an invisible character feels icky and can easily be broken by accidental trailing whitespace (though the lean core does have a VSCode setting to help avoid this).

[Mario Carneiro]

there is no accidental trailing whitespace in any of the lean related repos

[Mario Carneiro]

I forget where we landed on spaces after the \, but both possible behaviors I can think of (ignoring it and erroring) are not error-prone

[Kim Morrison]

And as I've suggested before, I think lake init should ensure everyone in the Lean world gets to enjoy no trailing whitespace. :-)

[Mac Malone]

I know. The principle and aesthetic of the matter just bugs me. I much prefer heredoc/YAML style multiline indents.

[Mac Malone]

(The principle bugs me because it a writing it just always induces a little stress until I remember that the accidental whitespace is solved by something else.)

[Mario Carneiro]

Surely it's better than the current hackaround of using

s!"foo\n{
  ""}bar"

[Mario Carneiro]

I see though that in lake you are using multiple s!"foo" ++ s!"bar" instead

[Mac Malone]

I also dislike it from a pedagogical point-of-view, as code with it requires ensuring students have an understanding of newlines and control characters, which may easily be more advanced than the current topic.

[Mario Carneiro]

I find this to be a dubious argument

[Mario Carneiro]

You are going to have to understand what \ does if you want to write a string literal containing any nonprintable characters

[Mac Malone]

From personal experience, I know when I learned of heredocs I indenting I intuitively understood it. Learning newline escapes in C took a bit of thinking to wrap my head around.

[Mario Carneiro]

I mean, string literals already exist with the backslash stuff

[Mario Carneiro]

And I don't know of any language that uses only heredocs without also having a backslash-based string literal syntax

[Mac Malone]

Mario Carneiro said:

You are going to have to understand what \ does if you want to write a string literal containing any nonprintable characters

\n is a very different beast from \<newline>. The latter is much more similar to \" or \\, the later of which is not what (at least) my mind goes to when thinking of control characters.

[Mario Carneiro]

I first learned about this escape in the context of C macros, and I always conceptualized it as "\ at the end of a line", not "\<newline>"

[Mac Malone]

Well, I guess we acquired different mental models?

[Mario Carneiro]

which isn't even entirely correct because <newline> could be a CRLF (or possibly some trailing whitespace and then a newline, depending on the details)

[Mac Malone]

crlf is a <newline>.

[Mac Malone]

Does C allow trailing whitespace after \?

[Mario Carneiro]

I don't think so

[Mac Malone]

Okay, now I am confused by what you just said then.

[Mario Carneiro]

actually no it is accepted with a warning

[Mario Carneiro]

in gcc at least

[Mario Carneiro]

rust gives an uncharacteristically unhelpful error:

error: unknown character escape: ` `
  --> <source>:10:18
   |
10 |    let x = "foo\
   |                  ^ unknown character escape
   |
   = help: for more information, visit <https://doc.rust-lang.org/reference/tokens.html#literals>
help: if you meant to write a literal backslash (perhaps escaping in a regular expression), consider a raw string literal
   |
10 ~    let x = r"bar\
11 ~      bar";
   |

[Mario Carneiro]

but like I said, neither erroring about it nor ignoring it (possibly with a warning) is error prone in the sense that you wrote code that produces different behavior than you expect

[Mario Carneiro]

regular multiline strings and heredocs do have this issue though, in that the existence of trailing whitespace can change the behavior of the program

[Mac Malone]

Apparently, accepting trailing whitespace is a C++23 feature

[Mac Malone]

The warning is thus nonstandard (pre-C++23)

[Mario Carneiro]

No I think that's what makes the warning standard

[Mario Carneiro]

presumably it's an error and not a warning on earlier C's

[Mac Malone]

Well, now. But what I had previously understood was the standard until literally this year.

[Mario Carneiro]

also I just did a C test not C++

[Mario Carneiro]

Like I said, I also understood that whitespace is not allowed after \ in C

[Mac Malone]

Mario Carneiro said:

presumably it's an error and not a warning on earlier C's

No, \ is a valid preprocessor token

[Mario Carneiro]

and a lot of C "warnings" are actually errors that are somehow forced not to be errors by some convoluted process involving backwards compatibility and standard compliance

[Mac Malone]

One of the reasons I believe I was confident of this was that I believe I have been burned by improper newline backslashing in a macro before (i.e., some of the code did not end up in the macro as expected, but was treated as a separate declaration and this took me a while to figure out).

[Mac Malone]

However, this is a vague feeling. I do not remeber a concrete example, so I could be imagining it.

[Mario Carneiro]

true, it is error prone to leave out the backslash if multiline strings are accepted

[Mac Malone]

And Lean does accept multiline strings.

[Mario Carneiro]

maybe there could be a warning if you mix backslash newlines and explicit newlines?

[Mac Malone]

That sounds like a good idea to me.

[Mac Malone]

Mario Carneiro said:

regular multiline strings and heredocs do have this issue though, in that the existence of trailing whitespace can change the behavior of the program

Yes, but the change is just to insert trailing whitespace into the string, which is usually much less suprising and more easily diagnosable.

[Mario Carneiro]

it is just as difficult to spot as the original error

[Mario Carneiro]

the reason trailing whitespace is banned in most codebases is because it's invisible

[Mac Malone]

Noticing it may be hard, but that is as hard as noticing trailing whitespace in general (and is usually as important as have trailing whitespace in ones program is).

[Mac Malone]

Mario Carneiro said:

the reason trailing whitespace is banned in most codebases is because it's invisible

I think ithe more promenient reason is because it causes suprious Git diffs.

[Mario Carneiro]

there was some case I forget now where there was a genuine use for a trailing whitespace, and people were universally against using it or finding a way to locally disable the trailing whitespace ban

[Mac Malone]

If Git was whitespace insensitive (which it good it isn't, but simply as a hypothesis), I am confident that the precentage of codebases with this rule would be significantly smaller.

[Mario Carneiro]

No, that's even worse, if you have a file with a bunch of random trailing whitespace and a programming language that might be making use of it you never know what you have to pay attention to

[Mac Malone]

However, I do agree the trailing whitespace is undesirable because it is invisible. But, I would argue, that is why string gaps are also displeasing, they operate on an invisible character (the newline).

[Mario Carneiro]

they don't operate on the invisible character

[Mario Carneiro]

I think they should act like the examples shown thus far: either ignore or mandate no trailing whitespace, so in either case you don't have to care or know whether there is any

[Mac Malone]

Yes, they do? As we just demonstrated, C, Rust, and Lean all model the string gap as a newline escape.

[Mac Malone]

(Rust and Lean just makes the alternative behavior an error.)

[Mario Carneiro]

just tested, \ at the end of a file with no newline is also accepted by gcc

[Mac Malone]

@Mario Carneiro This is because the C standard mandates adding a fake newline at the end of the file if one does not exist.

[Mario Carneiro]

although I think files which don't end in a newline are technically UB in the C spec so this is more about what compilers do in practice than what the spec says

[Mario Carneiro]

that page explicitly says "a \ at the end of the line" not "\ followed by a newline"

[Mac Malone]

One note from that specification that reinforces my newline escape model is the a file \<newline> is actually translated to the empty file and then a new newline is added.

[Mario Carneiro]

but I'm not sure why you are pushing for this model if it is also confusing for you?

[Mario Carneiro]

\ at the end of a line is a very visual thing

[Mario Carneiro]

you see a \ with nothing after it

[Mario Carneiro]

and whether that is because there is actually nothing or a LF or CRLF or whitespace and then a CRLF doesn't matter

[Mac Malone]

I do not think of the "end of the line" as a very visual things. The visual end-of-the-line to me is the end of the relevant text area (or piece of paper IRL).

[Mario Carneiro]

you can't play games with

"foo\                       lol not the end
 bar"

because the compiler rejects it

[Mac Malone]

To me, I naturally model a text line as a bunch of whitespace until the end of the text area (which I should note some editors also do -- moving up and down will keep you in the same column and insert trailing whitespace).

[Mac Malone]

@Mario Carneiro Are you talking about Lean?

[Mario Carneiro]

okay, that's fine, \ at the end of the line means a \ with only whitespace in the text area to the right of it in that model

[Mario Carneiro]

I'm talking about all languages with a backslash newline construct of some kind

[Mac Malone]

#define foo bar \ lol not the end definitely works in C.

[Mario Carneiro]

uh, what does it do?

[Mac Malone]

It creates the macro foo which expands to bar \ lol not the end.

[Mario Carneiro]

I see that you are right but I have never encountered that in the wild

[Mario Carneiro]

what is \ as a token?

[Mac Malone]

A preprocessor token?

[Mario Carneiro]

no, you are already past the preprocessor at that point, that's supposed to be C code

[Mario Carneiro]

I don't think \ means anything as a C token

[Mac Malone]

@Mario Carneiro One case I found is that #include directives support macro replacement, so you can use \ in macros and then use the macro as part of #include. More generally, they could be concatenated with other tokens via ## (but it would need to form a valid token, which I am not sure there is one).

[Mario Carneiro]

well in any case I think it's a bit of a distraction, C has all kind of weird things

[Mario Carneiro]

it's not used in practice which is good enough for me

[Mac Malone]

It could create some interesting security exploits, though. :rofl:

[Mario Carneiro]

Mario Carneiro said:

you can't play games with

"foo\                       lol not the end
 bar"

because the compiler rejects it

Maybe you should read this as "any self respecting language would have a compiler that rejects this, because it is easy to detect and prevent this class of bugs/exploits"

[Mac Malone]

I think C is a self-respecting language.

[Mac Malone]

But, I get your point.

[Mario Carneiro]

C is not overly concerned with detection and prevention of bugs

[Mac Malone]

True.

[Mac Malone]

My overal point was that string gaps allow for a \<newline> mental model, which is nerve-racking for the reasons we just described. Thus, I much prefer the heredoc/YAML approach which does not produce (at least in me) such stress.

[Mac Malone]

And I should note, that this is already the model used in docstrings, so applying it to some form of string literal seems reasonable.

[Mario Carneiro]

We don't have heredocs though

[Mario Carneiro]

at least not yet

[Mac Malone]

Yes, I am expressing a future feature request.

[Mario Carneiro]

if you want to propose them then we can talk about whether to prefer one or the other for string literals in code, but right now the option is multiline string literals or string gaps (or appending or other dynamic options, depending on the context)

[Mac Malone]

In my mind:
docstring style > heredoc > string append > string gap

[Mario Carneiro]

but when string gaps land I'm going to try to make them the standard for multiline string literals in std+mathlib

[Mac Malone]

Fair enough.

[Mario Carneiro]

string appending doesn't always work when you have a macro that expects a interpolatedStr

[Mario Carneiro]

it's also higher edit distance to add a line to a single line string

[Mac Malone]

I do agree that string gaps are functionally superior, but they are not aesthetically, which I care more about.

[Mario Carneiro]

docstring style is certainly good but it is also most limited. Lean 3 had a /-" ... "-/ syntax for docstring style string literals

[Mac Malone]

Oh, I love that! That sounds wonderful!