Memory Allocation Failure Running mathport

Stream: lean4

[Naruyoko]

I'm trying to use mathport to migrate a project. I followed the steps in the README and got to the place run ./build/bin/mathport --make config-project.json Project::all. However, that command throws errors and nothing is put out.

I tried to remove all import from all.lean except a test file:

import test

With test.lean containing (taken from project setup docs)

import topology.basic

#check topological_space

Which produces the following (modulo the specific .olean file):

[visit] { package := "Project", mod3 := `all }
[visit] { package := "Leanbin", mod3 := `init.default }
[visit] { package := "Project", mod3 := `test }
[visit] { package := "Leanbin", mod3 := `init.default }
[visit] { package := "Mathbin", mod3 := `topology.basic }
porting Test

[mathport] START test

uncaught exception: failed to port Project:Test with imports [Leanbin.Init.Default, Mathbin.Topology.Basic]:
failed to open './Outputs/oleans/mathbin/Mathbin/Algebra/GroupWithZero/Semiconj.olean': Cannot allocate memory
Failed to port { package := "Project", mod3 := `test }

I am running this in a Linux VM. It has a bit less than 8 GiB of free RAM before running the command.

[Scott Morrison]

It's possible you need more RAM than that. If you tell me a branch that I can check out and then run a single command to test for you, I'm happy to run it on a larger machine.

[Naruyoko]

Thanks, I have it here. The stuff outside the directory is unrelated to the Lean project.

I wonder how much RAM is needed to run mathport. I guess it's loading all of mathlib.

[Naruyoko]

@Scott Morrison Hello, I'm just checking in. Can you try mathport from your computer?
I removed the unrelated files from the branch.

[Scott Morrison]

Can you tell me exactly what you'd like me to run? Ideally a code block with terminal commands that I can run in an empty directory. :-) I'm a bit busy today to work out the details otherwise.

[Naruyoko]

Thanks, I'll do so in a moment.

[Naruyoko]

I am now getting a different error... Now, if I have any imports besides import test, then I get the following error:

libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Lean.pp.beta' in the same module

Here is a script

[Utensil Song]

As now more people would try to port to Lean 4, maybe mathport as a docker image or a more lightweight bundle is easier to use across environments, or even better, a Github actions that produces a lean4 branch for the repo.

[Scott Morrison]

@Naruyoko sorry, this was due to a problem that we've just fixed in #7774. Can you make sure everything is using the very lastest Mathlib master, and try again?

[Naruyoko]

Oh, unfortunate timing... I'll try it again.

[Mario Carneiro]

It appears mathport master is broken as of today due to the same issue: https://github.com/leanprover-community/mathport/actions/runs/6583820317/job/17887403829

[Naruyoko]

I tried to use the updated version by adding a sed command to replace the commit hash for mathlib4 after cloning mathport like follows:

sed -i "s|23a69c77985689d9930944c79bbccecf66cffea0|{NEWER HASH}|" lake-manifest.json

Unfortunately, this doesn't work with either 3c0fc27 or aa0ff04, though this could just be an inappropriate way to update mathlib4.
At lake exe cache get, the console gets filled thousands of:

Warning: lake-packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
Warning: lake-packages/std/Std/Tactic/Relation/Symm.lean not found. Skipping all files that depend on it

I guess I'll have to try again tomorrow, thanks for the support.

[Naruyoko]

I reran mathport again today, and it worked this time. I was able to put the file in a new Lean 4 project have the language server recognize mathlib imports with a few minor fixes.
Thank you.