Add Documentation for Elaborator Reflection

[martinbaker]

This adds new pages to the documentation to attempt to explain Elaborator Reflection.

Existing documentation pages are not changed except:

docs/index.rst - links are added to the new pages and
the section title is changed to 'Theorem Proving and Elaborator Reflection' to reflect the new content.

docs/conf.py - added table width fix for Read the Docs Sphinx theme as explained here:
https://rackerlabs.github.io/docs-rackspace/tools/rtd-tables.html
Without this change the tables would be extremely wide which would make them unusable.

[david-christiansen]

Thanks for doing this! I'll review soon!

[david-christiansen]

Thank you for this Herculean documentation effort!

I don't think these docs are quite ready to be merged yet. After sitting here for a couple of hours, there's still some left that I haven't had time to look at carefully. I'll make time when I can, but I am doing two jobs at the moment so my time is somewhat limited. I wrote a lot of comments, but most of them should be easy to either fix or decide that you're not doing them.

Generally, a lot of my comments are little nitpicky writing things, like making sure that the word "we" is used to refer to a consistent person or people, making sure that there's always appropriate singular/plural forms or definite/indefinite articles, or avoiding comma splices. I think I need to give it another round of proofreading when it's not late at night, but this is at least some things to look at so far.

As far as high-level concerns go, it looks like a lot of this text is copied and pasted from the built-in documentation, and then modified and extended. I don't think this is a sustainable way to document Idris. In particular, there's now two things to keep synchronized, and people who get their docs from one place or another will miss the information that's in only one of them. I recommend leaving the API docs in Idris itself, and reminding the reader how to find them. If they need to be improved, please improve them in the Idris library source code instead.

I appreciate the desire to use pictures, but I have two high-level concerns with the specific pictures here. The first is that we don't have the source files included in the repository, so anyone who needs to update them will have to recreate them. The second is that some of the content is only in the PNG files, and PNG files are not particularly accessible by people who can't see or by people using screen resolutions that we don't anticipate today. I think many of the pictures can be replaced by a textual version, some are not particularly necessary, and others are highly valuable but would benefit from text that contains the same information. I've indicated these in the comments.

I can tell you've done a lot of hard work on this. Thank you for catching up with what I didn't make happen after I graduated. I know I left a lot of little comments: they're intended in the spirit of making this as good as possible, and I hope that it's not too overwhelming.

[martinbaker]

@david-christiansen

Thank you for your comments so far.

I'll work through and resolve your detailed comments, at first glance, I tend to agree with most of them.

Regarding the high level-concerns:

