Do not raise an error when reveal mentions an already transparent function, only a warning

MikaelMayer commented 1 year ago

Summary

reveal should not raise an error when the function it refers to is not opaque

Background and Motivation

It's often the case when experimenting with the "opaque" keyword, that users want to reveal it in some places and not others, to compare resource units. However, once a user writes "reveals f();" they can't get back to removing the opaque keyword as it would raise an error on this "reveal". This makes it painful to experiment with the opaque keyword. Semantically, reveals f(); if f is a transparent function at best should simply be resolved as a no-op, and at worst emit a warning.

Proposed Feature

reveal f(); should never throw an error.

As an example:

function NonOpaque(): int { 1}
method TestNonOpaque() {
  reveal NonOpaque();
  assert NonOpaque() == 1;
}

should at worst only emit a warning like "function NonOpaque is already transparent and does not need to be revealed", not an error.

Alternatives

Not having this features impacts my work when I want to experiment with the opaque keyword., at least once a month (and today was that day)
There is now the option --defaultFunctionOpacity:autoReveal that inserts reveal lemmas for every function, so it's not a problem using this option; However, I want to make the fix for reveal work also when all functions are transparent
Should we do the same for assertion labels? I think yes, we should also only emit a warning if a label cannot be resolved, because someone might be experimenting with hiding assertions or requirements.

kjx commented 8 months ago

for what it's worth - I've regularly hit this problem too.

Hmm, seems it's "--default-function-opacity" (after trying to find it in the help)

perhaps I'll play with autoReveal, although it's not clear how autoReveal actually differs from standard behaviour (or is that the plan, to make it standard?). does AutoReveal behave differently depending on if functions are opaque or not?

MikaelMayer commented 8 months ago

For documentation about how to use autoreveal, see this section of the doc. https://dafny.org/latest/DafnyRef/DafnyRef#sec-autorevealdependencies

If you haven't find it, I'd be interested where you looked for it, perhaps we could include a link.

kjx commented 3 weeks ago

haven't played with it yet - still trying to get actual work done :-)

I still think warnings for revealing non-opaque names is a good idea, at least as an option.

but I see there is now a new "hide" statement? does that mean "opaque" is now deprecated? or what? sigh

IF I chop things up into modules, can I get the effect of "opaque"

notably abstractions over facts about programs - in another way?

dafny-lang / dafny