Improve web page generation

[chaudhuri]

• [ ] Abella should output XML or sexps or something that doesn't require guesswork
• [ ] Need to remove the dependency on OMake.
• [ ] Consider rewriting the web-page generation code in OCaml

[amerikan]

https://github.com/abella-prover/abella-prover.org/issues/4 just referencing.

[lambdacalculator]

Is there any plan to revamp the generation of html versions of developments? I'm re-building my PFPL development in Abella 2.0.6 and would like to make the whole thing available to students. Ideally, users should be able to type abella --html devel.thm or abella2html devel.thm and get HTML output in devel.html and devel-details.html.

[lambdacalculator]

One additional idea: when building the HTML, run abella with witnesses=on and use the information generated to enable display of search witnesses when hovering over the search tactic in a proof.

[chaudhuri]

There are always plans. I wish I had more time to spare to fix up all the weird corners of Abella. We are trying to hire a full time engineer to work on it.

For the time being you can make Abella-like web site output by putting your code in a subdirectory of abella/examples and running omake -j 1 upload-html. You will need to have omake (opam install omake) and Ruby with erb (apt-get install ruby erb). You will need to run this from the Abella source distribution, not the version installed with OPAM. The generated files for foo.thm will be called foo.html and foo-details.html, which you can freely move to any other location.

[lambdacalculator]

OK, thanks. As an aside, I noticed that this process only works if I copy all of my files to a directory in abella/examples; it doesn't work if I simply add a symbolic link there to my own repository. Is there a reason that omake doesn't follow symbolic links or provide an option that requests that it does? I couldn't find anything in the documentation that answers this.

[chaudhuri]

I don't know why the $(subdirs) directive of omake doesn't chase symlinks, sorry.

[amerikan]

I have started building a simple version of this, however, it's in Python 3.5, is there a preference in ecosystem?

To start I am keeping it simple, for example, python abella2html.py path/to/thm/myproof.thm would generate a simple myproof.html file. A later iteration can include folder and generate all .thm files in it.

[amerikan]

Here's the implementation: https://github.com/amerikan/abella2html

Note: currently it generates the "details" html

[amerikan]

Example preview of generated html: