Is the tool generating html outputs on hompage openly available?

[안기영]

Hello,

The example pages on the homepage seems to be automatically generated from an annotated output and its accompanying source code, which is much better than just having the annotated output option from Abella, but the tool used for that does not seem to be part of the repository. Do you have plans to distribute them as well at some point? Or, is it already out there as an undocumented feature?

Cheers,

[Kaustuv Chaudhuri]

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

[Yuting Wang]

I just found out that the OMakefile for generating html files breaks in Omake version 0.10.1. I reverted back to version 0.9.8.6-0.rc1 and the OMakefile works.

Just to let you know in case you have encountered the same problem.

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.
To post to this group, send email to abella-theorem-prover@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

[Jonas Kaiser]

HI, I was just wondering, if any progress has been made in this area?

cheers,

Jonas

[Todd Wilson]

I'll second this expression of wondering. I just added a question on the relevant ticket (Improve webpage generation, #9) to get it into the system, along with an idea about how search witnesses could be used.