In case HPC allow us to use their clusters, I suggest the following.
Each theorem proving task (or a group of theorem proving tasks) will be sent to the cluster, once the job is finished, it will initiate an API call with the job ID which will update the database. This way we can support much heavier and parallel tasks.
On the frontend side, instead of running it synchronously like now and displaying a message. The buttons for all theorem proving tasks (consistency, independence and queries) will have four states:
current buttons: execute and buttons are clickable
Success - a button with a green V? not clickable and denotes success. This can already be read fro the DB since I store the state of the last query if it is successful.
Failure - a button with a blue '-'? not clickable and denotes failure (i.e. not consistent). Can also already be read.
Error - a clickable button with an X? This happens when the theorem prover or something else broke down.
In addition, we should also think what do do about timeouts. On the HPC, a timeout of 30 seconds should be enough to declare a Non-theorem?
In case HPC allow us to use their clusters, I suggest the following.
Each theorem proving task (or a group of theorem proving tasks) will be sent to the cluster, once the job is finished, it will initiate an API call with the job ID which will update the database. This way we can support much heavier and parallel tasks.
On the frontend side, instead of running it synchronously like now and displaying a message. The buttons for all theorem proving tasks (consistency, independence and queries) will have four states:
In addition, we should also think what do do about timeouts. On the HPC, a timeout of 30 seconds should be enough to declare a Non-theorem?