How to run a old lean3 project?

Stream: new members

[chenjulang]

How to run a old lean3 project? Or how to translate it into lean4 to run?

Like this: https://github.com/kendfrey/rubiks-cube-group

[Ruben Van de Velde]

https://leanprover-community.github.io/leanproject.html

[chenjulang]

I dont know how to solve this:
image.png

[chenjulang]

I'm going to translate the files into lean4 myself...

[Kevin Buzzard]

You know about the program which attempts to do this automatically? https://github.com/leanprover-community/mathport (but if you cannot compile the project on your machine, you might also have problems using mathport)

[chenjulang]

I'll try , thank you :heart:

[chenjulang]

I tried oneshot, but failed at this command"make lean3-source":
image.png

[chenjulang]

Any one succeed before? If you have time, these 4 files needs help:

[chenjulang]

array_group.lean
array_perm_group.lean
fin_group.lean
rubiks_cube.lean

[Mauricio Collares]

brew install gmp could help with that, but Lean 3 probably wants x86 GMP, so you probably need to use x86 brew

[chenjulang]

I'll try

[chenjulang]

yeah, Still Error
image.png
i dont know how

[Mario Carneiro]

@chenjulang I tried porting your files myself, but import algebra.group fails. Step 0 of mathport is to upgrade to the latest lean 3

[chenjulang]

em..

[chenjulang]

i could not find the way to uninstall my lean4 and install lean3

[Mario Carneiro]

no need, they coexist

[Mario Carneiro]

the procedure for updating lean 3 is to set your lean-toolchain to match that of mathlib

[Mario Carneiro]

(and make a project if you haven't already, leanproject new foo should do it IIRC)

[Ruben Van de Velde]

I'll see if I can upgrade mathlib3 in the next little bit

[chenjulang]

em... I got a new problem with "leanproject new foo":
image.png

[Mario Carneiro]

leanproject +version new foo where version is the appropriate version of lean 3

[Mario Carneiro]

er, no leanproject isn't an elan wrapper

[Mario Carneiro]

elan toolchain override <version> in the folder you are running the command in I guess?

[chenjulang]

no idea..
image.png

[Mario Carneiro]

version should be leanprover-community/lean:3.51.1

[Mario Carneiro]

elan override set leanprover-community/lean:3.51.1
leanproject new foo
elan override unset
cd foo
leanproject build

[chenjulang]

OK, i'll try

[chenjulang]

I Failed in the first step :sweat_smile: : "elan toolchain override set leanprover-community/lean:3.51.1"
image.png

[Mario Carneiro]

sorry, my fault, it's just elan override not elan toolchain override

[chenjulang]

OK

[chenjulang]

elan override set 3.51.1 ?
image.png

[chenjulang]

downloading...

[chenjulang]

A problem, it is downloading from lean4 by default?:
image.png

[Mario Carneiro]

I think the first one looked the most promising

[chenjulang]

image.png
I failed ,but when i list, i have installed lean3 somehow?

[Mauricio Collares]

Mario Carneiro said:

elan toolchain override set leanprover-community/lean:3.51.1
leanproject new foo
elan toolchain override unset
cd foo
leanproject build

Did you try the exact commands Mario suggested?

[chenjulang]

No, the first line gets a error.

[Mario Carneiro]

minus the toolchain part

[Mario Carneiro]

elan override set leanprover-community/lean:3.51.1 didn't fail

[Mario Carneiro]

it wasn't able to parse the version for display purposes, but that doesn't really matter

[chenjulang]

OK

[Mario Carneiro]

@Sebastian Ullrich did elan lose the ability to parse lean 3 version strings?

[chenjulang]

I Failed the second step :laughing: "leanproject new foo"..
image.png

[Mario Carneiro]

ah okay so that's the same issue as with mathport, it seems like you can't run lean at all, you are missing some system dependencies?

[chenjulang]

I can run lean4 projects , in this M1 Macbook ,by the way

[Mario Carneiro]

does lean --version work?

[Mauricio Collares]

Presumably you've used Lean 3 on this machine (to write the files you want to port, for example). Do you have to do anything special to use it without getting an error message like the one above? Or are the files written by someone else?

[chenjulang]

someone else

[Mauricio Collares]

Ah, got it

[chenjulang]

i never use lean3

[chenjulang]

:joy:

[chenjulang]

image.png
I can use lean4.

[Mauricio Collares]

Follow these instructions to install x86 brew: https://gist.github.com/progrium/b286cd8c82ce0825b2eb3b0b3a0720a0

[Mauricio Collares]

Then use x86 brew to install gmp

[chenjulang]

OK

[Mario Carneiro]

are you on an M1 mac?

[chenjulang]

YES

[Mario Carneiro]

you may find https://leanprover-community.github.io/lean3/install/macos.html useful

[Mario Carneiro]

Specifically, elan – which is installed as part of the above instructions – will not be able to fetch Lean binaries on these devices if installed the normal way.

oh

[chenjulang]

So?I'm confused

[Mario Carneiro]

follow the instructions there, in the "M1 macs" section

[chenjulang]

OK, do i need to intall x86 brew? by the way?

[Mauricio Collares]

Does mathport have a gitpod config set up? Might be easier for a one-time effort

[Mauricio Collares]

chenjulang said:

OK, do i need to intall x86 brew? by the way?

Yes, but but Mario's instructions do that too and they're more detailed. Just follow his instructions and ignore mine.

[Mario Carneiro]

I think @Eric Wieser might have set something like that up? I'm a total noob wrt docker / gitpod stuff

[chenjulang]

Mauricio Collares said:

chenjulang said:

OK, do i need to intall x86 brew? by the way?

Yes, but but Mario's instructions do that too and they're more detailed. Just follow his instructions and ignore mine.

thanks

[Mario Carneiro]

(also it's a bad day to try mathport, the last mathlib4 upgrade broke so I'm temporarily without a working setup until the next nightly)

[chenjulang]

Oh , bad luck

[Ruben Van de Velde]

https://github.com/Ruben-VandeVelde/rubiks-cube-group has it updated to latest mathlib3

[chenjulang]

Now i have intalled gmp . I can succeed in command "make lean3-source".
But in the last step "make oneshot", still problem:
" failed to resolve 'init'"
image.png

[chenjulang]

For example , i try to translate "mathlib/archive/wiedijk_100_theorems
/solution_of_cubic.lean" in lean3 into Lean4, and get this error again:
image.png

[Ruben Van de Velde]

That's not the problem. The problem is all the build errors above that. Did you use the code and mathlib version I linked?

[chenjulang]

Oh, i only use the code

[chenjulang]

But how to use the "mathlib version" you linked?

[Eric Wieser]

While not relevant to the current issues, you might find https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks.lean interesting

[chenjulang]

Yeah , i knew it

[chenjulang]

But no proofs in that repository, only html

[chenjulang]

I thought mathport only needs a single file to translate into lean4, right?
image.png
So how to use the mathlib you linked?

[Quoting…]

[chenjulang]

I'll try again

[chenjulang]

Now i succeed translating the single files, but some compilation errors occurred:
image.png

[chenjulang]

the "imports" always lacks "Mathlib."
image.png

[chenjulang]

I'll try whole project translating.

[Mauricio Collares]

Mathport output definitely requires some manual fixing

[Mario Carneiro]

yeah, if you got it to produce lean 4 looking files then mathport succeeded, any remaining errors that occur in the file have to be handled manually

[Mario Carneiro]

there is a regex in mathlib4 that does some easy fixups to mathport output (which should be upstreamed)