[Libre-soc-bugs] [Bug 418] SPR pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=418

--- Comment #9 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68

On Tue, Jul 14, 2020 at 9:17 PM Samuel Falvo II <sam.falvo at gmail.com> wrote:
>
> On Tue, Jul 14, 2020 at 1:09 PM <bugzilla-daemon at libre-soc.org> wrote:
> >     cookie-cut setup from alu proof_main_stage.py
>
> I'm sorry; I'm trying; I'm just not getting it.  I do not feel
> comfortable just copy-pasta code from one file to another without
> knowing what it does. 

hm.  interesting.  then perhaps first it would be of value for you
to review the existing proofs, which were written by Michael, who
seems to very much know what he's doing, however (as you saw from
what i wrote and raised bug #429) occasionally misses thigns.

> It actively undermines, IMO, the value
> proposition behind formal verification. 

i hear you on that.

> If something goes wrong, and
> I cannot explain it, and even less, be able to reason about it, I
> don't know what value I'm providing the project.

very true.

ok so that makes reviewing the existing formal proofs up to and
*only* up to the verification of the op Record - quite important.


>
> >     #don't worry about it - tests are run manually anyway.  fail is fine.
> >     #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
> >     def test_formal(self):
> >
> > commenting out / disabling unit tests "just because they fail or are
> > otherwise incomplete" is generally bad practice.  the python unittest
> > module is *specifically* designed to catch success/fail exceptions and
> > provide reporting.
>
> This goes against what was written, several different places, on the
> libre-soc wiki insisting that the test suites always pass. 

ah no, definitely not.  if that's the impression then it's definitely
wrong.

> I can't
> remember where I read it now, but I distinctly remember reading that
> features and tests which are known to fail should not interfere with
> the remainder of the code.

yes - and a simple test like this definitely will not interfere with
the remainder of the code.  some of the tests *do* actually interfere.

>  Hence my feature flag; my FV tests are not
> yet complete, and can be misleading to others as I learn more about
> the build.

don't worry about it.  really.

> The intention is, once I'm confident that the tests are of good
> quality, then the feature flag can be removed.

this actively interferes with collaboration.  anyone else attempting
to help with the development and understanding of the test has to
also set that "feature" flag.

as this practice (of setting "feature" flags) has not been established,
discussed, or documented, sticking to "standard python unit test"
practice is the default.

and that means "only damaging unit tests get de-activated or skipped",
and this is not one of them.

-- 
You are receiving this mail because:
You are on the CC list for the bug.