v4.9.0-rc1 discussion

Stream: general

[François G. Dorais]

The following code

def getHexDigit? (char : Char) : Option (Fin 16) :=
  if char.toNat < 0x0030 then
    none
  else
    let n := if char.toNat < 0xFF10 then char.toNat - 0x0030 else char.toNat - 0xFF10
    if h : n < 10 then
      some ⟨n, Nat.lt_trans h (by decide)⟩
    else if n >= 17 then
      let n := n - 7
      if h : n < 16 then
        some ⟨n, h⟩
      else if n >= 32 then
        let n := n - 32
        if h : n < 16 then
          some ⟨n, h⟩
        else
          none
      else
        none
    else
      none

gives me (kernel) declaration has free variables 'Unicode.getHexDigit?'. This is fixed by removing the second or the third let. Not sure what's going on here.

[Joachim Breitner]

Looks like a plain bug to me, maybe you can report it ay the lean issue tracker.

[François G. Dorais]

I couldn't minimize much more. I submitted a report lean4#4375

[Floris van Doorn]

When updating Mathlib to the latest version (or a project depending on Mathlib) and trying to get the cache, I get an error when compiling the file Cache.IO to a C-file on a Windows laptop.

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ lake update
error: .\.lake\packages\mathlib\lakefile.lean:86:2: error: unknown attribute [test_driver]
error: .\.lake\packages\mathlib\lakefile.lean: package configuration has errors
mathlib: updating repository '.\.lake\packages\mathlib' to revision '678f4912899df76cc45934a56bdf929ffe3cac50'

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ cp .lake/packages/mathlib/lean-toolchain .

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ lake update
info: downloading component 'lean'
info: installing component 'lean'
✔ [1/10] Fetched proofwidgets:optRelease
✔ [2/10] Built Cache.IO
✔ [3/10] Built Cache.Hashing
✖ [4/10] Building Cache.IO:c.o
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe' exited with code 1
✖ [5/10] Building Cache.Hashing:c.o
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe' exited with code 1
✔ [6/10] Built Cache.Requests
✖ [7/10] Building Cache.Requests:c.o
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe' exited with code 1
✔ [8/10] Built Cache.Main
✖ [9/10] Building Cache.Main:c.o
trace: .> c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.9.0-rc1\bin\leanc.exe' exited with code 1
Some builds logged failures:
- Cache.IO:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o
- Cache.Main:c.o
error: build failed
info: batteries: updating repository '.\.\.lake\packages\batteries' to revision 'af2dda22771c59db026c48ac0aabc73b72b7a4de'
info: Qq: updating repository '.\.\.lake\packages\Qq' to revision '44f57616b0d9b8f9e5606f2c58d01df54840eba7'
info: aesop: updating repository '.\.\.lake\packages\aesop' to revision 'f744aab6fc4e06553464e6ae66730a3b14b8e615'
info: proofwidgets: updating repository '.\.\.lake\packages\proofwidgets' to revision 'e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5'
info: Cli: updating repository '.\.\.lake\packages\Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
info: importGraph: updating repository '.\.\.lake\packages\importGraph' to revision '7983e959f8f4a79313215720de3ef1eca2d6d474'
info: mathlib: running post-update hooks
error: mathlib: failed to fetch cache

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ lean --version
Lean (version 4.9.0-rc1, x86_64-w64-windows-gnu, commit be6c4894e0a6, Release)

[Floris van Doorn]

I get similar errors when running this in powershell, or using the VSCode menu item to get the Mathlib build cache.

[Floris van Doorn]

It looks like a false alarm: I deleted the Lean toolchain and redownloaded it, and it works correctly now.

[Sebastian Ullrich]

Ideally this should not happen with elan 3.1.1+, what version are you using?

[Floris van Doorn]

$ elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

[Sebastian Ullrich]

Thanks, that's disappointing. And we can see in your log that there was no error (or abort) downloading it, so how could it still be corrupted (and even semi-consistently, but only on Windows)? Unfortunately I have no idea.

[Floris van Doorn]

Yeah, that is disappointing, indeed...

[Floris van Doorn]

I added more detailed instructions on how to update Mathlib in downstream projects (including the fact that you have to update the Lean version first): leanprover-community.github.io#487.
I also took the opportunity to add the workaround to this issue to the troubleshooting section.

[Sebastian Ullrich]

