Possible infinite loop?

Stream: lean4

[Shange Tang]

The following lean code can not be compiled successfully. It took more than half an hour and the compiling is still running. I am wondering if there is some infinite loop in this code?

import Mathlib
import Init.Data.Nat

example (n : ℕ) : Nat.gcd (3 * n + 4) (2 * n + 3) = 1 := by
  induction n with
  | zero =>
    -- Base case: n = 0
    simp [Nat.gcd]
  | succ n ih =>
    -- Inductive step: assume the statement holds for n, prove for n + 1
    have h1 : Nat.gcd (3 * (n + 1) + 4) (2 * (n + 1) + 3) = Nat.gcd (2 * n + 3) (3 * n + 4) := by
      rw [Nat.gcd_comm]
      simp [Nat.gcd]
      ring
    rw [h1]
    exact ih

[Julian Berman]

Can you have a quick look at #backticks (it's a link, you can click) and fix the formatting just to be sure of exactly what you're running

[Julian Berman]

It's also possible that what appears to be compiling is Mathlib -- the way you should get access to Mathlib is by downloading a "cache" which saves all of the work of building it yourself. Usually the way you do that is by running lake exe cache get (first closing VSCode!) -- have you run that?

[Shange Tang]

Thanks for the reply! I will try that.

[Adomas Baliuka]

Julian Berman said:

the way you should get access to Mathlib is by downloading a "cache" which saves all of the work of building it yourself. Usually the way you do that is by running lake exe cache get (first closing VSCode!) -- have you run that?

Why close VSCode? I regularly lake exe cache get without closing, never had an issue (with this particular command. Of course, updating dependencies etc. causes issues often)

[Julian Berman]

I think not closing it just runs the risk that there's some compilation still ongoing (whereas closing it will stop that). It's not the worst thing, but I've seen others recommend closing it just to not be confused by continued high CPU usage. (All the above is parroted mostly though as I don't use VSCode often myself).

[Yaël Dillies]

I would strongly recommend you stop using lake exe cache get and start using the new vscode command Lean 4: Project: Fetch Mathlib Build Cache For Focused File (sadly only works within mathlib right now, but I'm sure we can open an issue)

[Marc Huisinga]

Yaël Dillies said:

I would strongly recommend you stop using lake exe cache get and start using the new vscode command Lean 4: Project: Fetch Mathlib Build Cache For Focused File (sadly only works within mathlib right now, but I'm sure we can open an issue)

This is due to the API of lake exe cache get, which IIRC is hardcoded for Mathlib.

[Marc Huisinga]

At least I think that I tested lake exe cache get <path> in projects downstream of Mathlib at the time and couldn't get it to work, but it's been a while

[Yaël Dillies]

I have just tried. Seems to work fine?

gitpod /workspace/LeanAPAP (nnLpNorm) $ lake exe cache get Mathlib/Algebra/Module/PID.lean
installing leantar 0.1.13
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100 1054k  100 1054k    0     0  1417k      0 --:--:-- --:--:-- --:--:-- 1417k

Attempting to download 1559 file(s)
Downloaded: 1559 file(s) [attempted 1559/1559 = 100%] (100% success)
Decompressing 1559 file(s)
Unpacked in 41 ms
Completed successfully!

[Marc Huisinga]

Yes, but you want to get the cache for the current file (i.e. all of its Mathlib dependencies), not a specific dependency, no? Otherwise you'll have to copy and paste paths again, which is why this command exists in the first place.

[Yaël Dillies]

Ah sorry, I misunderstood what you said. Let me try again

[Yaël Dillies]

Indeed :sad:

gitpod /workspace/LeanAPAP (nnLpNorm) $ lake exe cache get LeanAPAP/Prereqs/Expect/Basic.lean
uncaught exception: Unknown package directory for LeanAPAP

[Yaël Dillies]

The alternative would be for the vscode action to run lake exe cache get <file> for file runnning over all mathlib imports of the file. Do you think that's doable?

[Kim Morrison]

@Yaël Dillies, how about just fixing cache, rather than asking for the VSCode extension to jump through hoops?

[Yaël Dillies]

I mean, that's obviously the better solution, but I thought this was put aside because we didn't agree on mathlib getting special-casing?

[Marc Huisinga]

I don't think VS Code should provide this functionality. I'd like the commands of the extension to remain either thin wrappers over existing tooling functionality or more elaborate tools which provide UI interactivity that the corresponding CLI tools can't provide.

The crux with vscode-lean4 is that it is not versioned with Lean (or Mathlib) and needs to be backwards compatible at least with Lean versions where users could already rely on a given vscode-lean4 feature in the past.

[Ruben Van de Velde]

Why not use lake exe cache get without a path?

[Yaël Dillies]

That takes way longer than it should. Most files import at most a quarter of mathlib

[Ruben Van de Velde]

How often do you update mathlib?

[Yaël Dillies]

I switch branches every 3-5 minutes