Stuck on an outdated version of mathlib?

Stream: new members

[Jake Levinson]

I think the version of mathlib on one of my Lean projects is out of date. When I type lean -version I get

Lean (version 3.32.1, commit 35b3a9c4e2d3, Release)

But if I run elan update I get

> elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.42.1
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2020-04-28
info: checking for self-updates
error: failed to parse latest release tag

This might be tied to me being on an M1 mac. It caused me various weird hurdles with my initial install. (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20macs)

[Jake Levinson]

I guess I didn't actually ask a question... my question is, how do I get it to update?

[Yaël Dillies]

Assuming you created those projects using leanproject, leanproject up should be the way to go.

[Jake Levinson]

That command fails:

...
ImportError: dlopen(/opt/homebrew/lib/python3.9/site-packages/_cffi_backend.cpython-39-darwin.so, 2): Library not loaded: /opt/homebrew/opt/libffi/lib/libffi.7.dylib
  Referenced from: /opt/homebrew/lib/python3.9/site-packages/_cffi_backend.cpython-39-darwin.so
  Reason: image not found

I feel like I've seen this error message before, but I don't remember where...

[Matt Diamond]

might need to reinstall libffi? you could try brew uninstall libffi; brew install libffi

[Matt Diamond]

it might be installed but not linked

[Jake Levinson]

@Matt Diamond @Yaël Dillies I eventually got the commands working (I had to reinstall elan and lean in the end).

Now though, I keep getting "excessive memory consumption" errors in VS Code. I think (?) all of mathlib is already compiled, I have oleans files already, but e.g. a single command of library_search typically causes VS Code to crash now. Even plain old typing and editing in a file seems more prone to cause an outage. Any ideas on how to troubleshoot?

[Yaël Dillies]

This very much sounds like you have the wrong oleans. Try leanproject get-c again.

[Jake Levinson]

> leanproject get-c
Looking for lean-topology oleans for 07bfb91
  locally...
No cache available for revision 07bfb91
Looking for lean-topology oleans for b7d8e4d
  locally...
No cache available for revision b7d8e4d
Looking for lean-topology oleans for 0a2b52e
  locally...
No cache available for revision 0a2b52e
Looking for lean-topology oleans for 8b2359e
  locally...
No cache available for revision 8b2359e
Looking for lean-topology oleans for ed4a7a5
  locally...
No cache available for revision ed4a7a5
Looking for lean-topology oleans for 5a599b5
  locally...
No cache available for revision 5a599b5
Looking for lean-topology oleans for fc3ae7b
  locally...
No cache available for revision fc3ae7b
Looking for lean-topology oleans for 52ef265
  locally...
No cache available for revision 52ef265
Looking for lean-topology oleans for 57b15b3
  locally...
No cache available for revision 57b15b3
Looking for lean-topology oleans for a62215f
  locally...
No cache available for revision a62215f
Looking for lean-topology oleans for d4dee61
  locally...
No cache available for revision d4dee61
Looking for lean-topology oleans for dcdd346
  locally...
No cache available for revision dcdd346
Looking for lean-topology oleans for 5a30e79
  locally...
No cache available for revision 5a30e79
Looking for lean-topology oleans for c6552cc
  locally...
No cache available for revision c6552cc
Looking for lean-topology oleans for 431124f
  locally...
No cache available for revision 431124f
Looking for lean-topology oleans for 84b2ce0
  locally...
No cache available for revision 84b2ce0
Looking for lean-topology oleans for 25fcf7a
  locally...
No cache available for revision 25fcf7a
Looking for lean-topology oleans for 9e6d61a
  locally...
No cache available for revision 9e6d61a
Looking for lean-topology oleans for 1e6f420
  locally...
No cache available for revision 1e6f420
Looking for lean-topology oleans for 170c3fa
  locally...
No cache available for revision 170c3fa
Looking for lean-topology oleans for ebc4e68
  locally...
No cache available for revision ebc4e68
Looking for lean-topology oleans for f847ada
  locally...
No cache available for revision f847ada
Looking for lean-topology oleans for 9b8e5ca
  locally...
No cache available for revision 9b8e5ca
No archives available for any commits!

[Yaël Dillies]

Oh you're on your own project. Do leanproject get-m then.

[Jake Levinson]

