Tutorial for mathport

Stream: general

[Martin Dvořák]

I want to use mathport for my own project (to be ported from Lean 3 to Lean 4). Is there any tutorial for that?

[Riccardo Brasca]

https://github.com/leanprover-community/mathport#running-on-a-project-other-than-mathlib

[Martin Dvořák]

Can it be done on Windows please?

[Mauricio Collares]

If you do have WSL and Windows instructions aren't available, you can probably use the Microsoft Store to install Ubuntu and follow the Linux instructions.

[Ruben Van de Velde]

You may need to go boldly where no mathport run has gone before :)

[Eric Wieser]

Another option is to run mathport within a gitpod instance

[Martin Dvořák]

Can I use a Gitpod instance made from the mathlib4 repository for that?

[Eric Wieser]

No, you should use the mathport gitpod instance

[Martin Dvořák]

From here?
https://github.com/leanprover-community/mathport
Any idea whether Codespaces works as well as Gitpod for this purpose?

[Eric Wieser]

Well, there is gitpod configuration but no codespace configuration

[Eric Wieser]

So if you use codespaces you're starting from a clean linux machine, rather than one with everything pre-installed

[Bolton Bailey]

Will mathport port my tactics as well as my definitions and lemmas?

[Johan Commelin]

No, tactics have to be ported by hand

[Johan Commelin]

Because the meta framework changed radically

[Bolton Bailey]

What about if I have sorrys, will that cause a problem?

[Martin Dvořák]

Mauricio Collares said:

If you do have WSL and Windows instructions aren't available, you can probably use the Microsoft Store to install Ubuntu and follow the Linux instructions.

I followed the first step of the tutorial for Debian/Ubuntu in my WSL Ubuntu.
It continues with "In the mathport folder".
What mathport folder does it talk about?

[Bolton Bailey]

Presumably the folder you have cloned mathport into

[Martin Dvořák]

This step is not preceded by clone the mathport repository, is it?

[Bolton Bailey]

I guess the instructions assume you have already cloned the repo.

[Martin Dvořák]

Is it alright if I first downloaded the dependencies, then I clone the repo and do lake exe cache get afterwards?

[Bolton Bailey]

Yes that should be fine

[Bolton Bailey]

Ok I am trying to get this working but I get an error on the make source instruction, so I am switching to gitpod. But how do I clone my own repository into the gitpod? Gitpod says "write access to repository not granted". edit nvm i'm dumb my repo was private

[Bolton Bailey]

make source on my local machine gives me

boltonbailey@starlight mathport % make source
mkdir -p sources
if [ ! -d "sources/mathlib/.git" ]; then \
        cd sources && git clone --depth 1 https://github.com/leanprover-community/mathlib.git; \
    fi
