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