Installation demo

Stream: mathlib4

[Patrick Massot]

I think it would be nice to record a video showing someone installing Lean 4 and mathport from scratch and start doing something useful for mathlib4 such as opening a ported file and writing a GitHub issue, and then maybe even implementing an easy tactic. Many people, including me, are scared of the process and feel they don't have the right skills, but we know that the port is currently missing manpower. We could even record a zoom session where a couple of clueless users ask question while watching the expert doing this.

[Heather Macbeth]

Along these lines, I think Scott's "how to make a PR" video from 2 years ago has really paid dividends, we still link newcomers to it all the time.

[Arthur Paulino]

I am unable to run mathport on my computer due to resources constraints. I would love to see it in action :eyes:

[Patrick Massot]

I don't think anyone runs mathport except CI machines.

[Gabriel Ebner]

I am unable to run mathport on my computer due to resources constraints. I would love to see it in action

Running mathport on a single file is something you can easily do locally (only needs a few gigabytes of hard disk space), just do the following in the mathport directory:

./download-release.sh nightly-2022-03-09
lake build
./build/bin/mathport config.json Mathbin::algebra.opposites

This cheats a bit by getting the CI outputs for everything but algebra.opposites, but it's what I do whenever I test something in mathport.

But there's not much to do in mathport, except for keeping it up to date (for example with the ever changing tactic syntax https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+label%3Amodifies-tactic-syntax+is%3Aclosed).

[Mauricio Collares]

Is it possible to set things up so you can just open a synported file in the editor after running those commands? My emacs complains when I do that, even after setting the LSP workspace root (probably because there's no lakefile in the mathbin folder).

[Mauricio Collares]

I just want to see a list of errors for a particular file in a nice format, in case I'm #xy-ing things.

[Gabriel Ebner]

I think the easiest way to do that is to copy the file to mathlib3port and open it there.