I assume that leanc.exe really is just missing but it would be great to have a directory listing/diff from a broken toolchain. Or even some reproduction guidelines, e.g. whether simply reinstalling the toolchain has a nonzero chance of breaking it.

[Floris van Doorn]

The next time I encounter it I will try to see if I can send the state of the toolchain that I downloaded. The only extra piece of information I have is that leanc --version also showed the "no such file or directory"-error, so it must indeed be missing something pretty basic.

[Sebastian Ullrich]

Thanks, that basically confirms that the executable itself is missing

[Floris van Doorn]

@Sebastian UllrichI don't get incremental compilation in

set_option pp.explicit false in
example : True := by
  sleep 1000
  trivial
  sleep 1000
  sleep 1000

That should work since lean4#4364, right?

[Floris van Doorn]

Actually, that is not right. The incremental compilation is working. However, when elaborating the example, it shows the yellow bar for the whole example, not just the remaining part to elaborate.

[Michael Rothgang]

I just found a gem in a log for a failing build. The error is an unused argument warning (which is legitimate, the code is not finished yet). However, the output says

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
-- Mathlib.Tactic.Linter.TextBased
Error: ././././Mathlib/Tactic/Linter/TextBased.lean:180:1: error: (invalid MessageData.lazy, missing context) argument 4 mode : OutputMode

The invalid MessageData part should tell me the error instead.

[Joachim Breitner]

I am probably to blame for this, although ideally you always have a context around when pretty-printing terms, for hovers etc. Can you produce a #mwe and report an issue? It may just be a matter of inserting withSaveInfoContext in the right place, maybe in the linter.

[Michael Rothgang]

I can help you towards this: I did some minimisation and more testing:

• the #lint command in mathlib is fine: it's the runLinter step
• no code is required: anything with an unused argument is fine.
  #13634 is pretty minimal, and CI shows the same error.

[Michael Rothgang]

I just tried doing so in a new project, but I cannot even get lake exe runLinter to show me any errors... huh. New theory: it's about build warnings replayed by the linter step. Sorry, that's all I can do for now.

[Bulhwi Cha]

After moving the Lean toolchain in std#743 from v4.8.0-rc2 to v4.9.0-rc1, the following proof in Batteries.Data.List.SplitOnList no longer works:

theorem splitOnList_nil_left (sep : List α) : splitOnList [] sep = [[]] := by
  cases sep <;> rfl

[Bulhwi Cha]

I had to change the proof to by cases sep <;> unfold splitOnList <;> rfl.

[Joachim Breitner]

If splitOnList is defined by well-founded recursion that's expected, and your fix looks good.

[Sebastian Ullrich]

Floris van Doorn said:

Actually, that is not right. The incremental compilation is working. However, when elaborating the example, it shows the yellow bar for the whole example, not just the remaining part to elaborate.

Thanks, evidently I did not test all aspects of this late change. lean#4407 fixes it. Let's see when a good time for an rc2 would be.

[Kim Morrison]

Joachim Breitner said:

I am probably to blame for this, although ideally you always have a context around when pretty-printing terms, for hovers etc. Can you produce a #mwe and report an issue? It may just be a matter of inserting withSaveInfoContext in the right place, maybe in the linter.

We can consistently reproduce this in the unusedHaveSuffices linter running on nightly-testing. e.g. see the build failure at https://github.com/leanprover-community/mathlib4/actions/runs/9473031464.

However that is far from a #mwe. :-)

[Kim Morrison]

Currently in Batteries/Tactic/Lint/Misc.lean we have:

/--
Return a list of unused `let_fun` terms in an expression.
-/
def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do
  let res ← IO.mkRef #[]
  forEachExpr e fun e => do
    match e.letFun? with
    | some (n, t, _, b) =>
      if n.isInternal then return
      if b.hasLooseBVars then return
      let msg ← addMessageContextFull m!"unnecessary have {n.eraseMacroScopes} : {t}"
      res.modify (·.push msg)
    | _ => return
  res.get

[Kim Morrison]

Shall I change this to:

/--
Return a list of unused `let_fun` terms in an expression.
-/
def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do
  let res ← IO.mkRef #[]
  forEachExpr e fun e => do
    match e.letFun? with
    | some (n, t, _, b) =>
      if n.isInternal then return
      if b.hasLooseBVars then return
      let msg ← Elab.withSaveInfoContext do
        addMessageContextFull m!"unnecessary have {n.eraseMacroScopes} : {t}"
      res.modify (·.push msg)
    | _ => return
  res.get