> leanproject get-m
Looking for mathlib oleans for 2a04ec03f1
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 2340 [00:04, 553.28/s]

Is this equivalent to leanproject get-mathlib-cache? I believe I ran this command yesterday too.

[Jake Levinson]

I'm still getting memory errors, e.g.

excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)

This is in a 90-line file importing

import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

[Kyle Miller]

A shot in the dark: just in case there's something unknown wrong with them, you could try clearing all the archive files from the ~/.mathlib folder, then when you do leanproject get-mathlib-cache it'll download them again. (I believe leanproject get-m is the same and that it's just an abbreviation.)

[Jake Levinson]

Okay, I'll try it. How do I clear those files?

[Damiano Testa]

Maybe, after leanproject get-m, also leanproject build?

[Kyle Miller]

You can just delete them any way you might delete files

[Jake Levinson]

Ok. But which files are you referring to? ~/_target/deps/mathlib/archive/?

[Kyle Miller]

On Mac, you can go to the Finder, do Go -> Location, type in ~/.mathlib, then you can see all these .tar.xz files

[Jake Levinson]

Oh literally from my home directory.

[Kyle Miller]

(I doubt this will fix anything, but you'll save some disk space at least. I periodically clear it out for that reason.)

[Jake Levinson]

Damiano Testa said:

Maybe, after leanproject get-m, also leanproject build?

I had run this previously, I'll run it again once the the cache is remade. Though, is there a way to ask it to only compile mathlib, and not the files in my actual project? A bunch of them have scratchwork or incomplete stuff or whatever, so just running leanproject build produces a ton of error messages.

[Jake Levinson]

(All the files in my project are in a separate directory not along the _target/deps/mathlib path)

[Jake Levinson]

Okay, I have deleted those files and rerun leanproject get-m. Still getting memory errors, in this case it happened right away as soon as I made an edit to a line in the file I was working on.

[Kyle Miller]

I assume you restarted the Lean process too?

[Kyle Miller]

I wonder if there's a mismatch between the version of Lean you're using for your project and the version of Lean that produced the mathlib oleans. I have to admit I don't have much experience with using mathlib as a dependency -- usually I work within mathlib itself.

[Jake Levinson]

Is that separate from closing and reopening VS Code?

[Jake Levinson]

Hmm. I don't think I know the difference. What does it mean to work within mathlib itself?

[Kyle Miller]

That's sufficient. You can also open the command palette and do "Lean: restart"

[Jake Levinson]

Oh wow, that is so much more convenient than reopening VS Code!

Anyway, memory errors continue. This time I managed to edit two lines before it crashed.

[Kyle Miller]

Jake Levinson said:

Hmm. I don't think I know the difference. What does it mean to work within mathlib itself?

You can create a Lean project that, rather than depending on mathlib, is mathlib. This is mostly useful if you're planning on eventually submitting a PR.

For example, here's a command to create a project that's a local branch of mathlib called "kmill_add_frobozz"

leanproject get -b mathlib:kmill_add_frobozz

[Kyle Miller]

@Jake Levinson What are the contents of your leanpkg.toml for your project?

[Jake Levinson]

> cat leanpkg.toml
[package]
name = "lean-topology"
version = "0.1"
lean_version = "leanprover-community/lean:3.42.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "2a04ec03f17ad178e2e1e596973f7eb4c9838d1a"}

[Kyle Miller]

I just wanted to check that your version of mathlib matched up with your version of lean -- they do. (Revision 2a04ec... is from yesterday and uses lean 3.42.1.) Sorry, I'm pretty much out of ideas for what could be the problem now. I have both Intel Mac and Linux installations, but no M1 Mac installation.

[Jake Levinson]

Maybe I should just make a new leanproject and copy my files over to it.

[Jake Levinson]

I was born in am a child of in the 90s, so "turning it off and turning it on again" is one of my preferred troubleshooting methods.

[Kyle Miller]

If you have time to let it run, you could try lean --make _target/deps/mathlib/src to rebuild the oleans yourself

[Kyle Miller]

You can also let it compile in parallel by giving it the -j option, like lean -j4 --make _target/deps/mathlib/src to use four threads.

[Jake Levinson]

Hmm, that crashes immediately... maybe this is the sign:

/.../lean-topology/_target/deps/mathlib/src/topology/category/CompHaus/default.lean:1:0: error: ambiguous import,
it can be '/.../lean-topology/_target/deps/mathlib/src/topology/connected.lean'
or '/.../lean-topology/src/topology/connected.lean'

[Jake Levinson]

So maybe this is somehow my project (which has some homemade point set topology stuff) clashing with mathlib.

[Jake Levinson]

(It popped up a bunch of messages of that form

[Kyle Miller]

That seems promising. Maybe put all your own stuff in a subfolder, like jlevinson or something like that?

[Jake Levinson]

That stuff is in its own folder already (lean-topology/src/topology/ instead of lean-topology/_target/deps/mathlib/...). But I'm going to try renaming those files.

[Jake Levinson]

Oh, I guess renaming the topology folder to jl-topology or something would be fine too. It seems that I inadvertently had both the name and folder hierarchy the same as in mathlib.

[Kyle Miller]

Yeah, the point is to rename it so the modules show up elsewhere in the module hierarchy. (Maybe do jl_topology instead, because I don't think you can have hyphens in module names.)

[Jake Levinson]

Okay, now lean --make _target/deps/mathlib/src runs and terminates with no output after a ten seconds or so.

[Kyle Miller]

:thumbs_up: That means all the oleans are up-to-date

[Jake Levinson]

OK, time to try editing VS code again.

[Jake Levinson]

No dice... crashed again after editing a few lines in a larger file.

[Kyle Miller]

Maybe try lean --make src now?

[Jake Levinson]

That runs OK.

[Kyle Miller]

Are you able to edit files now if you restart lean?

[Kevin Buzzard]

This should all be working now. Have you got a lot of open files in VS Code? Close all but the one you're working on. Are you using a machine with <= 8 gigs of ram?

[Jake Levinson]

So I have been able to edit without further crashes in a different file that only imports data.set.basic from mathlib, plus importing other files I've been working on in this project, totaling ~1000 lines of code, say. (This project actually has nothing to do with topology, I just kept reusing a leanproject I created a year ago.)

If I work in the 90-line file with

import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

then it still seems to quickly crash when I make small changes.

[Jake Levinson]

For example -- I just switched over to that file and it crashed instantly upon opening. Whereas I just spent the last half-hour successfully editing the other file.

[Jake Levinson]

I'm on an M1 Macbook Pro with 16 gigs of ram. Prior to trying out this ring theory file, I've had no problem having nine files open at once, with hundreds of lines of code each, and frequently switching between them to work on different parts.

[Jake Levinson]

This error message seems very uninformative... I have no idea if it's an actual memory overload, or something else. I'm not even sure how to "increase the memory consumption threshold".

[Eric Rodriguez]

have you restarted vscode? if you can send the file, I have the exact same computer and things are fine here, no crashes. those first two lines don't seem to crash my computer

[Eric Rodriguez]

is this file you mention editing in the hierarchy to this 90-line file?

[Jake Levinson]

The folder hierarchy is like this:

lean-topology/
  polynomials_scratch.lean  -- 90-lines, imports ring theory
  src/
    dir1/ -- contains various other older things I've written
    current/ -- contains 9 files totaling 1000-1500 lines, mainly importing data.set.basic
  _target/ -- leads to mathlib

[Jake Levinson]

The polynomials file is (modulo small edits) posted here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Working.20with.20polynomial.20factorizations

[Jake Levinson]

Here is the current version:

import tactic
import ring_theory.polynomial.homogeneous
import field_theory.is_alg_closed.basic

variables {K : Type*} [field K] [is_alg_closed K]

lemma mv_polynomial.is_homogeneous.factor
  {σ : Type} {f g : mv_polynomial σ K}
  {n : ℕ} (hg : g.is_homogeneous n) (hfg : f ∣ g) :
f.is_homogeneous (f.total_degree) := sorry
-- proof: by Damiano's argument higher up the thread (look at minimum and maximum degree parts of f)

lemma mv_polynomial.prime_of_linear {σ : Type} (f : mv_polynomial σ K)
  (f_ne_zero : f ≠ 0) (hf : f.is_homogeneous 1) : prime f :=
begin
  split, exact f_ne_zero,
  split,
  { rintro ⟨g, hg⟩,
    have h1 : 1 = (coe g⁻¹) * f,
      rw [← hg, ← units.coe_mul], simp,
    have h2 := mv_polynomial.is_homogeneous_one _ K,
    have h3 := (h2.factor ⟨_, h1⟩).mul hf,
    rw h1 at h2,
    have h4 := mv_polynomial.is_homogeneous.inj_right h3 h2 _,
    exact nat.succ_ne_zero _ h4,
    rw ← h1, exact one_ne_zero, },

  sorry,
end
-- proof: irreducibility (by degree counting) + UFD

lemma mv_polynomial.has_linear_factor
  (f : mv_polynomial (fin 2) K) {n : ℕ} (hf : f.is_homogeneous n) :
∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ f := sorry
-- proof: possibly annoying since it involves dehomogenizing

example {A B q c : mv_polynomial (fin 2) K} (hA : A.is_homogeneous 1) (hB : B.is_homogeneous 2)
  (hq : q.is_homogeneous 2) (hc : c.is_homogeneous 3) (H : B * q = A * c)
  (q_ne_zero : q ≠ 0) (A_ne_zero : A ≠ 0) :
  ∃ x : mv_polynomial (fin 2) K, x.is_homogeneous 1 ∧ x ∣ q ∧ x ∣ c :=
begin
  obtain ⟨x, hx, hxq⟩ := q.has_linear_factor hq,
  have x_ne_zero : x ≠ 0 := ne_zero_of_dvd_ne_zero q_ne_zero hxq,

  by_cases hxc : x ∣ c,
  { exact ⟨x, hx, hxq, hxc⟩, },

  have hxA : x ∣ A,
  { apply ((x.prime_of_linear x_ne_zero hx).dvd_or_dvd _).resolve_left hxc,
    rw [mul_comm, ← H],
    exact hxq.trans (dvd_mul_left _ _), },

  -- pull out factors
  obtain ⟨y, hqxy⟩ := hxq,
  obtain ⟨A', hAxA'⟩ := hxA,
  have hA' : A' ∣ A := ⟨x, mul_comm x A' ▸ hAxA'⟩,
  have A'_ne_zero : A' ≠ 0 := ne_zero_of_dvd_ne_zero A_ne_zero hA',

  have H' : B * y = A' * c,
  { rw [hAxA', hqxy, (by ring : B * (x * y) = x * (B * y)), mul_assoc] at H,
    apply cancel_monoid_with_zero.mul_left_cancel_of_ne_zero x_ne_zero H, },

  -- now collect final goals

  have hyq : y ∣ q := ⟨x, mul_comm x y ▸ hqxy⟩,

  have hy : y.is_homogeneous 1,
  { convert hq.factor hyq,
    apply @nat.add_left_cancel 1,
    apply hq.inj_right _ q_ne_zero,
    exact (hqxy.symm ▸ hx.mul (hq.factor hyq)), },

  have hA'' : A'.is_homogeneous 0,
  { convert hA.factor hA',
    apply @nat.add_left_cancel 1,
    apply hA.inj_right _ A_ne_zero,
    exact hAxA'.symm ▸ hx.mul (hA.factor hA'), },

  have A'_inv : mv_polynomial (fin 2) K := sorry,
  have A'_mul : A'_inv * A' = 1 := sorry,
  -- inverse of a nonzero constant?

  have hyc : y ∣ c,
  { have H'' : c = y * (A'_inv * B),
    symmetry,
    calc y * (A'_inv * B) = A'_inv * (B * y)  : by ring
                      ... = A'_inv * (A' * c) : by rw H'
                      ... = (A'_inv * A') * c : by ring
                      ... = 1 * c             : by rw A'_mul
                      ... = c                 : by ring,
    exact ⟨_, H''⟩, },

  exact ⟨y, hy, hyq, hyc⟩,
end

[Eric Rodriguez]

this is a bit excessive, but what happens if you rm -rf _target and then leanproject get-m?

[Jake Levinson]

I can reproduce the error at this point: I simply can't have both polynomials_scratch.lean and a file from the other directory open at the same time without causing a crash.

I can have polynomials_scratch.lean open on its own, and it is fairly unstable (crashes fairly frequently, seems to run a bit slowly).

And, I can work on my other files (all 9 files open at once, jumping around between them) with only occasional problems.

[Jake Levinson]

Eric Rodriguez said:

this is a bit excessive, but what happens if you rm -rf _target and then leanproject get-m?

Happy to try it. I imagine this will take a while to re-download and recompile?

[Eric Rodriguez]

it's just a redownload, should be max 5 minutes unless your internet is glacial

[Eric Rodriguez]

it's weird that that's the case, because this sort of issue you raise is usually when polynomials_scratch would import something being edited lower down in the hierarchy. in that case, lean would have to recompile everything in-between without using oleans (just keeping it in the memory) which is completely infeasible

[Jake Levinson]

Right, that makes sense. Certainly I've occasionally encountered that in the other project. But I never touch or edit mathlib files themselves.

[Jake Levinson]

OK finished re-downloading. I can have several files from my other project open with no problem.

[Jake Levinson]

... but if I open polynomials_scratch, instant crash.

[Eric Rodriguez]

did you restart vscode as well? aa i've never seen this

[Jake Levinson]

Yes I did. Hmm, I have another file stub from when I tried to use linear_algebra.finite_dimensional, I'll see if that also causes problems. I wonder if my computer is doing something weird with mathlib.

[Jake Levinson]

Never mind, that file doesn't have much in it

[Eric Rodriguez]

I think it's worth trying the new leanproject approach just to check if it's something weirdly specific

[Jake Levinson]

Yeah, good idea. OK.

[Jake Levinson]

No, the same problems seem to arise. Very strange. I wonder if this actually is caused by some memory consumption threshold?

[Jake Levinson]

I also just went to check if VS Code needed to be updated, but it looks up-to-date.

[Arthur Paulino]

Are you watching your RAM while going through these attempts?

[Eric Rodriguez]

I mean, if it is you can up the RAM threshold in the VSCode settings:

[Eric Rodriguez]

image.png

[Jake Levinson]

Arthur Paulino said:

Are you watching your RAM while going through these attempts?

How can I do that?

[Eric Rodriguez]

Activity Monitor

[Jake Levinson]

OK I increased the memory threshold from 4096 to 12288...

[Jake Levinson]

omg that seemed to fix it

[Jake Levinson]

Now I can edit both files!

[Jake Levinson]

Maybe I really was just running out of memory...? bizarre! Maybe I just had too many Google Chrome tabs open (I noticed that my system was already using a lot of the available memory)

[Arthur Paulino]

@Jake Levinson I am not a Mac user but I am certain there's an app that allows you to monitor your memory consumption

[Eric Rodriguez]

oh awesome! now that it's fixed, I have some instructions for cross-compiling Lean to ARM64, if you want to mess with that:https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20Macs.3A.20Installing.20the.20Lean.203.20toolchain/near/265390589

[Jake Levinson]

Interesting. Yeah, some of this is possibly still running on Rosetta since that was the installation pathway before. Would this make things faster / more efficient?

[Eric Rodriguez]

I haven't tried, this is actually why I'm curious, I pretty much always just update myself using this script

[Eric Rodriguez]

not required, just a curiosity^^

[Eric Rodriguez]

note that you need to edit this line in the middle of the script:

# Set this to a local clone of leanprover-community/lean (that you don't mind being messed with!)
cd ~/repos/lean

[Matias Heikkilä]

@Arthur Paulino I think the standard profiler for OSX is "instruments". Source: https://stackoverflow.com/a/11445777

possibly a useful future reference

[Kyle Miller]

If you just want to know how much memory/cpu/power you're using generally, there's Activity Monitor.

[Pedro Sánchez Terraf]

Eric Rodriguez said:

did you restart vscode as well? aa i've never seen this

Not sure if this question belongs to this thread, but anyway:
Is it possible to work with different mathlib versions on the same instance of vscode?

I just realized that if I open two lean files in different repos (with different mathlib versions), vscode uses the version in the _target dir of the first file.

Is it "restarting it" the only way to get the correct mathlib version loaded?

[Eric Wieser]

If you open two vscode windows they the problem should go away

[Eric Wieser]

I don't think the extension can handle workspaces with multiple lean versions right now. Even though it probably should be able to handle "multi-root" workspaces, it's barely worth investing more effort into niche lean 3 tooling like that when lean 4 is around the ever-nearing corner