Zulip Chat Archive

Stream: new members

Topic: VS Code terminal popping up


view this post on Zulip Casper Putz (Jan 23 2019 at 20:28):

When typing in VS Code I constantly have the terminal window popping up with all error messages. It makes it impossible to work... I had this problem before and cannot remember how to fix it. Does anybody know how to fix this?

view this post on Zulip Rob Lewis (Jan 23 2019 at 21:28):

I've never seen this, what are the error messages?

view this post on Zulip Casper Putz (Jan 23 2019 at 21:47):

When you type the Output terminal with lean error messages pops up (if it was closed) and the cursor moves to the terminal. The terminal contains a bunch of these messages (they are all the same):
LEAN ASSERTION VIOLATION File: /home/travis/build/leanprover/lean/src/frontends/lean/elaborator.cpp Line: 3167 Task: /home/cp/Git/finite_fields/src/finite_field.lean: zmod_ring_hom m_ctx.match(e, *val2)

view this post on Zulip Casper Putz (Jan 23 2019 at 21:48):

I now changed this function zmod_ring_hom and now I dont get the problem anymore, nor can I recreate it... If I get it again I will let you know.

view this post on Zulip Rob Lewis (Jan 23 2019 at 21:49):

Well, assertion violations are probably bad, but ignoring that. Are you using a debug version of Lean? (lean --v will tell you.) I thought assertions are only checked in debug.

view this post on Zulip Casper Putz (Jan 23 2019 at 21:53):

Nope Release: Lean (version 3.4.2, nightly-2018-08-23, commit b13ac127fd83, Release).
Can the problem be 3.4.2?

view this post on Zulip Patrick Massot (Jan 23 2019 at 21:54):

At some point in the past, everybody was seeing assertion violations. But then they disappeared (for me)

view this post on Zulip Patrick Massot (Jan 23 2019 at 21:55):

You only need to search for "assertion violation" on this zulip. No need to run a debug version

view this post on Zulip Scott Morrison (Jan 23 2019 at 21:55):

I still see them occasionally, but have not tried to pin one down for a while.

view this post on Zulip Scott Morrison (Jan 23 2019 at 21:56):

Usually they occur when working with half-written structures, with weird syntax violations.

view this post on Zulip Casper Putz (Jan 23 2019 at 21:57):

Yes it was while writing a structure

view this post on Zulip Casper Putz (Jan 23 2019 at 21:57):

Then I just hope that it just does not happen again haha

view this post on Zulip Rob Lewis (Jan 23 2019 at 22:03):

Ah, it looks like there are two levels of assertions, most of them are only checked in debug mode but some are checked in release.


Last updated: May 13 2021 at 06:15 UTC