Cloning into 'mathlib'...
remote: Enumerating objects: 4015, done.
remote: Counting objects: 100% (4015/4015), done.
remote: Compressing objects: 100% (3911/3911), done.
remote: Total 4015 (delta 91), reused 678 (delta 53), pack-reused 0
Receiving objects: 100% (4015/4015), 12.08 MiB | 7.66 MiB/s, done.
Resolving deltas: 100% (91/91), done.
cd sources/mathlib && git clean -xfd && git fetch && git checkout "origin/master" --
Note: switching to 'origin/master'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 1b089e3 chore(*): add mathlib4 synchronization comments (#19211)
cd sources/mathlib && echo -n 'mathlib commit: ' && git rev-parse HEAD
mathlib commit: 1b089e3bdc3ce6b39cd472543474a0a137128c6c
cd sources/mathlib && leanpkg configure && ./scripts/mk_all.sh
configuring mathlib 0.1
cd sources/mathlib/archive && git ls-files \
        | sed -n '/\.lean/ { s=\.lean$== ; s=/=».«=g; s=^=import «= ; s=$=»= ; p }' > all.lean
sed: 1: "/\.lean/ { s=\.lean$==  ...": extra characters at the end of p command
make: *** [mathbin-source] Error 1

[Bolton Bailey]

This repo is only 1000 lines of code, is it going to be easier just to make a new lean 4 repo and translate everything by hand?

[Ruben Van de Velde]

Probably not

[Ruben Van de Velde]

Are you on a mac? This relies on GNU sed

[Bolton Bailey]

Yes I am on a mac

[Bolton Bailey]

Is this something I have to download?

[Bolton Bailey]

sed seems to be installed

[Ruben Van de Velde]

Yeah, but it's the wrong sed. See thread from here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Updating.20.60mathlib3port.60/near/302779660

[Bolton Bailey]

Ok but in that thread Scott says they fixed it to be macos compatible.

[Bolton Bailey]

Ok whatever the difference is, switching sed for gsed in the Makefile did seem to work, thank you.

[Martin Dvořák]

I followed till make build which gave me:

(...)
[1787/1955] Compiling Mathlib.Algebra.Algebra.Equiv
[1791/1955] Compiling Mathlib.LinearAlgebra.Prod
[1791/1955] Compiling Mathlib.Algebra.Algebra.Pi
[1793/1955] Compiling Mathlib.Algebra.Star.Module
[1795/1955] Compiling Mathlib.Data.Matrix.Basic
[1797/1955] Compiling Mathlib.Data.Matrix.Notation
[1799/1955] Compiling Mathlib.Mathport.Syntax
make: *** [Makefile:37: build] Error 1

[Martin Dvořák]

Repeating make build gives me:

lake build
[0/1955] Compiling FFI.c
error: > c++ -c -o ./build/c/ffi.o ./Mathport/FFI.cpp -I /home/madv/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/include -fPIC
error: stderr:
could not execute external process 'c++'
error: external command `c++` exited with code 255
make: *** [Makefile:37: build] Error 1

[Mauricio Collares]

You seem to be missing some basic deps. Try apt install build-essential clang

[Martin Dvořák]

[resolved]

[Bolton Bailey]

I was able to run mathport, but a ton of lemmas that needed to be renamed didn't get renamed. What gives?

[Bolton Bailey]

(these are definitely lemmas from files that have been ported polynomial.div_X_mul_X_add is an example.)

[Mario Carneiro]

Bolton Bailey said:

Ok but in that thread Scott says they fixed it to be macos compatible.

That fix was for update.sh, there is now an additional use of sed in the makefile. @Scott Morrison what did you do to fix it?

[Mario Carneiro]

@Bolton Bailey said:

I was able to run mathport, but a ton of lemmas that needed to be renamed didn't get renamed. What gives?

Do you have an example? When used in certain positions mathport has difficulty doing the rename (I see this mainly in tactic arguments and dot notation)

[Bolton Bailey]

PolyLemmas.lean
Here is an example of the mathport output, with many instances of nat_degree_le_nat_degree which should be natDegree_le_natDegree

[Bolton Bailey]

Here is the corresponding lean3 input
poly_lemmas.lean

[Bolton Bailey]

To fix the makefile for mac I just replaced every sed I could find with gsed

[Mario Carneiro]

there are no #align statements in this output, which means either you have a custom configuration or a very old mathport

[Mario Carneiro]

I think the issue here is that the names aren't being resolved because of the namespace

[Mario Carneiro]

e.g. it doesn't know nat_degree_le_nat_degree means polynomial.nat_degree_le_nat_degree and so can't use the #align line for it

[Bolton Bailey]

I just cloned mathport this morning. I don't know what I could've done to give it a custom configuration.

[Bolton Bailey]

Mathport version is 38063ec2

[Bolton Bailey]

Align statement is there in mathlib 4 https://github.com/leanprover-community/mathlib4/blob/6533094a68393dbab56cfb3ff2bed55c6978a84d/Mathlib/Data/Polynomial/Degree/Definitions.lean#L235-L237

[Bolton Bailey]

ok, I guess you're saying it's because there's a namespace in my code, that makes sense

[Scott Morrison]

I have adjusted the sed invocation in https://github.com/leanprover-community/mathport/pull/243 so that hopefully it works with all versions of sed. (Joint work with chatgpt, tested on mac with both gsed and sed.)

[Mario Carneiro]

is it the semicolon at the end or the use of / separators that makes the difference?

[Mario Carneiro]

@Bolton Bailey is "redundantAlign": true in your config.json?

[Bolton Bailey]

"redundantAlign": true in my config.json, but false in my config-project.json

[Scott Morrison]

It seems to be the / separators.

[Bolton Bailey]

Johan Commelin said:

No, tactics have to be ported by hand

Ok what is the best practice for doing this then? Mathport tells me that I have to build my project beforehand, but my project has a tactic that is custom-written and takes a long time to run. Will it cause problems if I just comment out this tactic invocation and replace it with sorry?

[Bolton Bailey]

(I guess I'm asking a question with no good answer, sorry about that)

[Scott Morrison]

@Bolton Bailey, you need to build your project in Lean3 before hand, but that shouldn't be a problem. You could adjust mathport to know about the syntax of your tactic and how to translate calls to it (as we do for all the mathlib3 tactics) (note this is not translating the tactic itself: just invocations of it!). But unless you have a lot of calls with complicated syntax, I would recommend skipping this step. Just replace all the my_tactic calls in your project with sorry, run mathport, fix up the output, reimplement my_tactic from scratch in Lean 4, then finally restore the sorrys back to my_tactic.

[Bolton Bailey]

Ok seems sensible, thanks for the advice

[Martin Dvořák]

After running mathport, we must:
(1) Change all "import Mathbin" to "import Mathlib".
(2) Reïmplement custom tactics in Lean 4 by hand.
Is there anything else everybody has to do?

[Ruben Van de Velde]

Add the new file to Mathlib.lean or equivalent

[Johan Commelin]

See the scripts/start_port.sh script in mathlib4.