HoTT / book

A textbook on informal homotopy type theory
2.03k stars 359 forks source link

How to add new material #614

Open mikeshulman opened 10 years ago

mikeshulman commented 10 years ago

Supposing we want to add new mathematics, let's discuss how to do it in a new thread. Some possibilities:

I feel like if and when we are seriously ready to work on the second edition, we'll need to go for the first option eventually anyway: merging in the new additions will probably require work over a period of time. But I do see the advantage of the second choice at first, in that it gives current readers an easy way to see what's being added.

andrejbauer commented 10 years ago

Without a doubt we should follow the open source community here. Which means that we would branch, what Vladimir proposes would make sense if we did not have Github.

But the old version should be branched off into 1st-edition, while the development of the second edition should take place on master. As far as I understand the open-source community, master is supposed to be where the bulk of current development takes place. Branches are there for keeping old versions around, for alternate developments, and for temporary branching (to submit a pull request, or to perform a non-trivial amount of changes).

And until somebody actually starts working on the 2nd edition there is no reason to branch.

mikeshulman commented 10 years ago

I am curious why it makes a difference which branch is called "master". Internally in git, there is no difference between a branch called "master" and a branch called "2nd-edition" other than their names, is there?

EgbertRijke commented 10 years ago

Should we also add "writing volume 2" to the list of things to consider?

2014/1/19 Mike Shulman notifications@github.com

I am curious why it makes a difference which branch is called "master". Internally in git, there is no difference between a branch called "master" and a branch called "2nd-edition" other than their names, is there?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/614#issuecomment-32718593 .

andrejbauer commented 10 years ago

There are various settings which default to master unless otherwise specified. I'll try to figure out whether the open source community has good reasons for their scheme (and whether I got it right). Actually, there ought to be some lurkers around here who can chime in.

JasonGross commented 10 years ago

Andrej is correct. On git it's 'master', on hg it's 'default', on svn it's 'trunk'. Ocassionally it's dev, but that's rare. One reason is to make it easier for new people coming to the project; you look for the same branch, regardless of project, to find the current development work. Another reason is that most people are either interested in "the most recent version" or "some particular past version" but not "whatever version was most recent when I cloned the repo". So it makes sense to have a consistent name for the "most recent work" branch, even if it's different from other projects (though I argued it should be the same above). Furthermore, github has a setting for "default branch" meaning "what branch do I get if I clone without specifying a branch?" and "what page do I see by default?" and "when I make a pull request from this repo I just cloned, which branch should it get merged in to?". People looking for the source generally want to see the current development (and if they don't, they probably have enough knowledge to find their way around anyway), and will get confused if you keep changing the "most recent dev branch" name, and will get even more confused if what they see by default isn't the "most recent dev" branch.

mikeshulman commented 10 years ago

Github certainly treats "master" specially, but does git treat it specially in software (not just users' conventions)?

JasonGross commented 10 years ago

As far as I know, git does not treat the name 'master' specially (neither does GitHub), though both use it as the default value in a number of related places when making a new repository. You won't have any technical problems if you change the name, though I expect you'll get a lot more confused people.

mikeshulman commented 10 years ago

On github, when I push changes to a branch in my fork and then click "compare and pull request", by default it compares to the "master" branch of the main repository. Is that just because "master" is set as the "default" branch of that repository, and if it were set to something else it would do the comparison to that branch?

But anyway, the question is about more than naming. My inclination was to have the first-edition branch be the "default" one, and I thought that that would actually be less confusing. Suppose, for instance, that mathematician X is reading the publically available version of the book (which is a recent release of the first edition), notices a typo, and wants to fix it for us. If the default branch is the first edition, then he can just make a fork, look through the source (which is the same as the source for the printed version he has in front of him) for the typo, fix it, and submit a pull request.

But if the default branch is the second edition, then when X makes his fork, the source he's looking at by default will not correspond to the printed version in front of him. Maybe the second edition has been reorganized, and the paragraph containing his typo has been moved into a different chapter. How is he supposed to find and fix it, without having been a part of all the development of the second edition? Of course, he could manually check out the first-edition branch instead and submit his pull request on that, but that requires more git-fu than I would like to ask of potential typo-fixers.

krakrjak commented 10 years ago

On Mon, Jan 20, 2014 at 11:26 AM, Mike Shulman notifications@github.comwrote:

On github, when I push changes to a branch in my fork and then click "compare and pull request", by default it compares to the "master" branch of the main repository. Is that just because "master" is set as the "default" branch of that repository, and if it were set to something else it would do the comparison to that branch?

Yes. Github will perform the comparison against the "default" branch for the project when preparing pull requests. For HoTT this is currently set to master.

Zac Slade krakrjak@gmail.com

JasonGross commented 10 years ago

On github, when I push changes to a branch in my fork and then click "compare and pull request", by default it compares to the "master" branch of the main repository. Is that just because "master" is set as the "default" branch of that repository, and if it were set to something else it would do the comparison to that branch?

I think github either uses the "default" branch, or it uses some more complicated algorithm to try to figure out which branch of the upstream (main) repository you based your branch on. I'm pretty sure it doesn't have any branch names that it treats specially. So, yes, if you set something else to the default branch, it'll probably compare with that branch.

But anyway, the question is about more than naming. My inclination was to have the first-edition branch be the "default" one, and I thought that that would actually be less confusing.

I guess the question is whether you want to cater to people fixing typos in old versions, or to people contributing to new versions. For most projects, the preference is overwhelmingly for new versions. Security fixes and other minor things will get backported to old versions, for some time, and eventually support is dropped (so if you find a bug in some part of Chrome that was removed 2 years ago, no one is going to take a request to fix it seriously; operating systems have a longer support cycle, maybe around 5 years). It may be different for books. It also depends how much you see this as a developing project; will there be more future editions after the second, as new discoveries are made, or will the book progress towards some "final" state, where there won't be much dev work to do.

mikeshulman commented 10 years ago

Perhaps the conclusion should be to put off the decision until we have a clear picture of what exactly the second edition will be (or even if it will exist at all), and who will be writing it.