The script is in the examples/ directory of the Abella source
distribution but it is not easy to use and is not documented.
Roughly:
1. Make sure that you have Ruby and omake (opam install omake).
2. Put your development in a subdirectory of the examples/ directory,
say examples/foo/ or examples/logic/foo/. Make sure that the abella
binary is present as examples/../abella (it can be a symbolic link).
3. From the examples/ directory, run: omake upload-html
4. This will recreate the HTML files for all recursive subdirectories
of examples/. You may want to delete or move the examples from the
Abella distribution you don't care about. Leave the
examples/html-files directory alone though.
5. The generated examples.tar.gz file packages things up in a form
that can be uploaded to a web-server.
Plenty of things are hard-coded in the generated HTML files, such as
links to the Abella web-site's style files and the Abella logo. If you
know some Ruby, you can perhaps try to modify
examples/html-files/annotate_thm.rb to change the hard-coded defaults.
This is all very hacky at the moment, of course. The Ruby script in
particular uses regular expressions and optimism to "parse" the Abella
sources, and often gets things wrong. Relevant issue:
<
https://github.com/abella-prover/abella/issues/9>.
Kaustuv