FStarUnit - a simple unit tester #2904
briangmilnes
started this conversation in
Show and tell
Replies: 2 comments 2 replies
-
What about KaRaMel? Should I try and make this run tests in C yet? Ever? |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
As I had to write some test code, and learn to run the tests (to check in Printabl) it's very hard to see what is in the test logs. So I wrote the obvious FStarUnit.
Tests look like:
(* FStarUnit is a very basic way of running unit tests, ala xUnits in other
languages.
A test is just a fun : unit -> bool & option string - so you can return a message.
You can run a single test with test.
You can run a list of tests as a suite with tests.
One of the most annoying things about several unit test frameworks that I have
used is that they simply output passed, failed, error, etc. But other code
may also do this, making searching hard. So I have annotated symbols with
FSU:, FSUCOUNT: and FSUTOTAL:.
As these are runtime OCaml tests, there is a Makefile.FStarUnit.
It has three top level targets that you care about: all clean test.
It builds in your test module a single DUNE directory and puts into this
a dune project that knows about all of your files. It also puts into
this a main.ml which is an ML main that calls a main function from
each of your files named Test*.
There is also a working example beneath this TestUnit (?) directory
called TestDirExample for you to work with.
*)
TestJudy.fst:
module TestJudy
open FStarUnit
let main() =
(ps "\n";
tests "Judy Blue Eyes"
[("Crosby", (fun () -> true, Some "It's getting to the point, where I FSU:PASSED the test."));
("Stills", (fun () -> true, None));
("Nash", (fun () -> false, Some "Some thing inside of me is telling me that I have a bug."));
("Young", (fun () -> false, None))])
And you get clean output.
FStarUnit: Test Crosby FSU:PASSED msg David
FStarUnit: Test Stills FSU:PASSED.
FStarUnit: Test Nash FSU:FAILED msg Graham
FStarUnit: Test Young FSU:FAILED.
FStarUnit: Running 4 tests in a suite named Judy Blue Eyes.
FStarUnit: Judy Blue Eyes Test Crosby FSU:PASSED msg It's getting to the point, where I FSU:PASSED the test.
FStarUnit: Judy Blue Eyes Test Stills FSU:PASSED.
FStarUnit: Judy Blue Eyes Test Nash FSU:FAILED msg Some thing inside of me is telling me that I have a bug.
FStarUnit: Judy Blue Eyes Test Young FSU:FAILED.
FStarUnit: Finished running test suite Judy Blue Eyes with FSUCOUNT:PASSED 2 tests and FSUCOUNT:FAILED 2 tests.
FStarUnit: Test suite Judy Blue Eyes FSUTOTAL:FAILED
.
FStarUnit: Running 2 tests in a suite named The Law.
FStarUnit: The Law Test 1 FSU:PASSED msg I fought the law and
FStarUnit: The Law Test 2 FSU:PASSED msg the law won.
FStarUnit: Finished running test suite The Law with FSUCOUNT:PASSED 2 tests and FSUCOUNT:FAILED 0 tests.
FStarUnit: Test suite The Law FSUTOTAL:PASSED
It could be extended with IO based tests pretty easily. It does need some exception
understanding and it might benefit from test_X functions that raise (test_exn "no power")
and so on.
My make files are certainly not quite ready to drop into the FStar/tests directory yet.
Would anyone like to help me by proposing some features and then I'll make it
fit if there is interest.
It might be nice also to see the runs of testing by normalization and their times, but
I'm not sure how to put that in a standard testing tool model as that's compile/verify time.
I can make a fork/branch/pull for this now if anyone would like to give it a try.
If there is a particular piece of the tests that anyone would like converted, I'd give it a shot.
And I'd be happy to update the wiki whose testing pages no longer match the
process.
I've done this so many times, and then gone onto the performance equivalence, it's old hat (1st startup, 1st and 2nd CMU research jobs, Lycos, Amazon, Zillow, ...).
Beta Was this translation helpful? Give feedback.
All reactions