Can't use #where

Stream: mathlib4

[Yaël Dillies]

What happened to #where? We seem to not be able to use it in mathlib anymore

[Kevin Buzzard]

It's working fine for me in this random file I have open...oh, in the filter game, which is on 4.7 (because lean4game is on 4.7). It was in Std.Tactic.Whereback then.

[Yaël Dillies]

Uh oh, maybe #where fell victim to @Kim Morrison's import reduction?

[Mario Carneiro]

could we maybe upstream tactics like this to batteries?

[Damiano Testa]

This works:

import Batteries.Tactic.Where

#where

so the upstreaming seems to have happened already.

[Damiano Testa]

But then I think that it is only imported in Mathlib/Mathport/Syntax.lean.

[Kyle Miller]

It's been there the whole time (it started in Std). It must have just lost its import in Mathlib.Tactic.Common somehow.

[Kyle Miller]

Huh, it's never been imported in Mathlib.Tactic.Common. Maybe there was a stray import Std somewhere in mathlib that was cleaned up?

[Yaël Dillies]

Yeah, I believe Kim precisely cleaned this up recently

[Kyle Miller]

#15139

[Frédéric Dupuis]

On a related note, I haven't been able to use conv? for a while now. Was it also the victim of that import reduction?

[Kyle Miller]

@Frédéric Dupuis It's imported in Mathlib.Tactic.Common (see import Mathlib.Tactic.Widget.Conv), so I'm not sure why you can't use conv?, unless you're working in some very low level files.

[Frédéric Dupuis]

On current mathlib master:

import Mathlib.Tactic.Widget.Conv

example : 1 + 2 = 3 := by
  conv?
  sorry

I get the error Error: The requested module 'blob:vscode-webview://176jrrsir8dt89g7e8g7qg35rpp6otm44id6t93mjif424eb3aen/efada8ef-24d7-4352-a41b-d1d17181cb08' does not provide an export named 'useRpcSession' in red in the Lean infoview and conv? doesn't do anything.

[Kevin Buzzard]

I don't get any errors with that script on cc495260156b40dcbd55b947c047061e15344000 which is a commit from today. It's also fine on the lean 4 playground.

[Frédéric Dupuis]

Very strange. I've been getting this error on the two computers that I use regularly for some time now.

[Frédéric Dupuis]

The above MWE was on commit 63341a2ea2f7c99ff4315e13c763dca1bfd13d7d, so only
two commits newer than Kevin's.

[Kyle Miller]

Maybe if you delete your .lake folder and get a fresh cache it'll magically start working?

[Kevin Buzzard]

yeah conv? is working fine for me with that code above on 63341a2ea2f7c99ff4315e13c763dca1bfd13d7d, I can shift click, all looks normal.

[Frédéric Dupuis]

Deleting .lake doesn't do anything. The problem appears to be system-wide, I get it in every project I have and every copy of mathlib.

[Daniel Weber]

What's your vscode version?

[Frédéric Dupuis]

Here's what I got from Help -> About:

Version: 1.91.0
Commit: ea1445cc7016315d0f5728f8e8b12a45dc0a7286
Date: 2024-07-03T20:40:42.797Z
Electron: 29.4.3
ElectronBuildId: undefined
Chromium: 122.0.6261.156
Node.js: 20.9.0
V8: 12.2.281.27-electron.0
OS: Linux x64 6.6.38-1-lts

[William DeMeo]

I'm getting the same error message. It seems to appear only when I place the cursor inside a calc proof. @Frédéric Dupuis did you ever figure out why this occurs and/or resolve it?

[Frédéric Dupuis]

No, I never figured it out, and it's still happening right now on mathlib from yesterday.

[Frédéric Dupuis]

OK, I just did figure out: I was using an absolutely antiquated version of the VSCode extension (v0.0.125), despite the fact that "Auto update" was supposedly on.

[Jon Eugster]

So does that mean everything works as expected?

I didn't quite get from @Mario Carneiro's message here whether we messed up something when making the changes to the lakefile about the mathlib-only linters or if it's all fine.

Mario Carneiro said:

This looks kind of wrong... are we sure the lakefile is set up correctly?
[...]
Apparently, weak options are handled by putting things in the Options struct which are not known to be options, meaning that code which handles options now has to be aware of this and deal with undefined options. My point above is that even after doing so, the results suggest that either lean is incorrectly setting the Options struct, or mathlib's lakefile is misconfigured, because I don't think there are supposed to be options literally containing weak.* in them, that's supposed to be a syntax just for the command line parser AFAIK

[Filippo A. E. Nuccio]

(deleted)