Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Wiki documentation seems outdated

Open ribosomerocker opened this issue 1 year ago • 3 comments

Specifically, in the wiki's "State of Idris 2 documentation" "documentation we wish we had" section, you mention that you wish you had:

a FAQ a tutorial on quantities a tutorial for how to use the REPL and it's commands

for the first two, i believe that

  • https://idris2.readthedocs.io/en/latest/faq/faq.html
  • https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html

are perfect as they are. But for the third one, I think it does need work, but there's already a fairly decent base at https://idris.readthedocs.io/en/latest/reference/repl.html, it just needs to be updated.

furthermore, in the community i've seen links like

  • https://www.idris-lang.org/docs/idris2/current/base_docs/
  • https://idris2docs.sinyax.net/

exchanged around, which would certainly be really useful to have on the idris2.readthedocs.io page and also here on the wiki. also, it would be nice to have a separate issue template for documentation and a tag for it too, as that's a very important part in my opinion.

ribosomerocker avatar Jul 29 '22 06:07 ribosomerocker

Thank you for pointing this out. The wiki is free to modify, would you (or someone else) be willing to perform the necessary updates?

andrevidela avatar Sep 19 '22 19:09 andrevidela

Yes. I wanted to do this way earlier, but I just didn't have the time. I'll get to it soon, though the one part I can't do is add a "documentation" issue template. I was also trying to get some more suggestions on the Discord server, though I haven't been very successful with that.

ribosomerocker avatar Sep 19 '22 22:09 ribosomerocker

I've added those last two links to the wiki and mentioned the first links in the wiki discussion

I do think there are more things that need adding to FAQs - a number of questions raised frequently on discord aren't in there

joelberkeley avatar Sep 21 '22 19:09 joelberkeley