I agree with the general principle that content should not be duplicated but I also think its a bad principle that new users should be forced to read the source code (or API doc) to find what commands are available.
In the case of:
https://github.com/martinbaker/Idris-dev/blob/mydoc/docs/proofs/primative.rst
The problem I have (and I'm assuming other people may have) is to get an overview of all the operators (tactics) so I really do want to have all the tactics together, in one big table, so I stand the best chance of choosing the correct one. If a (meta) programmer already has some clue about what the need then they can use the search tools but new users don't know what to search for. Even for experienced users, I think its valuable to have all the information together in a compact form.

As you say "a lot of this text is copied and pasted from the built-in documentation, and then modified and extended" but I would like this to only be a first step to documentation aimed at users rather than developers. I think there is a lot more that needs to be done here but I this is the best I can do for now. What I would really like is a diagram for each tactic showing the state before, the state after and arrows between them so users can pick out what they need visually.

Regarding pictures:

I can include a SVG and a PNG file for each picture. The SVG file, being vector graphics, is best for drawing and modifying (using Inkscape) and PNG, being raster graphics, gives more consistent rendering. I can add a readme explaining how to generate the PNG from the SVG.

I appreciate that everyone is different in what type of documentation appeals to them. Personally I'm put off by big blocks of text but I find visual clues really help me find what I'm looking for. I also imagine that people would be using the documentation in different ways, I imagine a high proportion would be quickly scanning to try to find a particular piece of information.

[zenntenn]

In terms of accessibility of images, including images is fine, as long as they are tagged properly so those using screen readers understand what they are, and that someone using a screen reader can still get all the information they need from the documentation without them. Basically, a visual aid to help grasp the text better but contributes no new information is fine, at least when it comes to accessible best practices.

[martinbaker]

I think I have made the changes to this pull request that I intend to do, for now.

It is getting very unwieldy and it would be good to get it to where you could accept it. Then, future updates could be done in more digestible chunks.

I think its a lot better than it was due to your helpful reviews.

I think a lot more work needs to be done, to this documentation, before it is in a state where it presents all the information a potential meta-programmer needs. However, any contribution I can make would be easier if spread out into smaller sub-goals.

Martin

[david-christiansen]

I'll look again as soon as I get some free time. Thanks for the hard work! Den tor. 23. maj 2019 kl. 04.28 skrev martinbaker <[email protected]

…

: I think I have made the changes to this pull request that I intend to do, for now. It is getting very unwieldy and it would be good to get it to where you could accept it. Then, future updates could be done in more digestible chunks. I think its a lot better than it was due to your helpful reviews. I think a lot more work needs to be done, to this documentation, before it is in a state where it presents all the information a potential meta-programmer needs. However, any contribution I can make would be easier if spread out into smaller sub-goals. Martin — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4700?email_source=notifications&email_token=AAA4FASZKSPG3MO65BT35P3PWZ5XVA5CNFSM4HLTFEBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODWB5OVY#issuecomment-495179607>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAA4FAST3TFY2R4HMZKOHT3PWZ5XVANCNFSM4HLTFEBA> .

[martinbaker]

I have now updated the diagrams, in the example, which show the holes and what they depend on.

They now separate the holes into different columns, I think this makes it much clearer.
I have also removed the confusing references to 'logic diagrams'.

Hopefully this documentation now explains elaborator reflection better.

[david-christiansen]

Thanks for keeping at this! I haven't forgotten you - I've just had a lot of work and travel. But the class I was teaching has finished, and my trip is done, so I should have some time this coming weekend.

Sorry for the delay.

[martinbaker]

so I should have some time this coming weekend.

Thats great!

I have just added a page about the notation for holes and guesses, I did not want the helpful information you gave to my forum question to get lost.

Regarding the elaborator reflection documentation as a whole: I am hoping that this pull request could just be the start, I think that a lot more documentation is needed, for example:

• More information is needed describing individual tactics such as 'attack'. The sort of information that is in your joint paper with Edwin. In addition I would really like to see a minimal example for each tactic. I would also like to have a diagram showing showing how each tactic modifies the state, I am just trying to find a fast way for a user to find the tactic required without searching lots of wordy text. I know you are concerned that what I have done, so far, duplicates the API documentation with some additional information. I just think a potential user needs a lot more than is in the API and what I have done so far is just intended as a framework to be improved later.

• I think a more motivational introduction is required to elaborator reflection and metaprogramming, when it is useful to customise the language, various methods of implementing domain specific languages and so on. I think this is best coming from you (but I could try to paraphrase your thesis if you want!).

I know you would prefer this all to be in a top-level metaprogramming section of its own, separated from proofs. But where would common information (like tactics) go? Should tactics should be separated out into a third section?
I think a rearrangement will be required, at the moment there is:

• A page about theorem proving in the introduction section.
• A top-level section about theorem proving and elaborator reflection.
• A page about elaborator reflection in the language reference section.
  So a lot of swapping around does seem to be required but would it be simpler and less messy to do that as a separate exercise later?

By the way, I have been checking the html produced by running sphinx from the command line like this:

sphinx-build -b html Idris-dev/docs IdrisDoc

You may find there are less artifacts in the diagrams when viewed this way?

I may be using a newer version of sphinx than readthedocs, but I have used very standard markup, so it seems unlikely to make a difference.

Martin

[melted]

I'm pretty sure the travis failure is because this is based on a commit where stack wasn't working. So it should be fine.

[martinbaker]

I was hoping to extend and improve this documentation further but I don't really want to do more until I know if this pull request will be accepted.

I guess you are busy on other things but I'm not sure how to allocate my own time at the moment. If this pull request is not helpful please let me know as I don't want to waste your time and mine.

Martin

[melted]

No worries about it being accepted, it's going in. But yeah, let's not put more stuff into the PR now, so we can merge something. It's always possible to expand it later.

@david-christiansen Any time for review?

[david-christiansen]

I hope to have time soon! I've been feeling quite overwhelmed with everything lately - sorry!

[melted]

This PR represents too much work to be left hanging, so I'll merge it.