Porting Lean3 code to Lean4 with `Mathport`

Stream: lean4

[Anand Rao]

I would like to port some Lean3 code (not a part of mathlib3) over to Lean4, and I have been experimenting with the code in Mathport to see if I can use it for this purpose. Here is what I have done so far:

• Run lean --tlean --ast --make --recursive src/ in the Lean3 repository to build the intermediate .tlean and .ast.json files
• Edit the pathConfig.packages field of the config.json file to point to the above repository containing the Lean3 code
• Add ./Outputs/oleans/<repo_name> to pathConfig.lean.leanPath in config.json
• Build the Mathport package with lake build and run ./build/bin/mathport config.json <PkgName>::<filename>

I was hoping that these changes would suffice, but trying to port a file this way resulted in the error uncaught exception: [resolveMod3] failed to resolve 'init'. Some investigation revealed that the headers of the .tlean files all contained the line IMPORT 1 init -1, which tries to import a file called init.lean and results in the error.

I have tried a few ways to get around this, but none of them have worked. I would really appreciate any help in modifying these steps to make the porting work.

[Gabriel Ebner]

Does mathport --make config.json .... work?

[Gabriel Ebner]

Without the make it will only port the specified module (which fails since it hasn't ported init yet)

[Anand Rao]

Unfortunately the error still remains after running with the --make flag.

Here are the changes I made in more detail to the .config.json (for concreteness, I am now trying this with the lean-community/tutorials repository, which I have copied to the folder ./sources):

     "pathConfig": {
         "outRoot": "Outputs",
         "packages": {
-            "Leanbin": "sources/lean/library",
-            "Mathbin": "sources/mathlib/src"
+            "Tutorialbin": "sources/tutorials/src"
         },
         "leanPath": [
-            "./lean_packages/mathlib/build/lib",
-            "./Outputs/oleans/leanbin",
-            "./Outputs/oleans/mathbin"
+           "./lean_packages/mathlib/build/lib",
+            "./Outputs/oleans/tutorialbin"
         ]

The command I entered was: ./build/bin/mathport --make config.json Tutorialbin::exercises.00_first_proofs
and the error I got was:

[visit] { package := "Tutorialbin", mod3 := `exercises.«00_first_proofs» }
uncaught exception: [resolveMod3] failed to resolve 'init'

[Anand Rao]

Gabriel Ebner said:

Without the make it will only port the specified module (which fails since it hasn't ported init yet)

Does init here refer to a specific file in the repository I am porting? I could not find a file called init.lean in the tutorials repository, which I why I was puzzled by the error message.

[Henrik Böving]

init in Lean 3 or Init in Lean 4 is the prelude so the files that implicitly always get imported into any Lean file, its part of the compiler source.

[Anand Rao]

I see, thanks.

[Gabriel Ebner]

Oh you need to keep the old entries in config.json

[Anand Rao]

Okay. Do I also need to generate the .tlean and .ast.json pre-data for the lean and mathlib folders (say via make predata)?

[Gabriel Ebner]

Yes!