Lean and GitHub

Stream: general

[Daniel Park]

Hello!

This is my very first time to use Lean for proving theorems. I was able to set up a new project using mathlib on my local machine, but I want to save and host my project on GitHub as well. Is there a way to do this or a tutorial I can follow on the Lean documentations?

Thank you!

[Jeremy Avigad]

I follow these instructions:
https://docs.github.com/en/migrations/importing-source-code/using-the-command-line-to-import-source-code/adding-locally-hosted-code-to-github

[Julian Berman]

Welcome. I interpreted your question as being "I'm new to Git + GitHub" so I wrote the below. Not sure if that was the intention:

Git and GitHub are in some ways 1) a rabbithole (there's a huge amount you could learn about them) and 2) totally general and not only useful for Lean + Mathlib + math.
The two of those mean that I think your best bet is to take a simple introductory tutorial for GitHub and try that, and if you need to learn anything after that you'll pick it up afterwards as you go.
Here are 2 resources for that:

• https://docs.github.com/en/get-started/start-your-journey/hello-world
• https://code.visualstudio.com/docs/sourcecontrol/intro-to-git

The first one is the first "how to use GitHub" tutorial. The second is for VSCode, your editor. Both of those you can likely go through as quickly or slowly as you choose.

Jeremy's suggestion is I'm sure great if the question was intended to be less introductory and you already kind of know what you want!

[Daniel Park]

Thank you so much! Also, is it possible to initialize a new Lean project with Mathlib on a code base that I that I was working? For instance, is it possible to change the structure of the project that VScode initially generated for me?

[Julian Berman]

You mean you want to add Mathlib as a dependency on a project that doesn't already depend on it? Or otherwise can you clarify what you mean by initializing a new project with Mathlib? Is this a directory you ran lake init ... on or lake new ... to create?

[Daniel Park]

Julian Berman said:

You mean you want to add Mathlib as a dependency on a project that doesn't already depend on it? Or otherwise can you clarify what you mean by initializing a new project with Mathlib? Is this a directory you ran lake init ... on or lake new ... to create?

Yes, adding Mathlab as a dependency on the project that doesn't depend on Mathlib previously. I did not run any lake commend to create this directory because I wanted to add Lean code to my previously created project.

[Daniel Park]

Also, if you don't mind, can you please explain what the lake command does or hand me the documentation related to it?

[Bulhwi Cha]

Can you show us your lakefile.lean or lakefile.toml?

[Bulhwi Cha]

Here's the lakefile.lean configuration for my lean-notes project:

My lakefile.lean

import Lake
open Lake DSL

package «lean-notes» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩
  ]
  -- add any additional package configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0"

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "main"

@[default_target]
lean_lib «Notes» where
  -- add any library configuration options here

Add the following lines to your lakefile.lean:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0"

Then, run lake update from the root directory of your project.