isWhiteSpace breaking the language server

Stream: general

[Alexandre Rademaker]

This is my first attempt to implement the Haskell words in Lean. I would like to avoid the partial, but it was not clear if I could prove termination.

partial def words (s : String) : List String :=
 let rec aux (s : List Char) : List (List Char) :=
   let rs := s.dropWhile (· = ' ')
   if rs == []
   then []
   else let (p, r) := rs.span (· ≠ ' ')
        p :: (aux r)
 List.map List.asString $ aux s.toList

It works as expected

#eval words " hello world  "  -- ["hello", "world"]

but the correct implementation should split the string at any whitespace character, not only a single space. But when I replace (· ≠ ' ') with (fun x => ¬ x.isWhitespace) the Lean Language Server crashes!

Any idea?

[Julian Berman]

What version of Lean are you on?

[Julian Berman]

Here (on 4.10.0-rc2) that replacement works fine

[Julian Berman]

Seems to work in the playground too: https://live.lean-lang.org/#code=partial%20def%20words%20(s%20%3A%20String)%20%3A%20List%20String%20%3A%3D%0A%20let%20rec%20aux%20(s%20%3A%20List%20Char)%20%3A%20List%20(List%20Char)%20%3A%3D%0A%20%20%20let%20rs%20%3A%3D%20s.dropWhile%20(fun%20x%20%3D%3E%20x.isWhitespace)%0A%20%20%20if%20rs%20%3D%3D%20%5B%5D%0A%20%20%20then%20%5B%5D%0A%20%20%20else%20let%20(p%2C%20r)%20%3A%3D%20rs.span%20(fun%20x%20%3D%3E%20%C2%AC%20x.isWhitespace)%0A%20%20%20%20%20%20%20%20p%20%3A%3A%20(aux%20r)%0A%20List.map%20List.asString%20%24%20aux%20s.toList%0A%0A%23check%20words

[Alexandre Rademaker]

% lean -v
Lean (version 4.9.0, arm64-apple-darwin23.5.0, commit 8f9843a4a5fe, Release)

[Alexandre Rademaker]

How can I change to 4.9.0 in the live.lean-lang.org to confirm the error in version 4.9.0? What is the easier way to upgrade to Lean 4.10.0-rc2? Do I need to manually edit the lean-toolchain?

[Alexandre Rademaker]

Same error after updating to Lean 4.10.0-rc2

% uname -a
Darwin tranco.local 23.5.0 Darwin Kernel Version 23.5.0: Wed May  1 20:12:58 PDT 2024; root:xnu-10063.121.3~5/RELEASE_ARM64_T6000 arm64

% lean -v
Lean (version 4.10.0-rc2, arm64-apple-darwin23.5.0, commit 702c31b80712, Release)

% cat lean-toolchain
leanprover/lean4:v4.10.0-rc2

% elan show
installed toolchains
--------------------

leanprover/lean4:nightly-2023-12-31
leanprover/lean4:stable (default)
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.6.0-rc1

active toolchain
----------------

leanprover/lean4:v4.10.0-rc2 (overridden by '/Users/ar/r/emap-20242-nlp/cs/lean-toolchain')
Lean (version 4.10.0-rc2, arm64-apple-darwin23.5.0, commit 702c31b80712, Release)

[Alexandre Rademaker]

I am curious! Maybe the partial is causing the crash because it is not protecting some mysterious behavior? The code below works. Note that the only change was to replace s.dropWhile (· = ' ') with s.dropWhile (fun x => x.isWhitespace)

partial def words (s : String) : List String :=
 let f : Char → Bool := (fun x => x.isWhitespace)
 let rec aux (s : List Char) : List (List Char) :=
   match s.dropWhile f with
   | [] => []
   | s => let (p, r) := s.span (not ∘ f); p :: aux r
 List.map List.asString $ aux s.toList

I am still uncomfortable with the partial! Any advice on how to prove the termination would be welcome!

[Damiano Testa]

I'm not at a computer, but an alternative approach to what you are doing is to use docs#String.splitOn first and then filter out empty lists from the output.

