HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Make an index #94

Closed cangiuli closed 11 years ago

DanGrayson commented 11 years ago

On Thu, May 30, 2013 at 5:53 PM, Mike Shulman notifications@github.comwrote:

The best one I've been able to think of so far is to have entries for denial, anger, bargaining, depression, and acceptance pointing to appropriate sections.

That sounds good!

We could also try putting in unintentional type theory, although I'm not sure what to make it refer to.

It could refer to the page in the bibliography where we (will) have a reference to Carlo's paper (with his (unintentional) permission).

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

mikeshulman commented 11 years ago

It would be more fun if it pointed to something in the text.

I might have some time to work on the index tonight, so I'll check out I, J, and K.

cangiuli commented 11 years ago

Of course; put it wherever you'd like. I agree with Mike that it should probably point to the text, though...

andrejbauer commented 11 years ago

If there is place in the book where we say that there are many variants of type theory, that's where we could refer to Carlo's paper.

mikeshulman commented 11 years ago

In the notes to chapter 1 or 2?

mikeshulman commented 11 years ago

I J K done.

mikeshulman commented 11 years ago

On second thought, I'm a little worried about putting a joke in the main text. It's not uncommon to put jokes in the index, but maybe since the book is potentially controversial, everything in the main text should be serious? Maybe it's good enough to point to the bibliography.

awodey commented 11 years ago

I agree. Lets keep the text clean.

Sent from my iPhone

On May 31, 2013, at 1:21 PM, Mike Shulman notifications@github.com wrote:

On second thought, I'm a little worried about putting a joke in the main text. It's not uncommon to put jokes in the index, but maybe since the book is potentially controversial, everything in the main text should be serious? Maybe it's good enough to point to the bibliography.

— Reply to this email directly or view it on GitHub.

DanGrayson commented 11 years ago

I'll do M.

mikeshulman commented 11 years ago

Now working on O.

DanGrayson commented 11 years ago

How about adding a reference that points to Andrej's video lecture on the five stages?

DanGrayson commented 11 years ago

I see definitions of both "metric compact" and "metrically compact" in reals.tex. Andrej?

spitters commented 11 years ago

That's a nice idea. Andrej has a write-up which would be better to refer to. Unfortunately, I cannot find the url.

On Sat, Jun 1, 2013 at 2:06 PM, Daniel R. Grayson notifications@github.comwrote:

How about adding a reference that points to Andrej's video lecture on the five stages?

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

mikeshulman commented 11 years ago

Now indexing P

mikeshulman commented 11 years ago

BTW, metric compact and metrically compact are the same.

DanGrayson commented 11 years ago

good catch; 42da9bf911f6c758c0966f5a461b23dea1569be7

On Sun, Jun 2, 2013 at 9:46 PM, Mike Shulman notifications@github.comwrote:

BTW, metric compact and metrically compact are the same.

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

DanGrayson commented 11 years ago

indexed some uniqueness principles in 762a7fdb1b6ad5f44acd11526521d4fb943e26ea

mikeshulman commented 11 years ago

Now indexing R

mikeshulman commented 11 years ago

Now indexing S

mikeshulman commented 11 years ago

Now indexing C

andrejbauer commented 11 years ago

How are we doing, are we close to finishing?

mikeshulman commented 11 years ago

I think only D E F remain to index.

mikeshulman commented 11 years ago

Now indexing D.

andrejbauer commented 11 years ago

Now indexing E.

andrejbauer commented 11 years ago

I consider the debuggin milestone completed! (I also predict it will take 10 minutes for someone to repoen this issue.)

mikeshulman commented 11 years ago

Sorry I'm a bit slow. (-: There are a few places where the index looks a bit ugly because of the very small space between the two columns. E.g. on the second page at the moment we have the "limited prin-bracket type". Can we do something about that?

awodey commented 11 years ago

I will make one more pass through the entire book looking for "stray" entries for the index.

Sent from my iPhone

On Jun 11, 2013, at 11:33 AM, Mike Shulman notifications@github.com wrote:

Sorry I'm a bit slow. (-: There are a few of places where the index looks a bit ugly because of the very small space between the two columns. E.g. on the second page at the moment we have the "limited prin-bracket type". Can we do something about that?

— Reply to this email directly or view it on GitHub.

awodey commented 11 years ago

the index needs to have a bit more space between the 2 columns.

awodey commented 11 years ago

which names should be indexed? Russell? Lawvere? Martin-L"of? Voevodsky? Bauer? How and where do we draw the line?

mikeshulman commented 11 years ago

