MathLib installing

Stream: new members

[Ming Li]

My Lean4 and Mathlib4 are doing fine on VS code. Now I got troubles on running Lean3 and Mathlib. #eval 2+3 is fine until import tatic.linarith The error message is "unknown package 'tactic'".

[Mario Carneiro]

are you trying to write lean 3 or lean 4 code?

[Mario Carneiro]

IIRC the extension detects whether it is supposed to be lean 3 or lean 4 based on whether you have a leanpkg.toml file or a lakefile.lean

[Mario Carneiro]

if it's just a random file not in a project the extension can't tell if you want lean 3 or lean 4, so you will have to disable the lean 4 extension to make that work

[Kevin Buzzard]

If you're using lean 4 (which you should be) then indeed that import is invalid.

[Ming Li]

Yes, some codes in lean 3 is not working in lean4. So I am trying to get familar with their difference. Indeed, leanpkg and lake file are respectively given in lean3 and lean4. In vscode, the used program is shown on the right bottom corner. I also notice that my folder mathlib4 takes 4GB and mathlib takes less than 1GB. And import.. in lean3, it often shows loading...

[Mario Carneiro]

yes, mathlib4 is a lot bigger. Mine is 6.6 GB, although that also includes 1.2 GB of .git and 1.06 GB of .cache (I think that was from a test)

[Kevin Buzzard]

Yes lean 3 and lean 4 are completely incompatible and lean 4's version of (compiled) mathlib is much bigger.

[Ming Li]

Indeed, even mathlib, i need to keep mathlib4 only for lean4. Is there any method I can transform lean3 code into lean4-code, by porting?

[Kevin Buzzard]

We translated mathlib from lean 3 to lean 4 using a tool called mathport which you can find on GitHub or by searching here

[Ming Li]

Thanks. Trying...
quote“
In the mathport folder:
lake exe cache get
make build This step is somewhat expensive as we need to compile (not just build) all of the dependencies of tactics.
make source
“
lake or make?

Kevin Buzzard said:

We translated mathlib from lean 3 to lean 4 using a tool called mathport which you can find on GitHub or by searching here

[Kevin Buzzard]

Assume the instructions are correct. They've been used many times.

[Ming Li]

Can Mathlib4 be installed at a common google drive so that it can be used at different terminals at different time?

[Notification Bot]

This topic was moved here from #maths > MathLib installing by Scott Morrison.