maximedenes / coq Goto Github PK

Version

8.8

Operating system

any

Description of the problem

Things that should be checked for the final Sphinx version of the manual:

• all chapter names, sections use the same syntax (===, ---,~~~,+++)
• resolve all TODO cross-reference
• all biblio references are used
• index entries are OK
• a per-chapter TOC at the top of each chapter

Version

8.8+alpha

Operating system

Linux x64

Description of the problem

Configure Coq with -natdynlink no. Then make sphinx. You get errors like:

Exception occurred:
  File "/usr/local/lib/python3.5/dist-packages/pexpect/expect.py", line 70, in timeout
    raise TIMEOUT(msg)
pexpect.exceptions.TIMEOUT: Timeout exceeded.
<pexpect.pty_spawn.spawn object at 0x7f12cb311c18>
command: /home/steck/sphinx-migration/coq/bin/coqtop
args: [b'/home/steck/sphinx-migration/coq/bin/coqtop', b'-color', b'on']
buffer (last 100 chars): '\r\n[Loading ML file fourier_plugin.cmxs ... done]\r\n[Loading ML file micromega_plugin.cmxs ... done]\r\n'
before (last 100 chars): '\r\n[Loading ML file fourier_plugin.cmxs ... done]\r\n[Loading ML file micromega_plugin.cmxs ... done]\r\n'
after: <class 'pexpect.exceptions.TIMEOUT'>

When building the Sphinx docs, if there's an ANTLR error, it doesn't indicate a line number, making it hard to find the error.

The migration is starting with the online 8.7 manual. Any changes to the docs post-8.7 should be added to Sphinx.

The current sphinx html output does not give numbered sections unless the :numbered:
option is given to the toctree directive. But even if that is done, the section numbers
restart at each toctree directive. Since we currently use a separate toctree directive
for each part this is a problem since we would like to have one contiguous sequence of chapter numbers.

Version

Commit 28ce265713 of the sphinx/ssr branch

Operating system

Linux/Ubuntu

Description of the problem

If sphinx becomes a way to build coqtop, what about testing and displaying its availability at configure time?