trying to run mathport

Stream: mathlib4

[David Renshaw]

I did:

1. clone https://github.com/leanprover-community/mathport
2. make mathbin-source
3. make lean3-source
4. make lean3-predata
5. make mathbin-predata (took 45 minutes)
6. make port-lean

Everything succeeded until the last step, whose output ends with

...
> /home/dwrensha/.elan/toolchains/leanprover--lean4---nightly-2021-10-28/bin/leanc -c -o ./build/ir/MathportApp.o ./build/ir/MathportApp.c -O3 -DNDEBUG
> /home/dwrensha/.elan/toolchains/leanprover--lean4---nightly-2021-10-28/bin/leanc -o ./build/bin/mathport ./build/ir/Mathport/Binary/TranslateExpr.o ./build/ir/Mathport/Binary/Number.o ./build/ir/Mathport/Binary/TranslateName.o ./build/ir/Mathport/Bridge/Rename.o ./build/ir/Mathport/Syntax/Translate/Tactic/Basic.o ./build/ir/Mathport/Syntax.o ./build/ir/Mathport/Bridge/Path.o ./build/ir/Mathport/Bridge/Config.o ./build/ir/Mathport/Syntax/Translate.o ./build/ir/Mathport/Util/System.o ./build/ir/Mathport/Binary/NDRec.o ./build/ir/Mathport/Binary/Basic.o ./build/ir/Mathport/Syntax/Translate/Basic.o ./build/ir/Mathport/Util/Json.o ./build/ir/Mathport/Util/Parse.o ./build/ir/Mathport/Binary/Apply.o ./build/ir/Mathport/Syntax/Translate/Tactic.o ./build/ir/Mathport/Binary.o ./build/ir/Mathport/Syntax/Translate/Tactic/Mathlib.o ./build/ir/Mathport/Util/String.o ./build/ir/Mathport/Util/Name.o ./build/ir/Mathport/Syntax/Translate/Parser.o ./build/ir/Mathport/Binary/Decode.o ./build/ir/Mathport/Syntax/Data4.o ./build/ir/Mathport.o ./build/ir/Mathport/Binary/EnvModification.o ./build/ir/Mathport/Util/While.o ./build/ir/Mathport/Syntax/Parse.o ./build/ir/Mathport/Syntax/Translate/Notation.o ./build/ir/Mathport/Util/Misc.o ./build/ir/Mathport/Syntax/Translate/Attributes.o ./build/ir/Mathport/Util/Import.o ./build/ir/Mathport/Binary/Heterogenize.o ./build/ir/MathportApp.o ./build/ir/Mathport/Syntax/Translate/Tactic/Lean3.o ./build/ir/Mathport/Binary/ParseTLean.o ./build/ir/Mathport/Syntax/AST3.o ./lean_packages/mathlib/./build/lib/libMathlib.a -rdynamic
LEAN_PATH=./build/lib:./lean_packages/mathlib/build/lib:./Lib4/leanbin/build/lib ./build/bin/mathport config.json Leanbin::all >> Logs/mathport.out 2> Logs/mathport.err
make: *** [Makefile:90: port-lean] Error 1

[David Renshaw]

$ cat Logs/mathport.err
uncaught exception: failed to import environment for Leanbin:Init.Logic with imports [Leanbin.Init.Core]: unknown package 'Leanbin'

[David Renshaw]

what am I doing wrong?

[Gabriel Ebner]

We should remove the port-lean target.

[Gabriel Ebner]

Just run

./build/bin/mathport --make config.json Leanbin::all

[Gabriel Ebner]

Btw there's also a download-predata.sh script if you don't want to wait 45 minutes.

[David Renshaw]

I think the --make flag does not exist?

$ ./build/bin/mathport --make config.json Leanbin::all
uncaught exception: no such file or directory (error code: 2)
  file: --make

[David Renshaw]

$ ./build/bin/mathport config.json Leanbin::all
...
[visit] { package := "Leanbin", mod3 := `init.default }
[visit] { package := "Leanbin", mod3 := `tools.debugger.util }
[visit] { package := "Leanbin", mod3 := `tools.debugger.cli }
[visit] { package := "Leanbin", mod3 := `tools.debugger.util }
uncaught exception: failed to import environment for Leanbin:Init.Logic with imports [Leanbin.Init.Core]: unknown package 'Leanbin'

[Gabriel Ebner]

Do you have the latest version of mathport?

[David Renshaw]

heh, good point. I seem to still be pointed at https://github.com/dselsam/mathport.git

[David Renshaw]

:face_palm:

[David Renshaw]

Updated my remote to be https://github.com/leanprover-community/mathport

[David Renshaw]

repulled, did git clean -xffd, and launched a new build...

[David Renshaw]

success!

[Alexander Bentkamp]

I tried to run mathport using GitHub Actions: https://github.com/abentkamp/mathport/runs/8265032056

After two hours of make mathbin-predata, I get:

cd sources/mathlib && lean --make --recursive --ast --tlean src
make: *** [Makefile:75: mathbin-predata] Killed
Error: Process completed with exit code 2.

Any ideas what could cause this?

[Gabriel Ebner]

Mathlib is so grandiose that it cannot be be built on standard github actions runners. :smile:

[Gabriel Ebner]

(I believe the machine is running out of memory.)

[Gabriel Ebner]

You should use the download-predata script to get the mathlib build handcrafted by artisan servers in Pittsburgh. (You removed that part in the CI scripts on your branch.)

[Alexander Bentkamp]

Hm, I'd like to be able to port my own material, so using download-predata is not an option I think.

[Alexander Bentkamp]

Also, I've just tried it on my own machine and I am still running into the same problem. How much memory do I need for this?

[Alexander Bentkamp]

Ok, I see that one needs a lot of memory. I restarted the process while observing the memory status and I can already see it filling up really fast :-)

[Gabriel Ebner]

Hm, I'd like to be able to port my own material, so using download-predata is not an option I think.

This depends.. is your stuff in mathlib?

[Alexander Bentkamp]

No. Not yet at least :-)

[Alexander Bentkamp]

Would it be an option to port lean + mathlib + a third project while reusing the existing predata for mathlib? I have no idea how to set this up though.

[Gabriel Ebner]

Yes, that should be possible as long as your project works with one of the mathlib versions on https://github.com/leanprover-community/mathport/releases

[Alexander Bentkamp]

ok, I'll try that then.

[Gabriel Ebner]

As for how to set that up:

1. Copy&paste the mathbin-predata/port-mathbin targets in the makefile to myproject-predata/port-myproject.
2. Add your myproject to config.json in all the required places.
3. Run ./download-predata.sh predata-nightly-YYYY-MM-DD where YYYY-MM-DD is the mathlib version your project works with. Or alternatively ./download-release.sh nightly-YYYY-MM-DD if you also want the ported oleans.
4. Run make myproject-predata
5. Run make port-myproject

[Alexander Bentkamp]

Thanks a lot, it works!

What's the best way to import the binport into a Lean4 project now?

[Gabriel Ebner]

Oh, you mean with the files you've just ported? Good question. I think you need to copy&paste mathlib3port.

[Alexander Bentkamp]

Ok :-)