Build fails

Stream: batteries

[Marcus Rossel]

I'm trying to build batteries and it always fails at:

error: ././././Batteries/CodeAction/Misc.lean:317:8: function expected at
  ' '
term has type
  Char

It's the same for v4.12.0 and v4.13.0-rc3. Is this expected?

[Mario Carneiro]

which version?

[Mario Carneiro]

There is nothing at that position of that file so I am suspicious of the provenance of your installation

[Ruben Van de Velde]

You should in any case be using the version listed in the lean-toolchain for the version of batteries you're using: https://github.com/leanprover-community/batteries/blob/main/lean-toolchain

[Mario Carneiro]

Actually there has never in the history of batteries been a token at position 317:8, at least while it had the name Batteries/CodeAction/Misc.lean

[Mario Carneiro]

There is an occurrence of ' ' a few lines up so perhaps the signature of String.pushn is wrong?

[Marcus Rossel]

Ahhhh, I think it's because I was incorrectly cating that file and didn't notice. Or somewhere along the line the \n turned into a newline.

[Mario Carneiro]

wait what? How did cat get involved in the pipeline here

[Marcus Rossel]

Mario Carneiro said:

wait what? How did cat get involved in the pipeline here

Only because of my personal use case. I just didn't notice that that was still happening.

[Mario Carneiro]

Oh, you are right, replacing the line with

        let indent := "
".pushn ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1

causes exactly the error you reported

[Marcus Rossel]

Yeah, sorry for the noise.

[Mario Carneiro]

This by the way is an exceedingly weird interpretation on lean's part:

• The expression

        let indent := "
".pushn

interprets the literal ... literally, so you end up with let indent := "\n".pushn, which is defining indent to be a partially applied function

• Between the pushn and ' ' is a space, but it can't be an application because it appears to the left of the let, which was set as the withPosition mark in the enclosing do block
• However, the character literal happens to perfectly line up with the let, so ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1 is interpreted as the next doElem in the sequence, which fails because ' ' is not a function

[Mario Carneiro]

this seems like abuse of the offside rule

[Mario Carneiro]

well this is entertaining:

example : Id Nat := do
    let x := 1
  - let x := 2
  x let x := x
    pure x

all the x's are used exactly once, can you figure out which is which?