Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bump Sphinx to 4.5.0 #17772

Merged
merged 3 commits into from Jun 30, 2023
Merged

Bump Sphinx to 4.5.0 #17772

merged 3 commits into from Jun 30, 2023

Conversation

ana-borges
Copy link
Contributor

@ana-borges ana-borges commented Jun 28, 2023 •
edited

To obtain / as a quick search shortcut and Esc as a shortcut to remove search highlighting.
Sphinx 4.5.0 was released in March 2022.

Fixes / closes #15778

  • [ ] Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • [ ] Documented any new / changed user messages.
    • [ ] Updated documented syntax by running make doc_gram_rsts.
  • [ ] Opened overlay pull requests.

@ana-borges ana-borges requested review from a team as code owners June 28, 2023 07:43
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 28, 2023
@ana-borges ana-borges added kind: documentation Additions or improvement to documentation. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 28, 2023
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 28, 2023
Zimmi48
Zimmi48 approved these changes Jun 28, 2023
View reviewed changes
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
Just FWIW, Debian's new stable version, that was released earlier this month, has Sphinx 5.3.0 packaged.

doc/changelog/11-standard-library/17772-bump-sphinx.rst Outdated Show resolved Hide resolved
@ana-borges
Bump Sphinx to 4.5.0
6fab43f 
To obtain / as a quick search shortcut and Esc as a shortcut to remove
search highlighting.
Sphinx 4.5.0 was released in March 2022.
@Zimmi48
Copy link
Member

Zimmi48 commented Jun 29, 2023 •
edited

On my computer, when testing the refman artifact generated from this PR, it looks like the search feature is broken (never returns):

image

@Zimmi48

This comment was marked as resolved.

Sign in to view
@Zimmi48 Zimmi48 mentioned this pull request Jun 29, 2023
Merged
@ana-borges
Copy link
Contributor Author

This was a much deeper rabbit hole than expected. Here are some findings:

  • Inspecting a local copy of the docs does not necessarily behave like inspecting a version generated by CI due to the url being of the form /home/bla/... instead of http://bla/....
    In particular, Search doesn't give any results if using the former url in my machine, although it does in Théo's. However, it doesn't show summaries of each result, as shown above.
    In order to get around both problems we can run a local server, for example with python3 -m http.server

  • Finding combinations of python packages that work together is not always trivial. Some combinations of versions, specially very old + very recent are accepted by pip but lead to build failures for the doc.

@ana-borges ana-borges mentioned this pull request Jun 29, 2023
Merged
@ana-borges
Try with a more recent version of docutils and rtd
f8594f4 
rtd because apparently there is a known incompatibility with old rtd and
recent sphinx versions, and docutils because that's the version I have
locally and it probably got bumped automatically due to constraints with
the other versions, although I didn't check. Let's see what happens
Zimmi48
Zimmi48 reviewed Jun 30, 2023
View reviewed changes
doc/README.md Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 self-assigned this Jun 30, 2023
@Zimmi48 Zimmi48 added this to the 8.19+rc1 milestone Jun 30, 2023
@Zimmi48 Zimmi48 removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 30, 2023
@Zimmi48
Copy link
Member

Zimmi48 commented Jun 30, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 3154ae5 into coq:master Jun 30, 2023
2 of 3 checks passed
@Zimmi48 Zimmi48 mentioned this pull request Jun 30, 2023
Closed
@ana-borges ana-borges deleted the bump-sphinx branch July 5, 2023 14:33
@ana-borges ana-borges added this to Request 8.18+rc1 inclusion in Coq 8.18 Jul 5, 2023
@ana-borges ana-borges modified the milestones: 8.19+rc1, 8.18+rc1 Jul 5, 2023
gares added a commit to gares/coq that referenced this pull request Jul 7, 2023
@gares
Backport PR coq#17772: Bump Sphinx to 4.5.0
eff34ca
@coqbot-app coqbot-app bot moved this from Request 8.18+rc1 inclusion to Shipped in 8.18+rc1 in Coq 8.18 Jul 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

Assignees

@Zimmi48 Zimmi48

Labels
kind: documentation Additions or improvement to documentation.
Projects
Coq 8.18
Shipped in 8.18+rc1
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

The highlighted search terms in the online refman are annoying
2 participants
@ana-borges @Zimmi48