Zulip Chat Archive

Stream: general

Topic: silent overflow


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:00):

changing example to theorem X shows that there is a problem

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:00):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:01):

but the error is not triggered if we use example

view this post on Zulip Kenny Lau (Apr 09 2018 at 16:02):

no error reported!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:02):

and perhaps this is relevant

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:02):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:03):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:03):

but it's hard to work with

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:03):

I guess proving 1000000 = 123456 is just as good

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:03):

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

view this post on Zulip 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:~$

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:10):

looks good to me

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:16):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:16):

you get the recursion error

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:26):

so near and yet so far

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 09 2018 at 16:27):

who is -t0?

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:27):

same as --trust 0

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:27):

"trust no-one"

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:28):

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

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:29):

well, AFAIK it's false

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

ooh

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

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

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

Ubuntu 16.04

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

mathlib HEAD

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:42):

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

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 16:43):

I can reproduce the issue

view this post on Zulip 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..

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 16:44):

...using my git build :)

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 16:44):

Let me know if you want me to open an issue

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 16:45):

...in release mode, could be relevant

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 16:45):

I'm always running relwithdebinfo.

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 17:10):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 17:16):

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

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 17:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Apr 09 2018 at 17:30):

We could do the same


Last updated: May 14 2021 at 03:27 UTC