Setting up a Lean4 project that can use mathlib3/binport

Stream: new members

[Johan Commelin]

Assuming that you want to work on helping with the porting process, the most important thing atm is to get tactic ported, which doesn't really require mathport or binport.
If you really want to set up the mathport repo, then you'll have to wait for another answer, because I can't help with that.

[Thomas Murrills]

Ok, totally new here—when you say "get tactic ported", is that one of the by-hand porting projects we need to do for mathlib4? (I'm guessing it's what's going on in this topic? Or is my guess off?)

I do want to help with the porting process, and I'd like to help with porting tactics if I can—it might be a good way to learn! But separately, I'm also just looking to start formalizing some particular math in Lean 4 that will make use of mathlib imports (for which I assume I only need the binaries). (I eventually found this thread and asked a more specific question there after attempting what I could.)