Skip to content

Commit dc4fc03

Browse files
cpitclaudelZimmi48
cpitclaudel
authored and
Zimmi48
committed
[doc] Create a separate index file for the LaTeX build
See sphinx-doc/sphinx#4977 for context.
1 parent 6146def commit dc4fc03

File tree

8 files changed

+135
-36
lines changed

8 files changed

+135
-36
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ doc/faq/axioms.eps
9999
doc/faq/axioms.eps_t
100100
doc/faq/axioms.pdf_t
101101
doc/faq/axioms.png
102+
doc/sphinx/index.rst
102103
doc/stdlib/Library.out
103104
doc/stdlib/Library.ps
104105
doc/stdlib/Library.coqdoc.tex

‎doc/sphinx/conf.py

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,30 @@
6666
# The encoding of source files.
6767
#source_encoding = 'utf-8-sig'
6868

69+
from shutil import copyfile
70+
71+
SUPPORTED_FORMATS = { fmt: os.path.abspath("index-{}.rst".format(fmt))
72+
for fmt in ["html", "latex"] }
73+
MASTER_DOC = os.path.abspath("index.rst")
74+
75+
# Add extra cases here to support more formats
76+
def copy_master_doc(app):
77+
for fmt, rst_path in SUPPORTED_FORMATS.items():
78+
if app.tags.has(fmt):
79+
copyfile(rst_path, MASTER_DOC)
80+
break
81+
else:
82+
MSG = """Unexpected builder; expected one of {!r}.
83+
Add support for this new builder in `copy_master_doc` in conf.py."""
84+
from sphinx.errors import ConfigError
85+
raise ConfigError(MSG.format(list(SUPPORTED_FORMATS.keys())))
86+
87+
def setup(app):
88+
app.connect('builder-inited', copy_master_doc)
89+
6990
# The master toctree document.
70-
master_doc = 'index'
91+
# We create this file in `copy_master_doc` above.
92+
master_doc = "index"
7193

