powdr-labs / powdr

A modular stack for zkVMs, with a focus on productivity, security and performance.
Apache License 2.0
392 stars 80 forks source link

Witness generation: Make CSV export work even if the solver fails #1407

Open georgwiese opened 4 months ago

georgwiese commented 4 months ago

When the solver fails (e.g. due to missing constraints, missing hints, or contradictions in the constraints), it can be pretty daunting to figure out why. Often, this involves inspecting the trace log.

I think one thing that could help would be to just "dump" the current state. We already have the CSV export, so we could use it to dump a partial witness in the case of failure.

This won't be simple, because for example a machine that doesn't complete (which can happen also during a successful run) discards the partial block, so we'd have to keep it around in case we need to dump the current state.

qwang98 commented 4 months ago

Oh that's why my --export-csv didn't export when debugging ;)