I haven't been indexing any names. On Jun 11, 2013 4:26 PM, "Steve Awodey" notifications@github.com wrote:

which names should be indexed? Russell? Lawvere? Martin-L"of? Voevodsky? Bauer? How and where do we draw the line?

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

awodey commented 11 years ago

I'm done.

awodey commented 11 years ago

remaining index issues:

andrejbauer commented 11 years ago

Feel free to fiddle with the column separation. I wasn't trying to get it right, I just created a configuration option that let's you do it.

I'm not sure we want names in the index. Those really can just be searched in the online version.

andrejbauer commented 11 years ago

I would like to suggest a bit of caution when you index entries. At this late stage, you have to be quite careful how you index. It is almost impossible to index correctly without first checking what has already been indexed. Some hints:

  1. Before you index anything, look at the index and think how it is going to fit with existing entries.
  2. When indexing "X Y", should you use \index{X Y}, or \index{X!Y}, or index{Y!X}? The answer depends on what is already there. For example, if there is already \index{connected type} and you want to index "connected function" you must first change connected type to \index{connected!type} and then index \index{connected!function}.
  3. Do not overdo it. For instance, it feels to me that "set" has too many entries.
  4. Use ranges where applicable. For example, instead of indexing five times "fundamental!group!of circle" all over the section on the fundamental group of circle, use a range: start it with \index{fundamental!group!of circle|(} and end it with \findex{fundamental!group!of circle|}.
  5. Do not index both \indexsee{X}{Y} and \index{X}.
  6. Index a term right next to where it appears and not for example at the end of the paragraph, or after the theorem statement. A page break could be inserted in between the term and the index command.
awodey commented 11 years ago

is the index done?

andrejbauer commented 11 years ago

As far as I know, and unless you make another pass ;-)

awodey commented 11 years ago

in that case, I'm closing this. good work everyone! this good index will be a big help to users.

mikeshulman commented 11 years ago

I'm not going to bother reopening, but I'm still fixing a bunch of stuff. Always look for previous index entries when adding new ones. If there are already a bunch of \index{monoid!free}s, then rather than adding a single \index{free!monoid} it's better to add an \indexsee{free!monoid}{monoid, free}.

mikeshulman commented 11 years ago

Ok, now I think I'm done.

andrejbauer commented 11 years ago

I keep finding missing spaces because we put % signs at the end of \index commands (mea culpa). I just removed them all in 0fb74542832776036b37713cb6621b2b90e4eedb. This is a very big commit with gazillion small changes. It is likely going to create merge conflicts, so make sure to pull it before you make further changes.

mikeshulman commented 11 years ago

Aren't we going to start finding spurious paragraph breaks now?

On Wed, Jun 12, 2013 at 2:12 PM, Andrej Bauer notifications@github.comwrote:

I keep finding missing spaces because we put % signs at the end of \indexcommands (mea culpa). I just removed them all in 0fb7454https://github.com/HoTT/book/commit/0fb74542832776036b37713cb6621b2b90e4eedb. This is a very big commit with gazillion small changes. It is likely going to create merge conflicts, so make sure to pull it before you make further changes.

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

andrejbauer commented 11 years ago

I don't think so. This would happen only if we introduced an empty line, but we did not. I replaced all occurrences of }%\n with }\n where \n means "new line". I don't think this can produce an empty line where there wasn't one before, can it?

mikeshulman commented 11 years ago

Okay, maybe not paragraph breaks, but we do have extra spaces. Look for example at the fifth line of chapter 2, where we have "topology, and a path" with extra space after the comma.

andrejbauer commented 11 years ago

Hmm, this is annoying. Well then, let's just revert the commit.

mikeshulman commented 11 years ago

I think the real problem is not being consistent about where the %s go. In principle, it should go on the line before the \index command, since otherwise there might be a page break in between. But it seems to be easier to put them on the line with the \index command. It's when we do both that spaces disappear. I don't know what the best solution is at this point.

andrejbauer commented 11 years ago

The best solution is regexp magic. At least let me try to find all bad occurrences. What would those be? A % sign at the end of a line, followed by an index entry with another % sign, then text?

DanGrayson commented 11 years ago

When doing the L's I indexed "Lawvere", not knowing whether I should.

On Wed, Jun 12, 2013 at 6:36 AM, Steve Awodey notifications@github.comwrote:

remaining index issues:

  • spacing between two columns needs to be increased?
  • need to decide whether to include some names, e.g.: Russell, Frege. Peano, G"odel, Martin'L"of ? if so, someone should insert \index commands systematically, if not, someone should remove the few that are already there.

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