search

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

Notify/warn the user when a `skip` is used in a .thm file? #137

Closed innofarah closed 2 years ago

innofarah commented 2 years ago

In the situation where a user wants to recheck a .thm file, the user would not know that some theorems were not really proved (if skip were used) if he doesn't read it explicitly in the file (in the .thm or in the output file). Wouldn't that be a problem in case of rechecking a large set of files where the user will not, in practice, read through every proof script?

ThatDaleMiller commented 2 years ago

I think it is good to provide a printed warning that a skip appears in the proof of a theorem when checking a theorem file. I believe this would only need to appear when someone runs the Abella command at the command line with a .thm file as its argument.