Abella documentation is woefully incomplete

[chaudhuri]

Please list here things that you were not able to find good documentation for. This will let us prioritize what needs to be fixed/updated.

[lambdacalculator]

Here is a list to get things started:

• The "For those who aren't familiar with the logic" section should be expanded to include enough information for the intended audience. What of those with little or no exposure to lambda-Prolog?
• Update the blurb in the description of Define concerning stratification. What, exactly, is the condition being enforced?
• Split doesn't apply only to mutually inductive theorems, although that is its main use case.
• Set should list all available options (at least subgoals and types have been updated/added).
• The tactic section should begin with a description of hypothesis naming as well as *hypothesis consumption, so the tactics that use it have something to refer to.
• Update induction to include alternating quantifiers and implications, with perhaps an example.
• search should include a rough description of the search procedure, so that users can quickly learn what to expect, as well as a clearer definition of search depth, since it is a parameter to other tactics.
• Update descriptions of unfold, exists/witness, clear.
• The description of Close contains an inconsistency: at first, in both the top-level command section and the subordination section, we are told that the tactic will close all subordinates of a list of types, but later in the same paragraph of the subordination section that we have to close them ourselves (which I believe is correct).

It would also be nice to have somewhere an annotated directory of the examples, briefly describing what each example is about, as well as which technical aspects of theorem proving in Abella are illustrated by those examples.

[chaudhuri]

Thanks Todd. I took the liberty of turning your bullets into checkboxes.

About the annotated directory, I am not sure if it makes sense to divide them up based on what features of Abella they use. We can perhaps improve this page a bit.

[lambdacalculator]

I wasn't suggesting reorganizing the examples in any way; I think the current organization is just fine. I was just thinking that a title alone is not enough information for someone looking for ideas on how to organize a development. Perhaps a brief paragraph on each example, with information on what techniques are illustrated by the example, would go a long way to help someone looking for ideas. I could try doing a few to illustrate better what I'm suggesting.

Also, it would be nice if there were a way to add a stylized comment in the example code itself that is automatically picked up by the website generation tool and turned into the blurb in the directory.

[chaudhuri]

Yes, @ThatDaleMiller and I have been discussing how to add a little bit of literate programming support to Abella so that we can interleave documentation and code in a web-page. We can try to steal ideas from Literate Haskell, Isabelle, Coq. or even use some turnkey solution such as noweb.

[amerikan]

It will be good to consider this for: abella-prover/abella-prover.org#4

[ThatDaleMiller]

I have updated this document with more about stratification.