feat: Add an :options attribute on modules

[cpitclaudel]

This is a draft to start a discussion on how we want to specify per-file options in Dafny.

The problem

Different files within a single Dafny project may need different settings:

• Warnings
• Syntax, when transitioning from one version of Dafny to the next (/functionSyntax, /allowGlobals)
• Handling of arithmetic (/NLArith, /arith)
• Tracking of print effects (/trackPrintEffects)
• etc.

We have discussed introducing a DafnyProject file, but this is not sufficient, because individual files or even individual modules may need custom settings.

Proposal

Introduce syntax within Dafny file to set options temporarily. This PR does this by adding an :options attribute that supports a subset of Dafny's command line options. For now, I've added the general infrastructure + support for /functionSyntax (which would allow us to migrate the libraries to the new function syntax (ghost function) without breaking customers, since they could compile their code using the old syntax while using libraries with the new syntax).

(Of course, in the case of functionSyntax, it would be relatively easy to build an automated porting tool)

The code needs small changes in Boogie (https://github.com/boogie-org/boogie/tree/cpitclaudel_cli-error-reporter), so this branch won't compile as is.

[RustanLeino]

I like this functionality! As you had described to me off-line, this proposal does:

When we find an :options (in the parser) we 0. save the current options; 1. Update the current options by parsing the arguments of the attribute; and 2. continue parsing [and 3. restore the saved options]

Since this lets us support options that affect syntax (like /functionSyntax), this will do great for now. Maybe one could also do this for the verifier. That is, when starting to verify a module:

0. as above; 1. as above; 2. translate the module into Boogie and perform the verification; 3. restore the saved options.

[RustanLeino]

Bravo!

[robin-aws]

Just adding my support for this feature as well - I had thought you were proposing some additional file-level #pragma-like syntax for this functionality, but having an attribute at the module level is much cleaner and fits perfectly into the Dafny language design!

Any chance {:cliOptions ...} would be a better name?

[MikaelMayer]

Any chance {:cliOptions ...} would be a better name?

This would also useful from within the IDE, so the more generic the attribute name, the better I would think.

[cpitclaudel]

@MikaelMayer

This would also useful from within the IDE

Yes, but the options themselves are CLI options (the arguments to that attribute are passed directly into the command line parser). So maybe cliOptions is in fact a good name?

Although I don't like the lowercase cli :P

[keyboardDrummer]

This is great :-)

Also an extra reason to remove references to DafnyOptions.O ! Will it make sense to do that first to ensure we don't refer to the wrong options somewhere by accident?

Yes, but the options themselves are CLI options

Doesn't this PR change that?

After this PR they are both CLI and module options. In the future they'll also be in the project file. I don't see what makes them more tied to the CLI than to the project or to a module.

[MikaelMayer]

Doesn't this PR change that? XD

@keyboardDrummer you got a point here ! But perhaps @cpitclaudel was concerned about the syntax, because this option attribute uses a syntax that is command-line.
However, the same options can be applied programmatically without launching Dafny on the command-line, but by any API that can launch a process.
Hence, I'm also in favor of just renamining this "options", unless we had two kinds of options.

[cpitclaudel]

We it make sense to do that first to ensure we don't refer to the wrong options somewhere by accident?

I don't think we need to do that urgently, because the only option this accepts for now applies to parsing (/functionSyntax)

[cpitclaudel]

Also an extra reason to remove references to DafnyOptions.O ! Will it make sense to do that first to ensure we don't refer to the wrong options somewhere by accident?

Done in Parser.cs

[cpitclaudel]

I don't have a strong opinion on the name of the attribute; but re:

I don't see what makes them more tied to the CLI than to the project or to a module.

I would say the syntax does: the choice here was to not invent a new syntax for options, so I used exactly the parser's options. In the future we might decide that it's cleaner to have a non-cli option syntax. But in that case we can give it a different name, like :config. So I'd say we're fine; let's see if the tests pass now that we've updated to the latest boogie.