Stateful comments, and clock, freeze commands

[gok99]

Difftests run with the watcher, are run until the file reach a fixpoint, which is expected to happen after 2 runs (the first run updates the file, which triggers a re-run which doesn't change the file). However, if a program has non-deterministic output, a fixpoint is almost never reached and difftests are continuously run as the watcher continuously triggers a run.

To avoid this, output that is expected to be non-determistic can be written with a stateful comment (starting with //+), which is passed as input to subsequent runs. This allows commands to force idempotence subject to conditions, based on the previous run's output. For example, with a command like :clock test or :freeze test, stateful comments starting with runtime clock time (test) or freeze (test) are re-output without change.

Some issues:

• While a command like freeze freezes output, the term is still executed, since subsequent blocks in the difftest may depend on it. This could lead to confusing behaviour in which the frozen output doesn't change, but the behaviour of subsequent code does.
• Re-timing a set of blocks with clock is very annoying, since all the identifiers need to be changed. Might be helped by introducing dependencies in which a block is re-run if one of it's dependencies is changed.

[gok99]

Is this the right thing to time?

[LPTK]

Can we just do the timing in node.js? Add a module with a time function that prints the elabsed time:

time of () =>
  foo(123)
> 456ms
= 42

[gok99]

that would probably make more sense, and this could be frozen. at the moment, I'm not sure if stateful comments are particularly useful for anything other than freeze

[LPTK]

Yeah, I would suggest only using freeze instead.

[LPTK]

Thanks for the proposal!

As discussed in the meeting, the ideal feature would freeze the rest of the file atfer the :freeze call (just like :exit), inserting a separator, and refreeze when the separator is deleted:

let config = 123
//│ config = 123

:freeze
====================================================================================================

print(config)
//│ > 123

Furthermore, the non-printed output would still be checked, and the difftest would fail if there is a change there.

This does mean that in the example above, changing config will not be reflected in printed output of the frozen print call. It would probably be advisable to just put everything after the freeze line to reduce such possible inconsistencies.

[LPTK]

By the way, this

Difftests are run until the comments reach a fixpoint, which is expected to happen after 2 runs. However, if a program has non-deterministic output, a fixpoint is almost never reached and difftests are continuously run.

is not quite true.

Difftests are run only once (by the corresponding test command). But if you run individual tests through the watcher, it's just that the watcher keeps detecting a change and re-running the file. The emergent fixed point behavior is an artifact of the watcher :^)

[gok99]

The emergent fixed point behavior is an artifact of the watcher :^)

Ah good point, have clarified.