package for mathport?

Stream: mathlib4

[Yury G. Kudryashov]

Is it hard to turn mathport into an installable executable? Does it rely on relative paths?

I think about writing a build.nix file that installs a mathport command that does "the right thing": either runs on 1 file or on the current git project.

[Yury G. Kudryashov]

(then add a debian package so that Ubuntu instruction can be "add this PPA, install mathport, run it")

[Notification Bot]

2 messages were moved here from #mathlib4 > mathport recompiles mathlib by Yury G. Kudryashov.

[Mario Carneiro]

It doesn't rely on any hard-coded paths AFAIK, but it does rely on a lot of external files given to it via LEAN_PATH, config.json and the command line

[Mario Carneiro]

i.e. it needs mathlib4 oleans to be available somewhere on disk

[Yury G. Kudryashov]

Do you know why it rebuilds the parts of mathlib4 it depends on?

[Mario Carneiro]

with Compiling or Building?

[Mario Carneiro]

Compiling is expected, it has to actually produce an executable and so it has to compile relevant parts of mathlib into an object file, which is not something we cache because it is architecture dependent.

[Mario Carneiro]

Building should not happen if you ran lake exe cache get

[Mario Carneiro]

It should be pretty quick to "compile" mathlib because most files have no computational content so it's just compiling a bunch of empty C files

[Mario Carneiro]

Note that this is getting worse over time because mathport depends on Mathlib.Mathport.Syntax and the dependencies of this file keep growing as people implement more tactics that depend on more parts of mathlib

[Mario Carneiro]

(I would guess this spiked recently because the witt vector tactics got implemented)

[Yury G. Kudryashov]

Indeed, it's "Compiling". Thank you for the explanation!