7294
# General information about the project.
7395
project = 'Coq'
@@ -104,6 +126,8 @@
104126
'Thumbs.db',
105127
'.DS_Store',
106128
'introduction.rst',
129+
'index-*.rst', # One of these gets copied to index.rst in `copy_master_doc`
130+
'refman-preamble.rst',
107131
'README.rst',
108132
'README.template.rst'
109133
]
@@ -267,12 +291,12 @@
267291
'papersize': 'letterpaper',
268292
'classoptions': ',openany', # No blank pages
269293
'polyglossia' : '\\usepackage{polyglossia}',
270-
'microtype' : '\\usepackage{microtype}',
271294
"preamble": r"""
272295
\usepackage{unicode-math}
296+
\usepackage{microtype}
273297
274298
% Macro definitions
275-
\input{preamble.tex}
299+
\usepackage{refman-preamble}
276300
277301
% Style definitions for notations
278302
\usepackage{coqnotations}
@@ -286,21 +310,15 @@
286310
########
287311

288312
latex_additional_files = [
289-
"preamble.tex",
313+
"refman-preamble.sty",
290314
"_static/coqnotations.sty"
291315
]
292316

293-
# Grouping the document tree into LaTeX files. List of tuples
294-
# (source start file, target name, title,
295-
# author, documentclass [howto, manual, or own class]).
296-
latex_documents = [
297-
(master_doc, 'CoqRefMan.tex', 'Coq Documentation',
298-
'The Coq Development Team', 'manual'),
299-
]
317+
latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
300318

301319
# The name of an image file (relative to this directory) to place at the top of
302320
# the title page.
303-
latex_logo = "../../ide/coq.png"
321+
# latex_logo = "../../ide/coq.png"
304322

305323
# If true, show page references after internal links.
306324
#latex_show_pagerefs = False

‎doc/sphinx/credits.rst

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,5 @@
1-
.. include:: preamble.rst
2-
.. include:: replaces.rst
3-
41
.. _credits:
52

6-
-------------------------------------------
7-
Credits
8-
-------------------------------------------
9-
103
Coq is a proof assistant for higher-order logic, allowing the
114
development of computer programs consistent with their formal
125
specification. It is the result of about ten years of research of the

‎doc/sphinx/index.rst renamed to ‎doc/sphinx/index-html.rst

Lines changed: 16 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,16 @@
1-
.. include:: preamble.rst
2-
.. include:: replaces.rst
1+
==========================
2+
The Coq Reference Manual
3+
==========================
4+
5+
.. _introduction:
6+
7+
Introduction
8+
------------
39

410
.. include:: introduction.rst
511

6-
------------------
712
Table of contents
8-
------------------
13+
-----------------
914

1015
.. toctree::
1116
:caption: Indexes
@@ -80,12 +85,12 @@ Table of contents
8085

8186
zebibliography
8287

83-
This material (the Coq Reference Manual) may be distributed only subject to the
84-
terms and conditions set forth in the Open Publication License, v1.0 or later
85-
(the latest version is presently available at
86-
http://www.opencontent.org/openpub). Options A and B are not elected.
88+
License
89+
-------
90+
91+
.. include:: license.rst
8792

8893
.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
89-
Optionally, you can enhance it with the minor mode
90-
Company-Coq :cite:`Pit16`
91-
(see https://github.com/cpitclaudel/company-coq).
94+
Optionally, you can enhance it with the minor mode
95+
Company-Coq :cite:`Pit16`
96+
(see https://github.com/cpitclaudel/company-coq).

‎doc/sphinx/index-latex.rst

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
==========================
2+
The Coq Reference Manual
3+
==========================
4+
5+
Introduction
6+
------------
7+
8+
.. include:: introduction.rst
9+
10+
Credits
11+
-------
12+
13+
.. include:: credits.rst
14+
15+
License
16+
-------
17+
18+
.. include:: license.rst
19+
20+
The language
21+
------------
22+
23+
.. toctree::
24+
25+
language/gallina-specification-language
26+
language/gallina-extensions
27+
language/coq-library
28+
language/cic
29+
language/module-system
30+
31+
The proof engine
32+
----------------
33+
34+
.. toctree::
35+
36+
proof-engine/vernacular-commands
37+
proof-engine/proof-handling
38+
proof-engine/tactics
39+
proof-engine/ltac
40+
proof-engine/detailed-tactic-examples
41+
proof-engine/ssreflect-proof-language
42+
43+
User extensions
44+
---------------
45+
46+
.. toctree::
47+
48+
user-extensions/syntax-extensions
49+
user-extensions/proof-schemes
50+
51+
Practical tools
52+
---------------
53+
54+
.. toctree::
55+
56+
practical-tools/coq-commands
57+
practical-tools/utilities
58+
practical-tools/coqide
59+
60+
Addendum
61+
--------
62+
63+
.. toctree::
64+
65+
addendum/extended-pattern-matching
66+
addendum/implicit-coercions
67+
addendum/canonical-structures
68+
addendum/type-classes
69+
addendum/omega
70+
addendum/micromega
71+
addendum/extraction
72+
addendum/program
73+
addendum/ring
74+
addendum/nsatz
75+
addendum/generalized-rewriting
76+
addendum/parallel-proof-processing
77+
addendum/miscellaneous-extensions
78+
addendum/universe-polymorphism
79+
80+
.. No need for an explicit bibliography entry in the toc: it gets picked up
81+
from ``zebibliography.rst``.

‎doc/sphinx/introduction.rst

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,5 @@
1-
.. _introduction:
2-
3-
------------------------
4-
Introduction
5-
------------------------
1+
.. include:: preamble.rst
2+
.. include:: replaces.rst
63

74
This document is the Reference Manual of the |Coq| proof assistant.
85
To start using Coq, it is advised to first read a tutorial.

‎doc/sphinx/license.rst

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
This material (the Coq Reference Manual) may be distributed only subject to the
2+
terms and conditions set forth in the Open Publication License, v1.0 or later
3+
(the latest version is presently available at
4+
http://www.opencontent.org/openpub). Options A and B are not elected.

‎doc/tools/coqrst/coqdomain.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -620,12 +620,12 @@ class PreambleDirective(Directive):
620620
621621
.. preamble:: preamble.tex
622622
"""
623-
624623
has_content = False
625624
required_arguments = 1
626625
optional_arguments = 0
627626
final_argument_whitespace = True
628627
option_spec = {}
628+
directive_name = "preamble"
629629

630630
def run(self):
631631
document = self.state.document

0 commit comments

Comments
 (0)