Line wrapping strings without inserting `\n`

Stream: general

[Eric Wieser]

How can I split a long string literal to make the linter happy, without inserting \n into its value?

#check "hello
world" -- contains \n, which I don't want

[Eric Wieser]

Is there a more idiomatic way than docs#string.join?

#eval string.join ["hello ",
  "world"]

[Mario Carneiro]

I would just use that, or ++

[Mario Carneiro]

If you really care about the expression being a single string, you can use a tactic to process it

[Johan Commelin]

Do you need a tactic? Can't you just filter \n out of the string?

[Mario Carneiro]

def foo :=
by do
  let s := "" ++
    "abc" ++
    "def",
  tactic.exact $ reflect s

#print foo

[Mario Carneiro]

Note that this gives the same definition as def foo := "abcdef", while

def foo :=
"abc" ++
"def"

#print foo

yields def foo := "abc" ++ "def"

[Floris van Doorn]

I think string literals (and URLs) should be allowed exceptions to the style linter.

[Johan Commelin]

URLs are already getting a pass

[Gabriel Ebner]

What is the use case for excessively long string literals?

[Floris van Doorn]

Typically error messages, for example some of the lines in src#simps_add_projections.

[Kyle Miller]

This is a kind of nice Haskell feature: http://book.realworldhaskell.org/read/characters-strings-and-escaping-rules.html#id689881

It would let you write

example : string := "hello \
                    \world"

[Mario Carneiro]

@Floris van Doorn But those have newlines in them

[Floris van Doorn]

Yes, but still some lines are too long, and I don't really want to split them up further.

[Gabriel Ebner]

The error messages shouldn't be longer than 100 characters per lines either. You should really split them up.

[Eric Wieser]

The context of this thread was actually an error message

[Eric Wieser]

But even if the error message is limited to 100 chars, I don't want it to inherit the indentation of my lean code. ++ was the right solution for me.

[Kyle Miller]

This is too horrible to contemplate for more than a moment or two, but you can use coercions to have Lean support C-style string literal concatenation:

instance : has_coe_to_fun string :=
{ F := λ _, string -> string,
  coe := λ s t, s ++ t }

def foo : string := "hello "
  "world"

[Yakov Pechersky]

instance : has_coe_to_fun string :=
{ F := λ _, string -> string,
  coe := λ s t, s ++ t }

def foo : string := "hello "
  "world"

#eval
  ("a" "l" "l" " " "w" "o" "r" "k" " " "a" "n" "d" " " "n" "o" " " "p" "l" "a" "y" " ")^[100] " "

[Yakov Pechersky]

Surprisingly fast up to 1e4 iterations; 1e5 is not.

[Huỳnh Trần Khanh]

after all this is O(n^2) so not surprising :joy:

[Huỳnh Trần Khanh]

https://codeforces.com/blog/entry/21772?#comment-264557

[Huỳnh Trần Khanh]

welp the <= 10k part is wrong

[Huỳnh Trần Khanh]

it's supposed to read O(nsqrt(n))