Oops, forgot to send.
>> Calculating graph properties scales very badly because the
>> specifications aren't optimised (naturally). Exhaustive testing with
>> leancheck is a lot more effective here because we avoid testing with
>> (too) large graphs. Unfortunately test-framework is a bit limited in
>> that it doesn't allow to scale the number of tests, just to set them
>> to a fixed value. We opt to set it to 0x8000 which covers all graphs
>> up to size 6.
>
> It'd be helpful to put the comments about why 0x8000 and why leancheck
> in the code.
Will do.
> BTW we might consider switching from test-framework to tasty, I think
> test-framework is in maintenance-only mode nowadays. From what I'm aware
> tasty is its natural successor.
I agree that this would be the right move, but not keen on doing it
myself. If you feel like it, go ahead.
>> * add Darcs.Util.Graph.components with properties and tests
> BTW I had to apply the patches in this order (which is not the order
> they were sent) to avoid build breaks.
Yet another missing explicit dependency. Can we automatically add them
using your new 'darcs test' features perhaps? Something like "try to
build project with all re-orderings of unpublished patches, inserting
dependencies whenever a commute breaks a build?
>> components :: Graph -> [VertexSet]
>
> Given the unsafe indexing inside this, I presume we could get a segfault
> if it is passed an invalid Graph. I'm not sure whether to be concerned
> about that or not. I'd be inclined to play it safe unless you're sure
> this really matters performance-wise. Just replacing the unsafeRead
> should be good enough as it also guards the unsafeWrite.
I agree that using the safe read and write operations should be fast
enough in practice. I am not sure why I didn't use them in the first
place, this is just unwarranted premature optimization. Will fix.
>> * use Darcs.Util.Graph.components for RepoPatchV3
>>
>> This required a few refactors and the introduction of a new data type for
>> components. In particular, the ltmis algorithm needs to be adapted to
>> working with just a subset of the vertices of a graph.
>
> Is this because previously we constructed the graphs after calculating
> the components, so each component had a self-contained graph with
> contiguous numbering?
Yes, exactly. The mapping from the list of Nodes to the Graph and back
is usually a bottleneck and therefore shouldn't be done more than once.
I found it unfortunate that this seemed to reduce compositionality,
which is why I added the Component data type as a new concept.
> I didn't read the code in detail but I'll assume the tests are good enough.
Exhaustive testing with a complete specification really gave me a warm
fuzzy feeling! This was fun to write and it actually worked the first
time I ran it. Though at first I did have a few bugs in the properties
that needed fixing before the tests succeeded :-)
BTW, I didn't want to go overboard with the new leancheck thing, but
there are a few closely related packages with interesting
functionalities, like discovering laws through testing and (to come to
the point) detecting redundancy among laws and IIRC also detecting
whether a set of laws fully specifies a function. Some of that may come
in handy in the future.
|
