Current master fails to build docs - requires sphinxcontrib.jquery

[mouse07410]

Current master fails to build docs - requires sphinxcontrib.jquery

[andreasabel]

The PR #6821 you referred to seems to say that bumping sphinx_rtd_theme to 1.2.2 fixed the issue?

I tried several things, browsing existing rtd issues. The bump to 1.2.2 alone was not sufficient.
One problem is that search is broken:

• on PR builds
• on local builds

So, basically the only way to test it is to deploy (push to master).

I am a bit unwilling now before the release 2.6.4 to do further sphinx experiments because:

• the deployed page on readthedocs works
• the PDF build works in CI, on rtd, and locally on my machine

So I suggest that for now you settle with a workaround, i.e., either get the PDF from

• CI, e.g. the artifact in https://github.com/agda/agda/actions/runs/6304153063
• rtd
• or via a patch you apply locally.

It would be easier to work on this issue if upstream fixed their bug:

• readthedocs/readthedocs.org#10714

[andreasabel]

Mmh, I just introduce the sillly dependency in

• #6821

Without it, the "Search" page was just broken (not displaying any results).

On my macOS Monterey, make user-manual-pdf just works. I am not using Macports though, just homebrew and pip.

[mouse07410]

Without it, the "Search" page was just broken (not displaying any results).

The PR #6821 you referred to seems to say that bumping sphinx_rtd_theme to 1.2.2 fixed the issue?

And on my macOS Ventura make user-manual-pdf just does not work, as shown above. Homebrew vs. Macports shouldn't really matter - except that neither Macports nor "straight" pip could locate/fetch sphinxcontrib.jquery, and of course README.md did not bother mentioning this new dependency that isn't ubiquitous availability-wise.

[mouse07410]

Funny. I found and installed sphinxcontrib.jquery (turned out, system-wide sudo pip failed, while user-level pip succeeded), but on two different MacOS machines (Intel and Apple Silicon) building docs fails:

======================================================================
========================= User manual (PDF) ==========================
======================================================================
gmake[1]: Entering directory '/Users/ur20980/src/agda/doc/user-manual'
Running Sphinx v7.2.6
building [mo]: targets for 0 po files that are out of date
writing output... 
building [latex]: all documents
updating environment: [new config] 72 added, 0 changed, 0 removed
reading sources... [100%] tools/search-about
looking for now-outdated files... none found
pickling environment... done
checking consistency... done
copying TeX support files... copying TeX support files...
done
copying additional files...  unicode-symbols-sphinx.tex.txtdone
processing Agda.tex... index overview getting-started/index getting-started/what-is-agda getting-started/installation getting-started/hello-world getting-started/a-taste-of-agda getting-started/tutorial-list language/index language/abstract-definitions language/built-ins language/coinduction language/copatterns language/core-language language/coverage-checking language/cubical language/cubical-compatible language/cumulativity language/data-types language/flat language/foreign-function-interface language/function-definitions language/function-types language/generalization-of-declared-variables language/guarded language/implicit-arguments language/instance-arguments language/irrelevance language/lambda-abstraction language/let-and-where language/lexical-structure language/literal-overloading language/lossy-unification language/mixfix-operators language/module-system language/mutual-recursion language/opaque-definitions language/pattern-synonyms language/positivity-checking language/postulates language/pragmas language/prop language/record-types language/reflection language/rewriting language/runtime-irrelevance language/safe-agda language/sized-types language/sort-system language/syntactic-sugar language/syntax-declarations language/telescopes language/termination-checking language/two-level language/universe-levels language/with-abstraction language/without-k tools/index tools/auto tools/command-line-options tools/compilers tools/emacs-mode tools/literate-programming tools/generating-html tools/generating-latex tools/interface-files tools/package-system tools/performance tools/search-about contribute/index contribute/documentation team 
resolving references...
done
writing... done
copying images... [100%] agda.svg
build succeeded.

The LaTeX files are in _build/latex.
Run 'make' in that directory to run these through (pdf)latex
(use `make latexpdf' here to do that automatically).
Traceback (most recent call last):
  File "/opt/local/bin/sphinx-build", line 8, in <module>
    sys.exit(main())
             ^^^^^^
  File "/opt/local/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/sphinx/cmd/build.py", line 339, in main
    return make_main(argv)
           ^^^^^^^^^^^^^^^
  File "/opt/local/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/sphinx/cmd/build.py", line 213, in make_main
    return make_mode.run_make_mode(argv[1:])
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/local/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/sphinx/cmd/make_mode.py", line 180, in run_make_mode
    return getattr(make, run_method)()
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/local/Library/Frameworks/Python.framework/Versions/3.11/lib/python3.11/site-packages/sphinx/cmd/make_mode.py", line 111, in build_latexpdf
    raise RuntimeError('Invalid $MAKE command: %r' % makecmd)
RuntimeError: Invalid $MAKE command: 'gmake'
gmake[1]: *** [Makefile:19: latexpdf] Error 1
gmake[1]: Leaving directory '/Users/ur20980/src/agda/doc/user-manual'
gmake: *** [Makefile:358: user-manual-pdf] Error 2

Any idea what could be wrong???

[mouse07410]

@andreasabel any idea what is the problem here?

[L-TChen]

Do you have GNU make installed?

[mouse07410]

Do you have GNU make installed?

Yes I do - Apple make and GNU make (under the name of gmake).

[L-TChen]

Humm, it says your make command is invalid. sphinx should produce a Makefile in the directory _build/latex which basically just runs latexmk to compile Agda.tex as a PDF. So, please check if you have mactex (texlive) installed and see if you can compile Agda.tex to PDF directly.

I checked the target user-manual-pdf with my (relatively) new Mac mini and it works fine.

[L-TChen]

I am closing this issue for now, as the original issue with sphinxcontrib.jquery has been fixed and I am not able to reproduce the issue with compiling LaTeX files in _build/latex to PDF on macOS 14.

@mouse07410, please open another issue if the problem persists after the instructions suggested above.