[Damiano Testa]

Btw, I think that String.dropWhile takes a function to Bool as an argument, so I would probably use (\. == ' ') instead of the Prop-valued =.

[Alexandre Rademaker]

The last version does not use ( \. = ' ') but Stgring.isWhitespace! But I got your point, thank you!

I used the String.split method, so I can still split by all whitespace characters and not only spaces. Thank you for pointing this out to me. Indeed, the code is much simpler and more efficient.

 def words₂ (s : String) : List String :=
  s.split (·.isWhitespace) |>.filter (· ≠ "")

Nevertheless, the crash of the server is still unexpected!

[Marc Huisinga]

I also can't reproduce the crash with the steps you described.

Note that not all crashes are necessarily the fault of the language server. If you are running faulty code in the language server (e.g. something that causes a stack overflow), then the process for that file that the faulty code is run in will crash.
It will show you an error of the form "The Lean Server has stopped processing this file." and the next edit you make to the file will automatically attempt to restart the process for that file. If one of your edits fixes the problem, it restarts just fine.

By the way, your code is also causing a stack overflow as soon as you use a non-space whitespace character, which is probably the issue you are seeing here:

partial def words (s : String) : List String :=
 let rec aux (s : List Char) : List (List Char) :=
   let rs := s.dropWhile (· = ' ')
   if rs == []
   then []
   else let (p, r) := rs.span (fun x => ¬ x.isWhitespace)
        p :: (aux r)
 List.map List.asString $ aux s.toList

/-
libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:
#1 words.aux._lambda_1
#2 words.aux._lambda_1._boxed
#3 List.dropWhile._rarg
#4 words.aux
...
-/
#eval words "Hello World\n"

[Alexandre Rademaker]

Yes, later yesterday, I found the bug that was probably producing a stack overflow. As you said, the presence of a whitespace character that is not space would make the code loop forever. But I didn't get this error above. Could you let me know where you saw this error? My screen is below. I didn't see libc++abi: terminating due to...

image.png

The code has a bug, and I fixed it. @Damiano Testa's idea is actually much simpler anyway.

partial def words₁ (s : String) : List String :=
 let f : Char → Bool := (fun x => x.isWhitespace)
 let rec aux (s : List Char) : List (List Char) :=
   match s.dropWhile f with
   | [] => []
   | s => let (p, r) := s.span (not ∘ f); p :: aux r
 List.map List.asString $ aux s.toList

 def words₂ (s : String) : List String :=
  s.split (·.isWhitespace) |>.filter (· ≠ "")

The remaining questions for me are:

1. Is the crash normal -- in a sense of unavoidable if a function does not terminate -- or would it be avoided if the function was not declared partial? Well, the crash was caused by a non-termination, right? So, proof of termination would probably reveal the bug, right?
2. How to prove termination?! This is an interesting case. If I remove the partial, Lean will report the message below. Lean could not detect that the first argument s changes in the recursive call. This makes sense. If s.dropWhile f does not change s and s.span (not ∘ f) can't split the string, an infinite loop will happen. Somehow, I need to show Lean that ∀ c ∈ S, f c ∨ ¬ f c. The principle of excluded middle!

fail to show termination for
  words₁.aux
with errors
structural recursion cannot be used:

argument #1 cannot be used for structural recursion
  it is unchanged in the recursive calls

argument #2 cannot be used for structural recursion
  failed to eliminate recursive application
    words₁.aux f✝ r

[Marc Huisinga]

You can find more detailed output in the troubleshooting output (forall menu in the top right > Troubleshooting: Show Output)

[Marc Huisinga]

Specifically, when the error occurs, you get two notifications:
image.png
The button in the bottom one takes you to the troubleshooting output as well.

VS Code can sometimes decide to hide these notifications if they have not been acted upon for too long or if there are too many notifications, but you can always display all notifications by clicking the notification bell in the bottom right.
image.png

[Alexandre Rademaker]

I found the menu and the notification icon on the top bottom right! Thank you.