Skip to content

Instantly share code, notes, and snippets.

@zorun
Last active April 18, 2018 13:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save zorun/c2c2cc2c7d47bab780915ed425eb164c to your computer and use it in GitHub Desktop.
Save zorun/c2c2cc2c7d47bab780915ed425eb164c to your computer and use it in GitHub Desktop.
Coq 8.8.0 doc build error
(cd doc/tutorial; hevea -fix -exec xxdate.exe Tutorial.v)
(cd doc/tutorial;\
latex -interaction=batchmode Tutorial.v;\
../tools/show_latex_messages Tutorial.v.log)
(cd doc/tutorial;\
pdflatex -interaction=batchmode Tutorial.v.tex;\
../tools/show_latex_messages Tutorial.v.log)
../common/macros.tex:215: Warning: Defining '\proof' by \renewcommand
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/Arch Linux) (preloaded format=pdflatex)
restricted \write18 enabled.
./Tutorial.v.tex:15: Warning: Command not found: \vfill
./Tutorial.v.tex:15: Warning: \hbox
./Tutorial.v.tex:15: Warning: Command not found: \vfill
This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017/Arch Linux) (preloaded format=latex)
restricted \write18 enabled.
entering extended mode
entering extended mode
HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right.
Run, run, again...
../common/macros.tex:215: Warning: Defining '\proof' by \renewcommand
./Tutorial.v.tex:15: Warning: Command not found: \vfill
./Tutorial.v.tex:15: Warning: \hbox
./Tutorial.v.tex:15: Warning: Command not found: \vfill
Fixpoint reached in 2 step(s)
Overfull \hbox (0.79283pt too wide) in paragraph at lines 1091--1096 (file Tutorial.v.tex)
Overfull \hbox (1.41699pt too wide) in paragraph at lines 1532--1537 (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
Overfull \hbox (2.69931pt too wide) in paragraph at lines 2278--2283 (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
Overfull \hbox (0.79283pt too wide) in paragraph at lines 1091--1096 (file Tutorial.v.tex)
Overfull \hbox (1.41699pt too wide) in paragraph at lines 1532--1537 (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
Overfull \hbox (2.69931pt too wide) in paragraph at lines 2278--2283 (file Tutorial.v.tex)
Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex)
! Extra }, or forgotten \endgroup. (file Tutorial.v.aux)
l.56 re on your own}
{47}{section.3.4}}
I've deleted a group-closing symbol because it seems to be
spurious, as in `$x}$'. But perhaps the } is legitimate and
you forgot something else, as in `\hbox{$x}'. In such cases
the way to recover is to insert both the forgotten and the
deleted material, e.g., by typing `I$}'.
! Extra }, or forgotten \endgroup. (file Tutorial.v.aux)
l.56 re on your own}{47}{section.3.4}}
I've deleted a group-closing symbol because it seems to be
spurious, as in `$x}$'. But perhaps the } is legitimate and
you forgot something else, as in `\hbox{$x}'. In such cases
the way to recover is to insert both the forgotten and the
deleted material, e.g., by typing `I$}'.
)
Package atveryend Info: Empty hook `AtVeryEndDocument' on input line 2734.
Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 2734.
Package rerunfilecheck Warning: File `Tutorial.v.out' has changed.
(rerunfilecheck) Rerun to get outlines right
(rerunfilecheck) or use package `bookmark'.
Package rerunfilecheck Info: Checksums for `Tutorial.v.out':
(rerunfilecheck) Before: D41D8CD98F00B204E9800998ECF8427E;0
(rerunfilecheck) After: 0864374CC31E16E22A6F1EC20F81BB34;2205.
Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 2734.
)
Here is how much of TeX's memory you used:
5986 strings out of 492983
82260 string characters out of 6138605
166208 words of memory out of 5000000
9502 multiletter control sequences out of 15000+600000
60601 words of font info for 83 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
29i,8n,28p,327b,424s stack positions out of 5000i,500n,10000p,200000b,80000s
Output written on Tutorial.v.dvi (47 pages, 120104 bytes).
make[1]: *** [Makefile.doc:148: doc/tutorial/Tutorial.v.dvi] Error 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment