Going Public Step 5

[awodey]

Put the book on the arXiv.

[andrejbauer]

This could be hard.

[mikeshulman]

I'm confident it should be possible to create a version that will compile on the arXiv, although we might end up having to create hott-arxiv.tex.

[andrejbauer]

We are most certainly going to create hott-arxiv.tex. I'll try to do this soon.

[mikeshulman]

@andrejbauer, are you still working on this? If not, I can give it a try.

[spitters]

Meanwhile, Google books has accepted our book and is currently processing it (I am not entirely sure what that means).

On Wed, Jun 26, 2013 at 7:57 AM, Mike Shulman notifications@github.comwrote:

Andrej, are you still working on this? If not, I can give it a try.

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

[andrejbauer]

I am not working on much of anything because my laptop was stolen and I am waiting for a new one.

[spitters]

Ouch!

On Wed, Jun 26, 2013 at 4:29 PM, Andrej Bauer notifications@github.comwrote:

I am not working on much of anything because my laptop was stolen and I am waiting for a new one.

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

[mdnahas]

My condolences. It sucks hard.

Hope you have a good backup. (And I'll go backup mine tonight...)

On Wed, Jun 26, 2013 at 4:30 PM, Andrej Bauer notifications@github.comwrote:

I am not working on much of anything because my laptop was stolen and I am waiting for a new one.

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

[RobertHarper]

oh, here in new orleans? how?

Sent from tablet

On Jun 26, 2013, at 9:30, Andrej Bauer notifications@github.com wrote:

I am not working on much of anything because my laptop was stolen and I am waiting for a new one.

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

[mikeshulman]

If we do manage to put the book on the arXiv, who are we going to list as the authors? Will the arXiv let us put just "The Univalent Foundations Project"?

[awodey]

On Jul 5, 2013, at 6:21 AM, Mike Shulman notifications@github.com wrote:

If we do manage to put the book on the arXiv, who are we going to list as the authors? Will the arXiv let us put just "The Univalent Foundations Project"?

that would be best. otherwise we'll have to make up a person : - )

[andrejbauer]

When youmsubmit a paper on arXiv they ask you whether you are doing it on someone else's behalf. That might be the way to go. But even better, rather than guessing we could try to talk to a live human within arXiv. Surely such creatures exist.

[mikeshulman]

I thought I would make a try at putting the book on arXiv. I started by just uploading hott-online.tex and all the .tex files it includes, as well as the bbl and ind files and mathpartir.sty (which isn't a standard package).

The first problem I ran into is that arXiv was unable to guess that hott-online was a LaTeX file, trying instead to pass it through plain TeX (or to run LaTeX on main.tex directly). I wasn't sure how to fix that, but just for the moment to see what other problems there might be, I tried pasting the important content of hott-online.tex at the top of main.tex (and renaming the bbl and ind files appropriately).

The second problem I encountered was "Undefined control sequence: \nopagecolor". Apparently this was due to the arXiv not realizing that it needs to use PDFLaTeX, and was fixed by adding \pdfoutput=1 at the top of main.tex.

The third problem was the dreaded "Option clash for package hyperref". This happens even when I comment out all the options we passed to hyperref. Any ideas anyone?

[andrejbauer]

Create a main-arxiv which bypasses main.tex and just live with it.

[mikeshulman]

Yeah, that'll solve the first problem, but what about the third?

[JasonGross]

Is the full log available somewhere? Do two of your packages try to require hyperref with clashing options? What options does it say were loaded the first time?

[JasonGross]

My first hypothesis, on no data: perhaps some package tries to load hyperref with some options if it thinks you're in dvi or ps mode, and other options if it thinks your in pdf mode, and the arxiv setup doesn't let that package know you're in pdf mode (maybe it needs to be passed [pdftex] as an option explicitly)?

[JasonGross]

Another possibility is that LaTeX might be finicky about the order in which packages are loaded.

[mikeshulman]

The error happens at the "\begin{document}" line.

[mikeshulman]

The first loading of hyperref says

Package hyperref Message: Driver (autodetected): hpdftex.

Then the error is

! LaTeX Error: Option clash for package hyperref.

See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
... 

l.157 \begin
{document}
? 
! Emergency stop.
... 

l.157 \begin
{document}
! ==> Fatal error occurred, no output PDF file produced!
Transcript written on main.log.

[JasonGross]

So some package is trying to set a package option at \begin{document}...? What does the log look like if, right before \begin{document}, you insert \show\document\relax \expandafter\show\csname @begindocumenthook\endscname, and try to get arxiv to compile it again?

[JasonGross]

Oh, also insert \show\nopagecolor, because that's the last command before \begin{document}, and I can't tell if the error is happening in \begin{document}, or right before it.

[mikeshulman]

It seems that each occurrence of \show stops the compilation permanently, so in order to get all of these shown I had to do three different runs.

Here's \show\document:

> \document=macro:
->\endgroup \let \AtEndPreamble \@firstofone \@endpreamblehook \protected \def 
\AtEndPreamble {\@notprerr \@gobble }\undef \@endpreamblehook \begingroup \endg
roup \ifx \@unusedoptionlist \@empty \else \@latex@warning@no@line {Unused glob
al option(s):
\@spaces [\@unusedoptionlist ]}\fi \@colht \textheight \@colroom \textheight \v
size \textheight \columnwidth \textwidth \@clubpenalty \clubpenalty \if@twocolu
mn \advance \columnwidth -\columnsep \divide \columnwidth \tw@ \hsize \columnwi
dth \@firstcolumntrue \fi \hsize \columnwidth \linewidth \hsize \begingroup \@f
loatplacement \@dblfloatplacement \makeatletter \let \@writefile \@gobbletwo \g
lobal \let \@multiplelabels \relax \@input {\jobname .aux}\endgroup \if@filesw 
\immediate \openout \@mainaux \jobname .aux \immediate \write \@mainaux {\relax
}\@beginmainauxhook \fi \process@table \let \glb@currsize \@empty \normalsize 
\everypar {}\ifx \normalsfcodes \@empty \ifnum \sfcode `\.=\@m \let \normalsfco
des \frenchspacing \else \let \normalsfcodes \nonfrenchspacing \fi \fi \@noskip
secfalse \let \@refundefined \relax \let \AtBeginDocument \@firstofone \@begind
ocumenthook \ifdim \topskip <1sp\global \topskip 1sp\relax \fi \global \@maxdep
th \maxdepth \global \let \@begindocumenthook \@undefined \ifx \@listfiles \@un
defined \global \let \@filelist \relax \global \let \@addtofilelist \@gobble \f
i \gdef \do ##1{\global \let ##1\@notprerr }\@preamblecmds \global \let \@nodoc
ument \relax \global \let \do \noexpand \ignorespaces \let \AfterEndPreamble \@
firstofone \@afterendpreamblehook \protected \def \AfterEndPreamble {\@notprerr
\@gobble }\undef \@afterendpreamblehook \ignorespaces .

I'm not going to copy everything in \expandafter\show\csname @begindocumenthook\endcsname (if you really want to see it, you can make it yourself, see next comment), but here's the only part that makes any explicit mention of hyperref:

{\@ifpackage
loaded {hyperref}{}{\def \hyper@natlinkstart ##1{\Hy@backout {##1}}}\PackageInf
o {backref}{** backref set up for natbib **}}

Here's \show\nopagecolor:

> \nopagecolor=macro:
->\no@page@color .

[mikeshulman]

I have made an "arxiv" branch in my fork here, in which you can type

make hott-arxiv.tar.gz

and it will make a tar file suitable for uploading to the arXiv, containing an autogenerated master file hott-arxiv.tex that deals with the first and second problems I encountered. You can then tweak it however you like to try to fix the hyperref issue.

[JasonGross]

It looks like you forgot to include frontpage.tex in the tar. I'm not sure what the difference between hpdflatex and pdflatex is, but it looks like arxiv is first trying hpdflatex, failing on option clash, then trying pdflatex instead, and getting further, but failing on including frontpage.tex.

As an aside, the sequence \message{\expandafter\unexpanded\expandafter{\foo}} is roughly equivalent to a non-fatal version of \show\foo.

[JasonGross]

You also seem to be missing some .png files, such as cover-lores-front.png.

[mikeshulman]

Ah, I assumed that BOOKTEXFILES in the Makefile was up to date, but I guess it was missing frontpage.tex. Let me try adding all of those...

[mikeshulman]

Aaand... it works!! (symbols.tex and blurb.tex were also missing.)

!!

[mikeshulman]

Thanks for your help, Jason. Are there any other changes to hott-online that we want to make for the arXiv version? I'm going to try to do something about #413 and #415 soon, and it would probably be nice to deal with #417 and #289 too.

Actually, should the arXiv version be made from hott-online or from hott-letter?

[mikeshulman]

By the way, regarding authorship here is what the arXiv has to say:

If the authors constitute a named collaboration, the collaboration name should be used in addition to listing all authors. Please contact arXiv administrators when our automated system objects to author lists that are too long, we can override this manually.

I feel like technically, "The Univalent Foundations Program" does constitute a "named collaboration" in the sense they mean, but I'm not really enthusiastic about listing all of us (meaning, presumably, everyone listed in the Preface) in the author field. I hope they won't mind if we just put "The Univalent Foundations Program".

[awodey]

right, let's try to get away with just "The Univalent Foundations Program". If they object and say they also need names of individuals, we'll have Andrej lecture them about 21st-century scientific best practices.

On Jul 27, 2013, at 12:54 AM, Mike Shulman notifications@github.com wrote:

By the way, regarding authorship here is what the arXiv has to say:

If the authors constitute a named collaboration, the collaboration name should be used in addition to listing all authors. Please contact arXiv administrators when our automated system objects to author lists that are too long, we can override this manually.

I feel like technically, "The Univalent Foundations Program" does constitute a "named collaboration" in the sense they mean, but I'm not really enthusiastic about listing all of us (meaning, presumably, everyone listed in the Preface) in the author field. I hope they won't mind if we just put "The Univalent Foundations Program".

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

[awodey]

I would think hott-online.
it seems likely that anyone who gets it from the archive will eventually find their way to the website and see that hott-letter is also there for printing. Hmm, on second thought, maybe hott-letter is actually the more universal version, and the above argument applies to finding hott-online.

On Jul 27, 2013, at 12:50 AM, Mike Shulman notifications@github.com wrote:

Thanks for your help, Jason. Are there any other changes to hott-online that we want to make for the arXiv version? I'm going to try to do something about #413 and #415 soon, and it would probably be nice to deal with #417 and #289 too.

Actually, should the arXiv version be made from hott-online or from hott-letter?

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

[mikeshulman]

I was thinking of putting in the notes field something like "arXiv v1: version first-edition-246-g5ee926b. Other versions available at http://homotopytypetheory.org/book." We could be more specific about what other versions are available there.

Anyone else have an opinion about hott-online vs hott-letter?

[zhenlin]

Regarding hpdftex and hyperref clashes: you can add nohypertex to the beginning of 00README.XXX to avoid this problem... but arXiv should automatically try pdflatex when that fails.

[mikeshulman]

@zhenlin : it did. I was just being a moron and not scrolling down far enough.

[mikeshulman]

It doesn't matter a whole lot, but I think I think that hott-online is the most "canonical" version. It's the one that I always compile as i'm working on things. And it's not a disaster if someone prints it out, either: the only differences to hott-letter are the bastard title page, some optimizations for b&w, and higher resolution images. Actually, the latter seems like a concrete reason to go with hott-online for the arXiv: the compiled file size is much smaller (4.3M vs 6.7M).

We also need an abstract, which is supposed to be no longer than "about 20 lines". Here's an abridged version of the back cover blurb that I think is about the right length:

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

Suggestions are welcome. If this looks okay, then as soon as someone merges #434, #439, and #440, I can post it to the arXiv.

[spitters]

Looks OK to me. Thanks for this. I will prompt Google books again next week. On Aug 1, 2013 3:54 PM, "Mike Shulman" notifications@github.com wrote:

It doesn't matter a whole lot, but I think I think that hott-online is the most "canonical" version. It's the one that I always compile as i'm working on things. And it's not a disaster if someone prints it out, either: the only differences to hott-letter are the bastard title page, some optimizations for b&w, and higher resolution images. Actually, the latter seems like a concrete reason to go with hott-online for the arXiv: the compiled file size is much smaller.

We also need an abstract, which is supposed to be no longer than "about 20 lines". Here's an abridged version of the back cover blurb that I think is about the right length:

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the ba sics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

Suggestions are welcome. If this looks okay, then as soon as someone merges #434 https://github.com/HoTT/book/issues/434, #439https://github.com/HoTT/book/issues/439, and #440 https://github.com/HoTT/book/issues/440, I can post it to the arXiv.

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

[awodey]

this looks good to me. thanks for doing this MIke -- especially right now, when you probably also have other things on your mind : - )

Steve

On Aug 1, 2013, at 3:51 PM, Mike Shulman notifications@github.com wrote:

It doesn't matter a whole lot, but I think I think that hott-online is the most "canonical" version. It's the one that I always compile as i'm working on things. And it's not a disaster if someone prints it out, either: the only differences to hott-letter are the bastard title page, some optimizations for b&w, and higher resolution images. Actually, the latter seems like a concrete reason to go with hott-online for the arXiv: the compiled file size is much smaller.

We also need an abstract, which is supposed to be no longer than "about 20 lines". Here's an abridged version of the back cover blurb that I think is about the right length:

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the ba sics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

Suggestions are welcome. If this looks okay, then as soon as someone merges #434, #439, and #440, I can post it to the arXiv.

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

[mikeshulman]

One last question: what subject category(ies)? Logic? Algebraic topology? Category theory?

[awodey]

On Aug 3, 2013, at 6:30 AM, Mike Shulman notifications@github.com wrote:

One last question: what subject category(ies)? Logic? Algebraic topology? Category theory?

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

[mikeshulman]

How about cs.PL? I think Dan Licata told me that a lot of type theory ends up in there. But I'm slightly worried about too much cross-listing.

[RobertHarper]

i would suggest so.

(sent from handheld)

On Aug 3, 2013, at 19:01, Mike Shulman notifications@github.com wrote:

How about cs.PL? I think Dan Licata told me that a lot of type theory ends up in there. But I'm slightly worried about too much cross-listing.

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

[mikeshulman]

Ok, submitted, but changes can still be made until Monday.

[mikeshulman]

Hmm, I guess I could also have used the Lulu "description" as the arXiv abstract. Oh well.

[spitters]

We have used CS.LO (logic) for this before, I guess either would do.

On Sat, Aug 3, 2013 at 7:01 PM, Mike Shulman notifications@github.comwrote:

How about cs.PL? I think Dan Licata told me that a lot of type theory ends up in there. But I'm slightly worried about too much cross-listing.

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

[mikeshulman]

http://arxiv.org/abs/1308.0729