Switch set.mm default branch to "develop" for now?

[David A. Wheeler]

In almost all cases people normally want to refer to the "develop" branch in set.mm, not the "master" branch.

I propose that we switch the set.mm default branch to "develop", to reduce errors and steps.

In the longer term we can discuss other changes, but this is an *easy* change.

Sound okay?

--- David A. Wheeler

[Alexander van der Vekens]

OK for me!

Alexander

[Norman Megill]

This is fine with me, please go ahead.  I vaguely recall discussing that a while back and thought it was already done. :)

Norm

[Jim Kingdon]

Sounds good to me

[David A. Wheeler]

On September 6, 2018 4:32:46 PM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>This is fine with me, please go ahead. I vaguely recall discussing
>that a
>while back and thought it was already done. :)

The default branch for set.mm is now develop on GitHub.


--- David A.Wheeler

[Benoit]

Does this change anyting to the documentation in https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing ?

I just followed the instructions on that page, and at step 5b, after typing

$ git checkout develop

I am told: "Already on "develop". At step 5c, after typing

$ git pull upstream

I am told:

From https://github.com/metamath/set.mm
 * [new branch] Achaemenid-develop    -> upstream/Achaemenid-develop
 ...
 * [new branch] usage-discouraged-3   -> upstream/usage-discouraged-3

You have required to pull from the distant repository 'upstream', but without indicating the branch. Since this is not the default distant repository in the configuration for the current branch, you have to specify the branch with the command.

What should I do ?

Also: is this connected to the "--no-single-branch" option used at step 4b? What does this option do?


Thanks in advance,

Benoit

[Antony Bartlett]

Can I just check what the definitive url is for getting an up to date release copy of set.mm is, please?  I think it's:

https://raw.githubusercontent.com/metamath/set.mm/master/set.mm

    Best regards,

        Antony

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

It depends on what you mean by "definitive".  The master is a snapshot of develop taken periodically but not that often.  For any kind of development you want to stay in sync with develop,

https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm

Norm

On Monday, September 10, 2018 at 8:37:39 AM UTC-4, Antony Bartlett wrote:

Can I just check what the definitive url is for getting an up to date release copy of set.mm is, please?  I think it's:

https://raw.githubusercontent.com/metamath/set.mm/master/set.mm

    Best regards,

        Antony

[David A. Wheeler]

> On Monday, September 10, 2018 at 8:37:39 AM UTC-4, Antony Bartlett wrote:
> >
> > Can I just check what the definitive url is for getting an up to date
> > release copy of set.mm is, please? I think it's:
> >
> > https://raw.githubusercontent.com/metamath/set.mm/master/set.mm

As Norm noted, the "master" branch is not updated often.

The latest-and-greatest version can be acquired here from the "develop" branch:

https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm

However, there's no tracking. If you plan to do this over time, the instructions here:
https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing

will set up an environment with git so that you can pull down the latest version
and have many different tracked versions without losing anything.

--- David A. Wheeler

[David A. Wheeler]

On Sun, 9 Sep 2018 12:00:01 -0700 (PDT), Benoit <benoit...@gmail.com> wrote:
> Does this change anyting to the documentation in
> https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing ?
>
> I just followed the instructions on that page, and at step 5b, after typing
> $ git checkout develop
> I am told: "Already on "develop".

Which is correct - now that the default is 'develop', that's what you'll get.

> At step 5c, after typing
> $ git pull upstream
> I am told:
> From https://github.com/metamath/set.mm
> * [new branch] Achaemenid-develop -> upstream/Achaemenid-develop
> ...
> * [new branch] usage-discouraged-3 -> upstream/usage-discouraged-3
> You have required to pull from the distant repository 'upstream', but
> without indicating the branch. Since this is not the default distant
> repository in the configuration for the current branch, you have to specify
> the branch with the command.

