mathport on external projects

Stream: mathlib4

[Scott Morrison]

@Mario Carneiro, I'm having trouble when running mathport on external projects, per the instructions I wrote up on the projects_instructions branch of mathport.

When it is time to run lean --make --recursive --ast --tlean src in the external project, it recompiles all of mathlib back in ..mathport/sources/mathlib/ (even though I have run ./download-release.sh and then in sources/mathlib/ run leanproject get-cache, and verified that we have .olean, .tlean, and .ast.json files.

I don't remember this happening (it's very time consuming!) when we ran on MIL last week. Do you have an idea why this might be happening?

[Mario Carneiro]

I know that this happens frequently and I am not sure how to fix it. I have generally resorted to hacks to make it accept the oleans

[Mario Carneiro]

Could it be that you are using a different version of lean in the external project than the one in mathlib?

[Scott Morrison]

We had bumped the project to recent mathlib, and it didn't occur to me to check the lean version separately.

[Mario Carneiro]

the mathport makefile uses some elan overrides to make sure we always use the right lean 3 version in the relevant directories

[Scott Morrison]

@Peter Nelson and I did eventually get his lean-matroids project "ported" via mathport to Lean 4.

If anyone else would like to try this, I'm happy to help out.

It's easiest if your project satisfies the following conditions, although many can be worked around:

• Depends on a very recent mathlib3.
• Uses the latest lean3 version i.e. leanprover-community/lean:3.51.1.
• Does not use relative imports.
• Compiles cleanly with leanproject mk-all && leanproject build.
• Has all source code under src/.

The current instructions are https://github.com/leanprover-community/mathport/blob/687878f207dacb3663d8738be7f8fc418adebd67/README.md (i.e. the README.md file from https://github.com/leanprover-community/mathport/pull/237 ). I'd be very happy to hear someone's results of trying to run it themselves, or do another repository myself, if anyone would like to volunteer a project satisfying the conditions above.

[Mario Carneiro]

Does not use relative imports.

This should be fixed now

[Mario Carneiro]

Also the "oneshot" mode should work with projects now

[Mario Carneiro]

although you are still better off using the project instructions in most cases