Allow disable-non-linear-arithmetic per module #4773
Conversation
More current attributes use snake case than camel case, so this is slightly more consistent.
Boogie now re-sets options for each query (so that they can differ for each query). This doesn't change wich options are set, however.
…ly, and add tests for this
| @@ -0,0 +1,104 @@ | |||
| // RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1000 > "%t" | |||
There was a problem hiding this comment.
I would put two RUN here, one with --disable-non-linear-arithmetic and one without. That way, we can verify that the output of Power1 no longer depends on this flag.
docs/DafnyRef/UserGuide.md
Outdated
| @@ -2274,6 +2274,10 @@ and what information it produces about the verification process. | |||
| operators. (This option will perhaps be replaced by `-arith` in the | |||
| future. For now, it takes precedence over `-arith`.) | |||
|
|
|||
| The behavior of `disable-nonlinear-arithmetic` can be turned on and off on a per-module basis | |||
| by placing the attribute `{:disable-nonlinear-arithmetic}` after the module keyword. | |||
There was a problem hiding this comment.
| by placing the attribute `{:disable-nonlinear-arithmetic}` after the module keyword. | |
| by placing the attribute [`{:disable-nonlinear-arithmetic}`](#sec-disable-nonlinear-arithmetic) after the module keyword. |
- please add an entry into the file Attributes.md
There was a problem hiding this comment.
Added it, although I do not think it makes sense to group documentation based on something being an attribute not. When I'm dealing with a particular topic, I would like to be told what language features, including attributes, I can use regarding that topic. When will I ever think, "I'd like to use attributes", and then go look for documentation specific to them?
There was a problem hiding this comment.
I understand that when one is presented with a concept, they will want to know all the language features that allow them to use that concept. I totally agree with that, I want this too. This is the explanation part of the documentation.
To give sense to group documentation based on something being an attribute or not, let's consider the following:
We all work and read in different ways, and this is a reason why we add links to the documentation to group concepts in different ways. Connectivity enables discoverability.
With your edit, if I browse the able of contents, I will now see this:
Users looking for attributes that could reduce the brittleness of proofs might not think about non-linearity, but might be looking for "reveal" and find {:autoRevealDependencies} or {:fuel}., and see that there is something about nonlinear arithmetic a few attributes above that catches their attention
Or users thinking that hey I have so many lemmas that are hard to prove, could want to use extern to prove them and import their proofs. They look for {:extern} and see the {:disable_nonlinear_arithmetic} attribute just before that catches their attention and actually could just be something they were needing.
I hope it helps!
There was a problem hiding this comment.
Users looking for attributes that could reduce the brittleness of proofs
Why would a user want to use attributes specifically? If they run into issues with brittleness, wouldn't they look for a section that's about just that? Like the "Debugging brittle verification" one. And then I would hope everything they need to know, whether it concerns attributes or not, is in there.
For me grouping by attributes is like grouping by all types of syntax that start with (. It's a grouping based on appearance instead of meaning, which doesn't seem useful to me.
I think the reason someone might have started a section with just attributes was because it allows you to add something to the documentation without having to think about where to place it: this section may contain anything as long as it is an attribute. I think it would be better for our users if we remove that section entirely, both so that developers do not get the option to only add something to that list but nowhere else in the manual, and so that users don't have to unnecessarily follow links in the manual. I'll put an item on my TODO list for that.
There was a problem hiding this comment.
Why would a user want to use attributes specifically?
They might be reading a code base and looking for the meaning of some attributes they find. In the future, we could provide documentation over attributes based on this section to explain what these attributes mean. In another future, when we will migrate attribute to proper typed Dafny datatypes, these paragraphs could serve as docstring.
I think it would be better for our users if we remove that section entirely, both so that developers do not get the option to only add something to that list but nowhere else in the manual, and so that users don't have to unnecessarily follow links in the manual.
What you are writing makes no sense to me. As a Dafny developer, I want to get the option to add something to that list before I find a suitable place to integrate it in the manual (e.g. later as part of a guide about how to reduce brittleness). Second, following links is the standard in the web documentation so I see no reason why to remove connected components.
There was a problem hiding this comment.
I think the sweet spot would be having a section that lists all the attributes for various declarations, but only as an index into sections that talk about the actual relevant features.
Definitely another +1 on #3149 providing an even better solution in the future though - I'd still much rather Go to Definition on an attribute reference in code to learn about it than to have to go to the reference manual at all!
|
Need another Boogie update: boogie-org/boogie#811 |
Description
Allow
{:disable_nonlinear_arithmetic}on any module, with the same effect as--disable-nonlinear-arithmeticbut scoped only to the definitions in that module.How has this been tested?
Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfyBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.