leanproject and branches

Stream: new members

[Heather Macbeth]

I have installed leanproject and am trying to create a new branch off master (see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bounded.20continuous.20functions/near/197060652). Am I supposed to do this directly with git, or is this process wrapped in a leanproject command (the way that the cloning of projects is)?
I tried to follow the intructions at mathlib-tools readme for simultaneously getting a project and creating a new branch, but when I tried (as instructed) the command leanproject get -b project_name:branch_name (with project_name and branch_name appropriately instantiated), I received the error message Error: no such option: -b.

[Johan Commelin]

@Heather Macbeth You should use git directly.

[Johan Commelin]

Or at least not leanproject. Are you familiar with git? If you are using vscode, you can use it's point-and-click interface to git, so that you don't have to learn yet another tool.

[Johan Commelin]

Heather Macbeth said:

I tried to follow the intructions at mathlib-tools readme for simultaneously getting a project and creating a new branch, but when I tried (as instructed) the command leanproject get -b project_name:branch_name (with project_name and branch_name appropriately instantiated), I received the error message Error: no such option: -b.

This sounds like you have an older version of leanproject, what does leanproject --version say?

[Johan Commelin]

On the other hand... if you just installed, you ought to have the latest version.

[Johan Commelin]

@Heather Macbeth Note that, if you want to push to a branch of the community repo, you need to tell us your github username. (Until that point, you can always create a fork of mathlib, make your change there, and make a pull request from your fork to the main repo.)

[Shing Tak Lam]

Johan Commelin said:

Heather Macbeth Note that, if you want to push to a branch of the community repo, you need to tell us your github username. (Until that point, you can always create a fork of mathlib, make your change there, and make a pull request from your fork to the main repo.)

I thought .oleans are only built for branches, not forks? So it'd probably be better to PR from a branch I think.

[Johan Commelin]

But this only matters for comfort and convenience for yourself. And when you change only 1 file, you don't even notice.

[Johan Commelin]

But for bigger PRs its "crucial"

[Heather Macbeth]

Johan Commelin said:

On the other hand... if you just installed, you ought to have the latest version.

Humph. I was on version 0.0.5; I must have caught it just before the release of 0.0.6 on Saturday. Thanks, that should help! I'll try again tomorrow.

[Heather Macbeth]

Johan Commelin said:

Heather Macbeth Note that, if you want to push to a branch of the community repo, you need to tell us your github username. (Until that point, you can always create a fork of mathlib, make your change there, and make a pull request from your fork to the main repo.)

I created a github account, username hrmacbeth.

[Johan Commelin]

You've got an invitation

[Heather Macbeth]

Great, I'm in!

[Patrick Massot]

Sorry, maybe I should put version information in the README, like (new in version 0.0.6)