You should be able to fix that by running (if you're already in your "develop" branch):

git branch --set-upstream-to upstream/develop

This means that from now on any "git push" on your current branch (develop) will be pushed to "upstream/develop" (your copy on GitHub). Then this command should work normally:

git pull upstream

Let me know if that seems to solve things, if it does we should add it to the instructions.

> Also: is this connected to the "--no-single-branch" option used at step 4b?
> What does this option do?

Not really. I've updated the instructions to explain what --no-single-branch does.
By default, git maintains the *entire* history of the project, but most people
only need relatively recent history, so our instructions try to be kind to your
download time and storage space.

--- David A. Wheeler

[Benoit]

David, thanks for your answer and for the "contributing" page. It is very useful.

Typing "git branch --set-upstream-to upstream/develop", as you advised, worked. This command has to be typed only once, if I understand correctly, so maybe it should be added as step 4f (and similarly, now "git checkout develop" has to be typed only once?).

Then, on step 7, after typing "git push --set-upstream origin", git complains that <YOUR_BRANCH_NAME> has no upstream branch, so I typed as indicated "git push --set-upstream origin <YOUR_BRANCH_NAME>". So apparently, for each branch created locally, one has to create the corresponding branch on github ?

Maybe the following type of diagram could be added to the page, to help understanding (and maybe my diagram should be corrected and completed):

(numbers indicate the steps)

distant metamath/set.mm develop    ---------------------------------------------------------

                                       \(3)                                       /(8)

distant username/set.mm (your fork)     ----------------------------------------------------

                                           \(4)   \(5c)                    /(7) (*)

local   develop                             ------------------------------------------------

                                                       \(5d)         /(5g)

local   <YOUR_BRANCH_NAME>                              -----(5e)----

(*): actually, you push to a branch which you then merge with your fork.

origin = distant metamath/set.mm

upstream = distant username/set.mm

Benoit

[Antony Bartlett]

Thanks.  Actually I think it depends on what I mean by "release".  When you release a new version of the MetaMath program it ships with a copy of set.mm, where does that come from - develop or master?  I'm writing some very modest tooling (like the proof-tree stuff I posted about at the end of May), and possibly a verifier, and can have the latest set.mm automatically downloaded at installation time (with an an option to update it later).  I think in these circumstances it would be better to provide the more stable master url in the default configuration.

If on the other hand I was involved with the development of any proofs, then I'm sure the develop branch would be most appropriate.

    Best regards,

        Antony

[Norman Megill]

On Tuesday, September 11, 2018 at 6:16:10 PM UTC-4, Antony Bartlett wrote:

Thanks.  Actually I think it depends on what I mean by "release".  When you release a new version of the MetaMath program it ships with a copy of set.mm, where does that come from - develop or master?

It comes from develop.  Actually, the metamath program download is updated every time the site is rebuilt, which is usually within a day after a set.mm develop commit. The commit number is mentioned at the top of the "Most Recent Proofs" page
http://us2.metamath.org:88/mpeuni/mmrecent.html .
 

  I'm writing some very modest tooling (like the proof-tree stuff I posted about at the end of May), and possibly a verifier, and can have the latest set.mm automatically downloaded at installation time (with an an option to update it later).  I think in these circumstances it would be better to provide the more stable master url in the default configuration.

Metamath databases are in a kind of unusual category compared to most software, because bugs are for practical purposes impossible.  A release to develop is rigorously tested with 3 independently-written proof verifiers along with a number of other checks to ensure various non-mathematical conventions.  Nothing goes to develop unless it passes all of these.  In particular, all proofs must be complete; a half-completed proof must stay behind in the user's local repository (typically, a user will comment these out or delete them before updating develop with their ongoing work).

Because of this, there really isn't such a thing as a "stable" release of set.mm in the sense of software that has undergone alpha, beta, and pre-release testing.  Every release of develop is automatically "stable".  What we call "master" is thus somewhat vague and in essence up to my whim as maintainer.  In the past I typically have made master snapshots prior to significant database changes, such as a change of theorem naming conventions that might affect hundreds of proofs.  The next master release I have planned will be the last develop commit before the update to the new df-riota definition I announced last week and am working on now (outside of the develop branch until it is complete).
 
The only reason I can think of to use the master instead of develop is if you have software that may not have all of the bugs worked out, and the master can provide a relatively fixed data source that you have tested the software with.

Norm

PS - Google classified your post as spam, and even worse, it took 31 hours after you submitted it before Google notified me (as moderator) that your message was likely spam and needed approval.

If on the other hand I was involved with the development of any proofs, then I'm sure the develop branch would be most appropriate.

    Best regards,

        Antony

[fl]

 

  What we call "master" is thus somewhat vague and in essence up to my whim as maintainer. 

All that sounds like a project that tries at all cost to comply with version control strategies not made for it.

I think that a simple day by day list with no branch would better fit the pecularities of the metamath databases.

 

PS - Google classified your post as spam, and even worse, it took 31 hours after you submitted it before Google notified me (as moderator) that your message was likely spam and needed approval.

I proudly must admit that Google never classifies my post as spam. But they absolutely want to know

my phone number.  What I don't want. The essence of Capitalim is harassment.

--

FL

[Antony Bartlett]

All that sounds like a project that tries at all cost to comply with version control strategies not made for it.

 

Norm's saying we have a robust continuous delivery pipeline.  In these circumstances it's fine to commit directly to master (or anywhere).

https://hackernoon.com/i-have-a-confession-to-make-i-commit-to-master-6a804f334beb

(note this article is only relevant as far as the first sub-heading)

In my view this is both a well-respected version control strategy, and entirely appropriate for Metamath.

Apart from the naming - and there's nothing magic about the name 'master' - what I'm describing here is already current practice.  However, I do think the actual name of the branch being called 'develop' has connotations of something less solid and doesn't properly convey the verified-correctness and stability of its contents.  Certainly it is what's suggested to me by the name 'develop' that prompted me to ask for clarification about the correct url. That naming was probably one of the things David had in mind to look at in the longer term when he kicked off this thread with:

In the longer term we can discuss other changes, but this is an *easy* change.

    Best regards,

        Antony

[David A. Wheeler]

On Wed, 12 Sep 2018 15:05:30 +0100, Antony Bartlett <a...@akb.me.uk> wrote:
> Norm's saying we have a robust continuous delivery pipeline. In these

> circumstances it's fine to commit directly to master (or anywhere)....

> That naming was probably one of the things David had in mind
> to look at in the longer term when he kicked off this thread with:
>
> > In the longer term we can discuss other changes, but this is an *easy*
> > change.

That's right. In most projects I work with "master" is the branch that is constantly getting the latest updates, and we might want to switch to that.

However, that will require people changing their workflows. Since "develop" is the branch people usually want to use, I thought it'd be simplest to start making the default the "normal case", since that doesn't change the meaning of any branch.

--- David A. Wheeler