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

Various problems with the test suite #57

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

There is (as far as I can tell) no easy way to build and run the test suite. I am experimenting with minimal changes to get this working in a branch of my local fork (https://github.com/robblanco/abella/tree/tests).

Notably, many tests seem to have run out of sync with the module APIs they test and fail to compile. Among those that work I have noticed some regressions. I think getting all these back up and running is important. What do you think?

chaudhuri commented 8 years ago

I looked into it around the 2.0.x change but it was a lot of work to port the tests over. Do you have a specific reason for wanting these tests?

robblanco commented 8 years ago

Part of me wants them out of principle, because they make Abella better (and the sooner, the less painful). Another part is that I write tests to go with my experiments and it makes no sense to roll my own when there is a test infrastructure in place, waiting to be used.

I have opened a pull request #58 with my tentative changes. As it stands, execution reveals two regressions. I can open issues for these as needed.

chaudhuri commented 8 years ago

Interesting. Yes, please open issues for the regressions. I'll review your PR now.

chaudhuri commented 8 years ago

Thanks. For reference, Rob just created #59 and #60.

chaudhuri commented 8 years ago

All existing tests now pass. Some obsolete tactics tests had to be commented out.

Note that the test suite has basically negligible coverage.