Gabriel Ebner

compiz-cms determines whether to color-correct or not on a per-window basis. It is unlikely (but possible) that pipelight opens its own window "in front" of firefox, in this case you...

It is surprisingly hard to disable the PDF plugin in electron: see https://github.com/electron/electron/issues/24334 and https://github.com/electron/electron/issues/24977 The first issue links to a workaround implemented in the min browser: https://github.com/minbrowser/min/commit/42fefc3eb534d819197643bead4f269bd4f8b384

Would you be happy with a PR that adds (something like) the workaround in the min browser? (With a `nopdfplugin` option?) The PDF situation is really annoying me.

AFAICT it won't disable the built-in PDF viewer, but intercepts all responses with content-type `application/pdf` and (in our case) download the file instead. I haven't tried it yet.

> One easy (but weird) fix is to disallow sizeof in compiled code. > @gebner Does it sound reasonable to you? It certainly fixes the problem for now, and having...

> However, users may still experience the failure if they use the recursors generated by the inductive compiler directly. I cannot mark them as forbidden since the instances generated by...

> We would still use the *.cases_on recursors. Yes, but we can use the user-facing cases_on recursor (which is compiled correctly) instead of the internal one. As far as I...

We can do something very close in pure Lean using the `cur_pos` parser: we could use the position *after* the closing brace as the default position. To get the position...

I could not reproduce the bug here. 1. Can you post the output of `lean -p` (in the test directory)? 2. Can you try restarting the lean server?

So `C:\Users\Mario\lean\library/test/{a,b,c}.lean` are the files? Does any of the other directories in the path contain a `test/a.lean` file? (Maybe we pick up the `test.a` import from another directory.)