Dafny has --filter-symbol for "verify only this symbol", but nothing for "exclude this symbol from verification". That functionality would be very useful to ignore a member that is known to be slow/brittle while verifying everything else. Particularly useful for e.g. verifying a whole git history where we know that a few symbols were bad behaved along history and drag up the verification time even if they never changed.
This might be better to implement inside of Dafny than outside.
(Outside, it'd have to be done by patching the source with {:verify off} which sounds fragile, or by including everything but the unwanted symbol; but inclusion is by substring, so carving the exception might not be doable)
Dafny has
--filter-symbolfor "verify only this symbol", but nothing for "exclude this symbol from verification". That functionality would be very useful to ignore a member that is known to be slow/brittle while verifying everything else. Particularly useful for e.g. verifying a whole git history where we know that a few symbols were bad behaved along history and drag up the verification time even if they never changed.This might be better to implement inside of Dafny than outside.
(Outside, it'd have to be done by patching the source with
{:verify off}which sounds fragile, or by including everything but the unwanted symbol; but inclusion is by substring, so carving the exception might not be doable)