idris-lang/Idris-dev

Readthedocs not tracking Idris Github

martinbaker opened this issue · 12 comments

martinbaker commented

The idris documentation on 'Read the Docs' here:
http://docs.idris-lang.org/en/latest/
is out of date, that is, it is not tracking the documents in Github.

I think its important that this is up to date because, if people search for Idris information on the internet, this is what they are likely to find.

I tried to look into this and found the following:
https://readthedocs.org/projects/docs/downloads/pdf/latest/

"Last year, GitHub announced that effective Jan 31st, 2019, GitHub Services will stop working. This means GitHub will stop sending notifications to Read the Docs for projects configured with the ReadTheDocs GitHub Service.If your project has been configured on Read the Docs for a long time, you are most likely still using this service to automatically build your project on Read the Docs.In order for your project to continue automatically building, you will need to configure your GitHub repository with a new webhook."

Could this be the reason?

Please could the person with the Idris readthedocs administer account look into this.

I suspect there may be a shortage of people to do this administration, is there anything I can do to help?

melted commented

@jfdm Can you help with this?

LeifW commented

HTML version of doc on setting up the Github webhook for ReadTheDocs: https://docs.readthedocs.io/en/stable/webhooks.html#github

martinbaker commented

To set up this webhook it looks like someone needs to:

  • go to Admin > Integrations > Add integration dashboard page on the Read the Docs account.
  • go to Settings > Webhooks > Add webhook on the github project page.

So it looks like it needs someone with administrator access to both Read the Docs and github accounts for Idris.

Is there anyone who needs to be lobbied to do this?

I think its important this is fixed. At the moment anyone who searches online for Idris documentation will get something that is very out of date. This tells uses that the latest version of Idris is v1.3.1. I think this will give a bad impression to potential new uses and discourage anyone from improving the documentation.

melted commented

Only @edwinb and @david-christiansen have admin rights, so let's see if they notice naming them. You could try Slack too.

jfdm commented

@melted is correct here, although I took the necessary steps on readthedocs.io @edwinb and @david-christiansen have the requisite rights for github.

edwinb commented

Thanks for flagging. I believe I've done the necessary fiddling now. There is a build error on readthedocs, related to pdf generation I think, but the web documentation is up to date again.

jfdm commented

I've fixed the PDF generation in #4825. Can we close this now?

martinbaker commented

I'm away from my main computer at the moment, so I may not be reading this correctly, but it looks to me like the PDF generated by readthedocs and the one on GitHub are both from the old documentation on idris-tutorial rather than the new documentation in idris-dev/doc.

Is this the intention?

jfdm commented

The PDF within the project root was freshly generated and added from the Idris sources, and checking the output from the build for RTD shows that the PDF for 'latest' is from the latest sources.

martinbaker commented

OK I think I have worked out what is confusing me. When I look at the HTML pages I get the following chapters:

  • The Idris Tutorial
  • Frequently Asked Questions
  • Implementing State-aware Systems in Idris: The ST Tutorial
  • The Effects Tutorial
  • Theorem Proving
  • Elaborator Reflection
  • Lexer and Parser Library
  • Language Reference
  • Tutorials on the Idris Language

But when I look at the PDF file I only get the first of these chapters. Is this the intention? If so I suggest closing this issue and I will think about starting another issue as I think this could also be confusing to others.

Thanks for the work you have done on this, it's certainly fixed the important issue and finding documentation is lot better than it was.

melted commented

Sounds good all around, so let's close.

jfdm commented

Just to confirm with @martinbaker you are correct.

The PDF we generate using RTD is for the Idris Tutorial only. We used to specify it for generating the 'complete' documentation, and the tutorial as a stand alone document. However, RTDs doesn't like it when there are multiple targets for LaTeX. Thus in #4825 I went for the tutorial only.

If there is a big push for the complete documentation to be generated as a PDF then that can be arranged.