search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 233 forks source link

Output diffs for unit tests #10

Closed catalin-hritcu closed 9 years ago

catalin-hritcu commented 10 years ago

We discussed that we want to check for any output changes in the unit tests, and report any inconsistencies with respect to previously saved and audited logs.

catalin-hritcu commented 10 years ago

Pierre-Yves proposed to use the Xunit format to integrate the reports produced this way with Jenkins. Here are some links about this: http://www.mitls.org/jenkins/ https://www.easycrypt.info/jenkins/job/easycrypt--test-suite/ws/xunit.xml http://nose.readthedocs.org/en/latest/plugins/xunit.html https://www.easycrypt.info/trac/browser/scripts/testing/runtest https://www.easycrypt.info/jenkins/job/easycrypt--test-suite/

catalin-hritcu commented 10 years ago

Was wondering, is there any reason to produce output diffs for fully successful tests? My impression was that we're comparing outputs only to make sure that the error messages are still the same, but if there are no errors there is nothing to compare. In any case, I'll try to solve #9 first.

strub commented 10 years ago

If they are successful, the diff should be empty, no?

catalin-hritcu commented 10 years ago

As far as I can see F* outputs stuff even when it successfully type-checks a file. Do we want to diff that stuff at all?

catalin-hritcu commented 10 years ago

[5:42:33 PM] Pierre-Yves Strub: Still, the diff should be empty [5:42:43 PM] Catalin Hritcu: not if the output changes [5:42:54 PM] Catalin Hritcu: but the whole thing still succeeds [5:43:02 PM] Pierre-Yves Strub: Ah yes, for successful test, do we check the diff [5:43:03 PM] Pierre-Yves Strub: I don't know [5:43:06 PM] Pierre-Yves Strub: I would say no [5:43:16 PM] Catalin Hritcu: ok :) [5:43:37 PM] Catalin Hritcu: this would be a big incentive to separate failing from succeeding things [5:43:50 PM] Catalin Hritcu: since for failing things one has to deal with the diffs, and that's a pain [5:44:13 PM] Catalin Hritcu: I mean, separating things out in different files [5:44:19 PM] Pierre-Yves Strub: Yup

nikswamy commented 10 years ago

On a successful run, unless we pass --silent (I guess), it should say "Verified module XXX" for each verified module. It's worth checking that it verified all the modules we think it should have verified, no? So, why not diff the successful runs also?

catalin-hritcu commented 10 years ago

What kind of bugs would this prevent? Magically disappearing modules? Generally I'm very much worried by the overhead all this will add, so I would like to contain that as much as possible.

nikswamy commented 10 years ago

You're worried about the overhead of diff'ing the output of a build against a known good run? Really?

Sent from my Windows Phone

From: Catalin Hritcumailto:notifications@github.com Sent: ‎10/‎22/‎2014 11:31 To: FStarLang/FStarmailto:FStar@noreply.github.com Cc: nikswamymailto:nswamy@live.com Subject: Re: [FStar] Output diffs for unit tests (#10)

What kind of bugs would this prevent? Magically disappearing modules? Generally I'm very much worried by the overhead all this will add, so I would like to contain that as much as possible.

Reply to this email directly or view it on GitHub: https://github.com/FStarLang/FStar/issues/10#issuecomment-60132320

catalin-hritcu commented 10 years ago

The development overhead of changing the type-checker in trivial ways and breaking the output checks, and then having to go through a ton of diffs to make sure they are all OK.

catalin-hritcu commented 9 years ago

Closing with wontfix. A more targeted variant of this filed as #231.