abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
90 stars 18 forks source link

Improve web page generation #9

Open chaudhuri opened 11 years ago

chaudhuri commented 11 years ago
amerikan commented 6 years ago

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

lambdacalculator commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

amerikan commented 5 years ago

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 commented 5 years ago

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

Note: currently it generates the "details" html

amerikan commented 5 years ago

Example preview of generated html:

Screen Shot 2019-05-22 at 1 04 42 AM

Screen Shot 2019-05-22 at 1 48 27 AM