silent overflow

Stream: general

[Kevin Buzzard]

#check id -- all seems fine

example : 1000 * 1000 = 123456 := rfl -- no error reported

#check id -- all still seems fine

[Kevin Buzzard]

changing example to theorem X shows that there is a problem

[Kevin Buzzard]

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

[Kevin Buzzard]

but the error is not triggered if we use example

[Kenny Lau]

no error reported!

[Kevin Buzzard]

Changing example to theorem also gives us the not a rfl-lemma, even though marked as rfl error

[Kevin Buzzard]

and perhaps this is relevant

[Kevin Buzzard]

because example : 1000 * 1000 = 123456 := by refl gives the recursion error

[Kevin Buzzard]

no error reported! So maybe we can prove 0=1

[Kevin Buzzard]

but it's hard to work with

[Kevin Buzzard]

I guess proving 1000000 = 123456 is just as good

[Kevin Buzzard]

Do you know how to run this through Lean with max paranoia options on?

[Kevin Buzzard]

buzzard@bob:~$ more wrong.lean
example : 1000 * 1000 = 123456 := rfl -- no error reported
buzzard@bob:~$ lean --trust=0 wrong.lean
buzzard@bob:~$

[Kevin Buzzard]

looks good to me

[Kevin Buzzard]

dammit example : 0 = 1 := @nat.add_left_cancel (1000 * 1000) 0 1 rfl doesn't work :-(

[Kevin Buzzard]

you get the recursion error

[Kevin Buzzard]

theorem W : 0 = 1 → false := dec_trivial

theorem X : 1000 * 1000 + 0 = 1000 * 1000 + 1 → false := λ H, W (nat.add_left_cancel H)

example : 1000 * 1000 + 0 = 1000 * 1000 + 1 := rfl -- no problem

example : false := X rfl -- recursion error

[Kevin Buzzard]

so near and yet so far

[Kevin Buzzard]

" As far as we know, no proof of false has ever been accepted by Lean when using -t0. " (from the FAQ)

[Kenny Lau]

who is -t0?

[Kevin Buzzard]

same as --trust 0

[Kevin Buzzard]

"trust no-one"

[Kevin Buzzard]

0 means do not trust any macro, and type check all imported modules

[Kevin Buzzard]

My session earlier had Lean accepting wrong.lean even at -t0 but it's not a proof of false, it's just a proof of something which is false :-)

[Kevin Buzzard]

well, AFAIK it's false

[Gabriel Ebner]

This would be really awesome, but I get an error:

type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  1000 * 1000 + 0 = 1000 * 1000 + 1

[Kevin Buzzard]

ooh

[Kevin Buzzard]

so maybe there's a problem with my set-up

[Kevin Buzzard]

$ lean --version
Lean (version 3.3.1, nightly-2018-04-06, commit 8f55ec4c5037, Release)

[Kevin Buzzard]

Ubuntu 16.04

[Kevin Buzzard]

mathlib HEAD

[Kevin Buzzard]

Nothing to do with VS Code because I can reproduce on the command line

[Sebastian Ullrich]

I can reproduce the issue

[Gabriel Ebner]

I now see it with the nightly as well, but not with my git build from master..

[Sebastian Ullrich]

...using my git build :)

[Kevin Buzzard]

Let me know if you want me to open an issue

[Sebastian Ullrich]

...in release mode, could be relevant

[Gabriel Ebner]

I'm always running relwithdebinfo.

[Sebastian Ullrich]

@Gabriel Ebner Some initial observations:
1) the exception is not reported by check_example because stack_space_exception is not a lean::exception
2) It's then caught by task_queue::execute but never reported, apparently

[Gabriel Ebner]

Yeah, task_queue::execute doesn't report errors.

[Gabriel Ebner]

I guess we should catch all exceptions in check_example to be consistent with add in module.cpp.

[Gabriel Ebner]

I can now reproduce the error as well. It just takes a slightly larger number:

example : 1000*1000*100 + 0 = 1000*1000*100 + 1 := rfl -- no problem

[Sebastian Ullrich]

Surely we should try and report the caught exception at some point...?

[Gabriel Ebner]

Yes, in check_example. We just need to add std:: in front of the exception, and add a second catch-all ... case like in add.

[Sebastian Ullrich]

That too, but the task_queue shouldn't just swallow exceptions silently

[Gabriel Ebner]

Mmh, good point. At least some debugging output on stderr would be good. For exceptions inheriting std::exception we can even print the error message.

[Gabriel Ebner]

That won't work, many tasks end in an exceptional state. And these exceptions are eventually reported. We wouldn't want to print something to stderr for every red squiggle the user sees.

[Gabriel Ebner]

This is similar to the failed promise issue in javascript. There, a promise can also fail without throwing an exception or printing anything, you only get notified of the error if you listen to it.

[Sebastian Ullrich]

In the sane promise APIs I know, not extracting the exception will make the promise throw it in its destructor. Which may kill the process if the exception is not caught in a background thread.

[Sebastian Ullrich]

We could do the same