New member question about possible bugs

Stream: lean4

[Ioannis Konstantoulas]

Hello all; I am trying Lean right now in my Linux box, and encountered two unexpected crashes while compiling lean code from the tutorial. I hope this is the right place to ask about them; if not, please direct me to the appropriate place! My system is a latest Arch Linux build, and the lean version is Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

Both crashes are in sample code from Functional Programming in Lean.

The first problem comes from Section 2.4 (Worked Example : cat) where the Lean version of cat, named feline, is implemented. It is supposed to be a simple version of cat that can nevertheless read infinite streams.

However, when I run it with an infinite stream, I get a Lean error

# works fine
$ lean --run feline.Lean <( echo 'hello!' )
hello!

#crashes
$ lean --run feline.Lean /dev/urandom | head -c 100 | tr -dc '[:alnum:]'
uncaught exception: resource vanished (error code: 32, broken pipe)

I have been unable to pipe any infinite stream into the feline program successfully; I always get non-zero exit code and the above message.

The second problem I encountered was at the end of the interlude. We have the Lean function showFifth:

def showFifth (inp : List α) (ev : inp.length > 5) : α := inp[5]

which carries evidence of soundness in its second argument, and can be carried out by simp. I expected calling this function with a non-compliant input to cause Lean to reject the line; instead, however, I get a segfault in the command line, and vscode reports Lean server crash:

def showFifth (inp : List α) (ev : inp.length > 5) : α := inp[5]
#eval showFifth [1, 2] (by simp)

$ lean --run Main.lean
[1]    26700 segmentation fault (core dumped)  lean --run Main.lean

Lake building reports:

$ lake build
Building Main
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/user/.elan/toolchains/leanprover--lean4---stable/lib:./build/lib /home/user/.elan/toolchains/leanprover--lean4---stable/bin/lean ./././Main.lean -R ././. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c
error: external command `/home/user/.elan/toolchains/leanprover--lean4---stable/bin/lean` exited with code 139

I am not sure if this is supposed to be the result of evaluating on an invalid input, or it is indeed a bug.

Can someone who knows more give me some directions?

[Sebastian Ullrich]

The second issue is https://github.com/leanprover/lean4/issues/1697. The first one is new to me, but you could very well be the first one exercising it.

[Ioannis Konstantoulas]

Sebastian Ullrich said:

The second issue is https://github.com/leanprover/lean4/issues/1697. The first one is new to me, but you could very well be the first one exercising it.

Oh, I see there is a github page for lean; I will look there if my first problem is a known issue and if not, I will try opening one.

[Ioannis Konstantoulas]

OK, I see one possibly related issue in the github repo, Issue #349, but it does not address the present situation. I have opened a new issue to study the possible bug: https://github.com/leanprover/lean4/issues/2013