VS Code terminal popping up

Stream: new members

[Casper Putz]

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?

[Rob Lewis]

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

[Casper Putz]

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)

[Casper Putz]

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.

[Rob Lewis]

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.

[Casper Putz]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Casper Putz]

Yes it was while writing a structure

[Casper Putz]

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

[Rob Lewis]

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.