[Kim Morrison]

@Joachim Breitner, I tried out this change, but it did not have any effect. Suggestions?

[llllvvuu]

^I've diagnosed the issue: lean4#4432. If this is the intended behavior in core, then Batteries printWarning can be patched like so: batteries#838

[Daniel Weber]

I can't reproduce it consistently, but sometimes, especially when having a bunch of nested proofs, the state shown in the infoview is the state of the previous level of nesting.

[Daniel Weber]

def g (a : Nat) : Nat := 2 * a

def f (a : Nat) := g a

theorem f_eq_g (a : Nat) : f a = g a := rfl

example : f 1 = 2 := by
  rw [f_eq_g]
  unfold g
  --<--here
  rfl

this seems to work fairly often, but note that it doesn't happen if you copy-paste the example - you have to type it by hand

[Sebastian Ullrich]

Could you please test this on nightly-testing as well?

[Daniel Weber]

It doesn't seem to happen there

[Sebastian Ullrich]

Thanks! Did your original example have a comment as well? The issue is very sensitive on the amount of whitespace and comments around

[Daniel Weber]

No, but adding the comment here didn't change it

[Notification Bot]

15 messages were moved from this topic to #general > MessageData without context by Joachim Breitner.

[Michael Stoll]

When editing in a long proof yesterday evening (in Mathlib.NumberTheory.GaussSum, while working on #13737) recently, I noticed various problems (using VSCode):

• sometimes the old goal state (i.e., before the tactic) was shown after a tactic
• sometimes the proof (or the part from the editing position onwards) was not re-checked after editing (and Shift-Ctrl-X did not work; I had to click the "Restart File" button)
• sometimes the language server seemed to hang (with either the whole file being marked with the orange bar or only the long proof)

These problems did not appear to be completely deterministic, so it is probably hard to produce reproducible #mwe s.

[Yaël Dillies]

This was already reported and is being fixed upstream

[Yaël Dillies]

(not sure where this was reported, though)

[Sebastian Ullrich]

@Michael Stoll @Riccardo Brasca Could I ask you as well to reproduce your issues on the nightly-testing branch?

[Michael Stoll]

I can try this evening (CEST).

[Riccardo Brasca]

Same problem for me.

[Sebastian Ullrich]

Okay, I can reproduce. Thanks.

[Peter Nelson]

What is the planned timeline for rc2? The 'wrong goals' bug is a little painful.

[Chris Birkbeck]

I'm also having this bug and I agree its quite painful.

[Michael Stoll]

Michael Stoll said:

I can try this evening (CEST).

The current nightly-testing branch seems to have errors in the imports of the file I was working on. Is there a specific nightly-testing-xxx branch that I can use?

[Michael Stoll]

OK; I've fixed the build errors...

[Michael Stoll]

Playing around a bit with the long proof it seems to work OK (and feels quite a bit snappier) on nightly-testing.

[Kim Morrison]

Sorry about the delay here. I'm hoping to do rc2 tonight.

[Daniel Weber]

Sometimes after finishing a proof it warns that a declaration uses 'sorry' even though it doesn't (Shift-Ctrl-X fixes it). Is this also part of what was fixed?

[Michael Rothgang]

I also had this error.

[Kevin Buzzard]

Worse -- I have VS Code reporting that a proof is fine, and both "restart file" and "restart server" continue to report that it's fine (the orange bars appear and then they go with no errors), but building Lean on the command line reports an error.

[Kevin Buzzard]

I've fixed my proof in VS Code and now it's compiling fine on command line and reporting

this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`

on a random simp call in VS Code. I remember seeing Lean like this once before, around a year ago, it was constantly giving incorrect "this tactic is never executed" reports. This time "restart file" does fix it.

[Yaël Dillies]

Same issues here

[Kim Morrison]

Repros very welcome. :-)

[Yaël Dillies]

Currently it's an heisenbug to me :frown:

[Mario Carneiro]

I'm pretty sure this is related to a bad interaction between unreachableTactic linter and the new tactic caching feature in 4.9.0-rc1

[Sebastian Ullrich]

Are these observations about rc2? If so, could we please move them to a new topic?

[Mario Carneiro]

Well I think they are true about both rc1 and rc2

[Mario Carneiro]

the issue was introduced in rc1

[Sebastian Ullrich]

Mario Carneiro said:

both rc1 and rc2

Thanks, that was the important missing bit. Certainly if there is any incongruence in positions between the info tree and the syntax tree, this linter will be the most prominent part to complain. Now we just need a reproducer.

[Sebastian Ullrich]

I'd hope that if you do come across such an example, undoing and then redoing a few steps should consistently replay it

[Peter Nelson]

I found the unused tactic linter error bug rare (and nondeterministic) but once it shows up, it sticks around even when things are changed quite substantially in the proof where it appears - this was with rc1.

Given that it goes away when the server is restarted, are there any specific tips for actually isolating such a thing once it starts appearing?

[Sebastian Ullrich]

See if it disappears if you undo enough steps and reappears if you redo them

[Daniel Weber]

Perhaps it's possible to use rr? Or maybe just screen recording and restarting the server every so often will suffice

[Sebastian Ullrich]

This topic has been pretty quiet, are people still encountering this issue on rc2?

[Yaël Dillies]

Which one? The unused tactics one? I've been encountering it

[Sebastian Ullrich]

Yes, that's the one. Randomly editing Mathlib doesn't trigger it for me so I'm not sure what else to try

[Yaël Dillies]

I can't quite ensure you it was on rc2. I keep on switching branches and it might have happened on a branch that was still on rc1

[Sebastian Ullrich]

From the code I can completely see how this issue was introduced by rc1 and could have been fixed by rc2 so I'm really going off Mario's and your report that this is still happening

[Yaël Dillies]

Okay, I'll keep an eye out

[Kevin Buzzard]

I'm pretty sure I'm still seeing random "this tactic is not used" incorrect reports on rc2 but whenever I see them I try and capture them with ctrl-Z and ctrl-shift-Z but they're gone. Will keep trying.

[Rémy Degenne]

I saw that yesterday as well (on rc2): I modified the last line of a proof and suddenly several lines above were reported as containing unreachable tactics. Restarting the file made it go away. I don't have a file where I can reliably reproduce it though.

[Floris van Doorn]

One of my students @Hannah Scholz reported that she didn't encounter the "wrong goal state / no goals" issue anymore in rc2.

[Kevin Buzzard]

I think Hannah just saw me encountering it in rc2

[Floris van Doorn]

Ok, never mind then.

[Peter Nelson]

I've seen it in RC2 as well. I tried isolating, but made it disappear.

[Bhavik Mehta]

I just hit an instance of this too, it still happens but it seems much less frequent than in rc1

[Martin Dvořák]

Does rc3 have the same problem? I cannot decide whether to upgrade or downgrade my project.

[Sebastian Ullrich]

Most likely no changes in rc3. Even if we don't have a reproducer, it would be really helpful to just post where you have encountered the issue, ideally together with the first affected state of the command and a description of the change you did to get there. Perhaps there is a common theme that could explain the low frequency of the issue, such as a specific tactic combinator triggering it.

[Sebastian Ullrich]

Because I still haven't seen it myself and @Mario Carneiro, author of the linter, just told me he likely hasn't either on rc2

[Martin Dvořák]

Alright, non-minimal non-working example:
https://github.com/madvorak/vcsp/blob/e13013a79d4b66ad2c1c3976571cd475ff6769c7/VCSP/LinearProgrammingE.lean#L251

Just write any nonsense on this line (but it must use existing identifiers — such as rfl which won't work there). VS Code does not show any error. The only way to find out that something is wrong (inside the IDE, without going to the command line) is that the proof state does not update with new lines.

[Sebastian Ullrich]

This is a different issue and on rc1? rc1 bug reports are not helpful at this point.

[Martin Dvořák]

Oh sorry; I tried to do the same thing in rc2, but the error was the same so I didn't commit the bump.

[Sebastian Ullrich]

Huh, thanks, I'll take a look

[Sebastian Ullrich]

Could you please push a commit/branch with the updated toolchain and manifest and a description of a specific change to trigger the issue?

[Martin Dvořák]

Alright, this is the same bug on v4.9.0-rc3:
https://github.com/madvorak/vcsp/tree/bug
The bug doesn't seem to depend on the sequence of editing operations that got me there. Just open this project as it is in VS Code.

Clearly, this long rfl sequence should trigger an error:
https://github.com/madvorak/vcsp/blob/97f4ce4ef774e730b5e6495c43434adebf2e188e/VCSP/LinearProgrammingE.lean#L250
Unfortunately, VS Code does not show anything. You must go to the command line and build it there in order to see the the error message.

[Martin Dvořák]

Not really MWE:

import Mathlib.Order.Basic
import Mathlib.Data.Nat.Defs

example {a : ℕ} (ha : a ≤ 1) : a = 0 := by
  cases eq_or_lt_of_le (by exact ha) with
  | inl eq1 => rfl
  | inr lt1 => rwa [Nat.lt_one_iff] at lt1

example {a : ℕ} (ha : a ≤ 1) : a = 0 := by
  cases eq_or_lt_of_le ha with
  | inl eq1 => rfl
  | inr lt1 => rwa [Nat.lt_one_iff] at lt1

The rfl in inl eq1 should make VS Code complain in both proofs.
Only the second example leads to VS Code displaying the error.
The same inconsistency happens in Lean 4 Web.

[llllvvuu]

That can be de-Mathlibifed it seems:

example {a : Nat} (ha : a ≤ 1) : a = 0 := by
  cases Nat.eq_or_lt_of_le (by exact ha) with
  | inl eq1 => rfl
  | inr lt1 => sorry

example {a : Nat} (ha : a ≤ 1) : a = 0 := by
  cases Nat.eq_or_lt_of_le ha with
  | inl eq1 => rfl
  | inr lt1 => sorry

[Martin Dvořák]

MWE:

example {P Q : Prop} (hpq : P ∨ Q) : Q := by
  cases (show P ∨ Q by exact hpq) with
  | inl hp => rfl
  | inr hq => exact hq

example {P Q : Prop} (hpq : P ∨ Q) : Q := by
  cases (show P ∨ Q from hpq) with
  | inl hp => rfl
  | inr hq => exact hq

VS Code displays the error only in the second example.

[Mario Carneiro]

I guess this is not an incr.comp. bug it is

[llllvvuu]

just reported: https://github.com/leanprover/lean4/issues/4553

[Sebastian Ullrich]

And fixed: lean#4554

[Sebastian Ullrich]

Thanks for the reproducer, if only the other issue was as easy to pin down!

[Sebastian Ullrich]

Even if we don't have a reproducer, it would be really helpful to just post where you have encountered the issue, ideally together with the first affected state of the command and a description of the change you did to get there. Perhaps there is a common theme that could explain the low frequency of the issue, such as a specific tactic combinator triggering it.

Just to clarify, this wasn't meant as a direct answer to @Martin Dvořák but to anyone encountering the linter issue!

[Bhavik Mehta]

I'm not certain about this, but I just had a lemma give a(n incorrect) warning that it used sorry, then #print axioms agreed. On commenting out and uncommenting, the warning went away and everything seemed normal. The step I took just before the weird behaviour happened was deleting a simp only command. I believe that the unused tactics thing has also happened to me in the past twice just after deleting a simp only. Again I'm not certain about this, but maybe this is still useful.
(Specifically in this case, the simp only was unnecessary, and so deleting it should have made the theorem true. And it was sorry-free, so the warning surprised me)

[Kim Morrison]

I also saw an incorrect "uses sorry" warning yesterday, which appeared on the declaration above the one I was editing. I couldn't get it to come back after restarting the server, however, but I also couldn't remember the exact edit sequence.

[Martin Dvořák]

Sebastian Ullrich said:

And fixed: lean#4554

Can projects downstream of Mathlib already use the fixed version please?
Sorry, I didn't notice it hadn't been merged yet.

[Kim Morrison]

lean#4554 has just been sent to the merge queue, and it will be backported to v4.9.0. Since this seems to have been causing trouble for users I'm inclined to just cut v4.9.0-rc4 shortly (tonight or tomorrow my time), and move Mathlib to that (and then anyone downstream has the option, too).

[Sebastian Ullrich]

Since this seems to have been causing trouble for users

I think this has been reported only once so far, by Martin? That's more than zero but I'm currently more concerned about the open issues mentioned above, the linter issue and the sorry issue.

[Sebastian Ullrich]

(moving to mathlib@stable also fixes the bug for downstream usesrs, in a manner)

[Kim Morrison]

Okay, in that case I will not cut rc4 at this point!

[Martin Dvořák]

Martin Dvořák said:

Does rc3 have the same problem? I cannot decide whether to upgrade or downgrade my project.

I apologize for the confusion I caused. I originally thought I was experiencing the same bug as everybody else, as I hadn't read this thread properly.

[Sebastian Ullrich]

No problem, I don't expect users to differentiate whether two issues could have the same root cause or not. But for the protocol, your issue did turn out to be quite specific to the induction/cases ... (by ...) ... with pattern which I don't think is used very often :) .

[Mario Carneiro]

I already showed this to Sebastian in person, but I have a reliable non-minimized reproduction for the sorry bug:

• check out mathlib commit 59f1833d, open file Mathlib/InfinityCosmos.lean
• just before line 39 (Functor.id_eq_id), add the following:

                                   -- (this line should be blank but zulip eats the formatting)
def foo := 1

• Insert the two lines above in quick succession (about 1/3 second between them). The easiest way to do this is to type out those two lines, then delete the def foo := 1 line, delete the blank line, and then use Ctrl-Z twice in quick succession to reinsert them.
• Expected result: There will be a message on Adjunction.ofHomRestrictionIso saying it uses 'sorry', and depending on how fast you were some of the simp calls will also trigger the unreachableTactic linter.

Screencast-from-06-25-2024-024339-PM.webm

[Bhavik Mehta]

Another bug I've hit a few times today (on rc3) is my vscode suddenly disabling any unicode inputs. I can type, eg, \N, but it just remains like that (no underscore appears). It seems to happen when I change tabs in vscode. (gitpod on a recent mathlib, 4.9.0-rc3). Apologies if this is also unrelated to the issues above.

[llllvvuu]

Bhavik Mehta said:

Another bug I've hit a few times today (on rc3) is my vscode suddenly disabling any unicode inputs. I can type, eg, \N, but it just remains like that (no underscore appears). It seems to happen when I change tabs in vscode. (gitpod on a recent mathlib, 4.9.0-rc3). Apologies if this is also unrelated to the issues above.

I've been hitting this for a while as well (probably well before 4.9.0-rc3, maybe even 4.8.0 or earlier), but I didn't know if it was an issue with Lean LSP, Lean VSCode extension, VSCode itself, or some unrelated other extension or OS issue

[Kim Morrison]

Any repro on the unicode inputs issue would be great.

I have a semi-reducible repro, which is that if I work over an ssh connection with a very long ping time that then the unicode replacement works either some or not at all. I did attempt to simulate this without travelling to Europe via a nested sequence of ssh tunnels, with partial but not particularly useful success!

@Marc Huisinga is aware of this one, but I'm not sure if what @Bhavik Mehta and @llllvvuu are seeing is the same or not.

[llllvvuu]

It might be the same issue; I've only experienced it over SSH

[Marc Huisinga]

Bhavik Mehta said:

Another bug I've hit a few times today (on rc3) is my vscode suddenly disabling any unicode inputs. I can type, eg, \N, but it just remains like that (no underscore appears). It seems to happen when I change tabs in vscode. (gitpod on a recent mathlib, 4.9.0-rc3). Apologies if this is also unrelated to the issues above.

What version of the VS Code extension are you using?

[Marc Huisinga]

Ah, I think I know what's going on here. This is likely a bug that was already fixed by vscode-lean4#480, but since GitPod uses VS Code extensions from the openvsx marketplace which has been down for the last week until yesterday, preventing us from publishing the extension, GitPod is still using an old VS Code extension version that doesn't include the fix. Let me see if publishing to openvsx works now.

[Marc Huisinga]

So, GitPod uses an extension version of 0.0.164, but the most recent one is 0.0.168.

[Marc Huisinga]

0.0.169 is now available on OpenVSX. Please let me know if you still encounter issues with the abbreviation mechanism breaking when switching tabs on that version.

[Marc Huisinga]

llllvvuu said:

Bhavik Mehta said:

Another bug I've hit a few times today (on rc3) is my vscode suddenly disabling any unicode inputs. I can type, eg, \N, but it just remains like that (no underscore appears). It seems to happen when I change tabs in vscode. (gitpod on a recent mathlib, 4.9.0-rc3). Apologies if this is also unrelated to the issues above.

I've been hitting this for a while as well (probably well before 4.9.0-rc3, maybe even 4.8.0 or earlier), but I didn't know if it was an issue with Lean LSP, Lean VSCode extension, VSCode itself, or some unrelated other extension or OS issue

I consider the SSH thing to be a VS Code issue, since (AFAIK) there is no way for us to work around it in vscode-lean4. We may however mitigate it in the future by moving the abbreviation mechanism to an entirely separate VS Code extension that always runs on the client and is hence not affected by the added latency of using SSH.
If you're curious about some of the details on what causes this race condition, see vscode-lean4#389. The core issue is that VS Code provides no API to read from the text editor and write to it in an atomic manner.

[Bhavik Mehta]

Yeah I think I've only had this on ssh as well, so it seems most likely the same issue. Thanks for the resolution!

[Marc Huisinga]

To be clear, the SSH issue in particular is not resolved yet. It also manifests differently from what you described: The underline is rendered, but when you attempt to replace the abbreviation, VS Code refuses the edit and retains the underline instead of replacing the abbreviation. In your "Lean: Editor" output window (Troubleshooting: Show Output), you should also see an "Unable to replace abbreviation" error when this occurs.

The particular issue you described where the abbreviation mechanism stops working entirely when switching tabs may have been fixed by vscode-lean4#480, though, and now that we can ship this fix to GitPod again, it may have been resolved.

[Bhavik Mehta]

Sebastian Ullrich said:

Most likely no changes in rc3. Even if we don't have a reproducer, it would be really helpful to just post where you have encountered the issue, ideally together with the first affected state of the command and a description of the change you did to get there. Perhaps there is a common theme that could explain the low frequency of the issue, such as a specific tactic combinator triggering it.

Just had it again, I think ~5 lines below and including a simp only had the unused tactic lint flag them. The action I took directly before this happened was to delete an unused argument. I may just have increased suspicions around simp only, but it does seem a common factor to me.
Reinserting the unused argument then deleting it again didn't make the warnings come back though.

[Sebastian Ullrich]

Yes, this issue turned out to be specific to simp and perhaps some other elaborators plus specific timing around edits, which explains why it was so hard to nail down. lean#4569 should fix both the sorry bug and the lint bug.

[Shreyas Srinivas]

I had the issue Floris described at the top of this thread when trying to update a repository from 4.8.0 to 4.9.0

[Shreyas Srinivas]

Specifically, lake complains about unknown attribute [test_driver]. This issue persists even if I delete lake-manifest.json and ./.lake.

What's the recommended fix?

[Shreyas Srinivas]

I am on ubuntu

[Mario Carneiro]

restart the server, after ensuring that lean-toolchain has the correct version in it

[Shreyas Srinivas]

why would the LSP cause errors if I am in the terminal?

[Shreyas Srinivas]

Now I have a new error:

error: ././.lake/packages/mathlib/lakefile.lean:21:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:22:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:23:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:24:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:25:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors

[Shreyas Srinivas]

The error is specifically on these lines of the newly cloned mathlib:

require "leanprover-community" / "batteries" @ "git#main"
require "leanprover-community" / "Qq" @ "git#master"
require "leanprover-community" / "aesop" @ "git#master"
require "leanprover-community" / "proofwidgets" @ "git#v0.0.39"
require "leanprover-community" / "importGraph" @ "git#main"

[Shreyas Srinivas]

Which is strange. has the syntax for require changed?

[Shreyas Srinivas]

Okay so I think the reason for the second error is I had removed the "stable" branch in my project lakefile. Added it again. It works now. Maybe this error was an issue with updating to 4.10-rc1

[Mario Carneiro]

You need 4.10.0-rc1 to compile mathlib master's lakefile. Use cp .lake/packages/mathlib/lean-toolchain . and then rerun lake update

[Mario Carneiro]

or don't use the master branch of mathlib, use stable / v4.9.0 branch if you want to use v4.9.0

[Shreyas Srinivas]

Wasn't there an update script that handled precisely this issue of copying lean toolchain files?

[Shreyas Srinivas]

Anyway, I'll go with 4.9.0 for now

[Mario Carneiro]

Shreyas Srinivas said:

Wasn't there an update script that handled precisely this issue of copying lean toolchain files?

There is, but it's written as a lake script which means that it breaks whenever lake has a forward-incompatible change, which happens almost every stable

[Mario Carneiro]

i.e. it's in that mathlib lakefile that breaks due to a syntax error because the old lake can't read it

[Shreyas Srinivas]

Some lake failures feel like they should be silent failures. For example, when I am setting up a mathlib project, it is not clear why I need the part of Mathlib lakefile that deals with tests to work.

[Shreyas Srinivas]

With TOML files hopefully this can already be done since lake just has to ignore the sections it doesn't understand yet