## Stream: general

### Topic: silent overflow

#### Kevin Buzzard (Apr 09 2018 at 16:00):

#check id -- all seems fine

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

#check id -- all still seems fine

#### Kevin Buzzard (Apr 09 2018 at 16:00):

changing example to theorem X shows that there is a problem

#### Kevin Buzzard (Apr 09 2018 at 16:00):

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

#### Kevin Buzzard (Apr 09 2018 at 16:01):

but the error is not triggered if we use example

#### Kenny Lau (Apr 09 2018 at 16:02):

no error reported!

#### Kevin Buzzard (Apr 09 2018 at 16:02):

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

#### Kevin Buzzard (Apr 09 2018 at 16:02):

and perhaps this is relevant

#### Kevin Buzzard (Apr 09 2018 at 16:02):

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

#### Kevin Buzzard (Apr 09 2018 at 16:03):

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

#### Kevin Buzzard (Apr 09 2018 at 16:03):

but it's hard to work with

#### Kevin Buzzard (Apr 09 2018 at 16:03):

I guess proving 1000000 = 123456 is just as good

#### Kevin Buzzard (Apr 09 2018 at 16:03):

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

#### Kevin Buzzard (Apr 09 2018 at 16:09):

buzzard@bob:~$more wrong.lean example : 1000 * 1000 = 123456 := rfl -- no error reported buzzard@bob:~$ lean --trust=0 wrong.lean
buzzard@bob:~$#### Kevin Buzzard (Apr 09 2018 at 16:10): looks good to me #### Kevin Buzzard (Apr 09 2018 at 16:16): dammit example : 0 = 1 := @nat.add_left_cancel (1000 * 1000) 0 1 rfl doesn't work :-( #### Kevin Buzzard (Apr 09 2018 at 16:16): you get the recursion error #### Kevin Buzzard (Apr 09 2018 at 16:26): 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 (Apr 09 2018 at 16:26): so near and yet so far #### Kevin Buzzard (Apr 09 2018 at 16:27): " As far as we know, no proof of false has ever been accepted by Lean when using -t0. " (from the FAQ) #### Kenny Lau (Apr 09 2018 at 16:27): who is -t0? #### Kevin Buzzard (Apr 09 2018 at 16:27): same as --trust 0 #### Kevin Buzzard (Apr 09 2018 at 16:27): "trust no-one" #### Kevin Buzzard (Apr 09 2018 at 16:28): 0 means do not trust any macro, and type check all imported modules #### Kevin Buzzard (Apr 09 2018 at 16:29): 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 (Apr 09 2018 at 16:29): well, AFAIK it's false #### Gabriel Ebner (Apr 09 2018 at 16:41): 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 (Apr 09 2018 at 16:42): ooh #### Kevin Buzzard (Apr 09 2018 at 16:42): so maybe there's a problem with my set-up #### Kevin Buzzard (Apr 09 2018 at 16:42):$ lean --version
Lean (version 3.3.1, nightly-2018-04-06, commit 8f55ec4c5037, Release)

Ubuntu 16.04

#### Kevin Buzzard (Apr 09 2018 at 16:42):

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

#### Sebastian Ullrich (Apr 09 2018 at 16:43):

I can reproduce the issue

#### Gabriel Ebner (Apr 09 2018 at 16:43):

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

#### Sebastian Ullrich (Apr 09 2018 at 16:44):

...using my git build :)

#### Kevin Buzzard (Apr 09 2018 at 16:44):

Let me know if you want me to open an issue

#### Sebastian Ullrich (Apr 09 2018 at 16:45):

...in release mode, could be relevant

#### Gabriel Ebner (Apr 09 2018 at 16:45):

I'm always running relwithdebinfo.

#### Sebastian Ullrich (Apr 09 2018 at 17:08):

@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 (Apr 09 2018 at 17:12):

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

#### Gabriel Ebner (Apr 09 2018 at 17:14):

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 (Apr 09 2018 at 17:16):

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

#### Gabriel Ebner (Apr 09 2018 at 17:16):

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 (Apr 09 2018 at 17:17):

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

#### Gabriel Ebner (Apr 09 2018 at 17:19):

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 (Apr 09 2018 at 17:20):

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 (Apr 09 2018 at 17:21):

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 (Apr 09 2018 at 17:30):

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 (Apr 09 2018 at 17:30):

We could do the same

Last updated: May 14 2021 at 03:27 UTC