search

abella-prover / abella

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

Bring part of the test suite up to date #58

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

As pointed out in #57, the Abella test suite is needing some attention. A few simple changes allow five out of ten test modules to compile. From a conversation with @chaudhuri it seems that the changes made to the parser are indeed correct.

A new target for make creates a tester executable that runs all the (current) tests in the battery. Although a simplified scenario, I am finding it helpful.

chaudhuri commented 8 years ago

Rebased onto master and pushed (b9bacfc2). Thanks.