output of theorems should be lazy, but is not, because of alignment

[jwaldmann]

For larger values of maxSize, I have to wait a looong time to see anything, in the output of speculate.

I was hoping that theorems are printed as they are discovered. But I think they are all held until the end - for computing the alignment. (report calls prettyEquations calls table which wants to see all words)

A work-around (I guess) is to call finalEquations directly, but then I have to copy code out of report.

Assuming the above is true (the lazy list of theorems is available), perhaps Args can get an attribute that says whether to print them at once (but un-aligned), or in the end (and aligned).

[rudymatela]

For larger values of maxSize, I have to wait a looong time to see anything, in the output of speculate.

The quick workaround I tended to use was to actually call Speculate multiple times, each time increasing the maxSize. You could use:

./yourprogram-s4 && ./yourprogram -s5 && ./yourprogram -s6 && ./yourprogram -s7

In some cases the runtime magnitude increases by one with each two increments of size, so the earlier runs wouldn't matter to much in the overall runtime. (This a similar process to how the seminal SmallCheck ends up retesting values of ealier series.)

I was hoping that theorems are printed as they are discovered. But I think they are all held until the end - for computing the alignment. (report calls prettyEquations calls table which wants to see all words)

If I recall correctly, the output is not lazy just because of equation alignment, but actually it is so because Speculate may use later equations to discard redundant earlier ones. It's been a while, so I could be wrong (-:

Assuming I'm not, in theory, Speculate could have an option where we only discard later (bigger) equations based on earlier (smaller) ones, so output would appear while Speculate tests and thinks. For that to happen, the reasoning engine has to become lazy. This would be non-trivial to implement as my reasoning engine is a currently sort of a can of worms.

(some handwavy technical details below)

Now about "Speculate may use later equations to discard redundant earlier ones":

One of the reasons why earlier equations may be discarded is that by default, on the term-rewriting-based reasoning module, Speculate uses a variation of Dershowitz order which is more "lexicographicky" rather than using Knuth-Bendix order, which is more based on term size.

(A technical detail of a technical detail now.) Though Speculate is not strictly lexicographic. Leaf terms are actually compared quasi-lexicographically based on the position they appear in the constants list and their arity -- so the order in constants may influence which equations are discarded or how they are displayed. This was chosen sort of in an ad-hoc manner, to replace weird equations in examples.

Warning: the two above paragraphs are handwavy - I'm not being strict on the terms I use.

[jwaldmann]

Thanks for explanation. Well, then just keep this issue open, as documentation for current behaviour, and reminder for possible enhancement.