Development Notes

Here's a list of cautionary tales from the project's original devs to those who wish to extend the features:

Compiler

• To interact with SAT solvers, an input file for them must first be generated. In most cases this comes in the DIMACS CNF format. Since we could find no algorithm for CNF conversion, we wrote one from scratch in za.org.cair.logic_app.generator.CNFConverter. This was an immense pain and we strongly encourage you make use of this class for further interactions with SAT solvers or HOL reasoners.

Webserver

• The editor's validation functionality comes from JS pings to a specific webserver endpoint. That endpoint is not in our main code, but rather gets generated from the xtext lib during build time. Thus there is no easy way to change the way validation happens (though the way it works is totally fine) but more importantly no easy way to create a compilation endpoint that utilises that compiler instance. As we discovered creating more than one generator instances in the same program causes cryptic OutOfBounds errors referencing files outside our codebase. From what we gathered from research, the way people implement this is by running the code generator as its own program and calling on it externally with Runtime.exec().
• We can't use Heroku for deployment. They only support Java 1.8 (this project uses 11). Also, setup for a complicated project like this is even more complicated on Heroku.