Zulip Chat Archive

Stream: new members

Topic: Setting up a Lean4 project that can use mathlib3/binport

Johan Commelin (Sep 27 2022 at 03:02):

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 (Sep 27 2022 at 03:08):

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.)

Last updated: Dec 20 2023 at 11:08 UTC