Allow /prune:0 to disable pruning

[atomb]

Add a /noprune flag to turn off pruning. It's off by default, but this can be convenient if a) it's turned on earlier on the command line, or b) Boogie is being used from another system like Dafny.

I would have made it /prune:{1,0}, but it's harder to make that backward compatible with the current behavior.

[keyboardDrummer]

a) it's turned on earlier on the command line

Applying that pattern to all options would introduce a lot of duplication. Why not remove the earlier invocation?

b) Boogie is being used from another system like Dafny.

Can you elaborate? Boogie is invoked as a library by Dafny

[shazqadeer]

The goal is indeed confusing. It seems odd to have both /prune and /noprune.

[atomb]

b) Boogie is being used from another system like Dafny.

Can you elaborate? Boogie is invoked as a library by Dafny

The main use case I have in mind is being able to pass /noprune to Dafny (which otherwise enables pruning by default) for experimentation and debugging. It's not something I want to generally expose as a Dafny option, though, so I'd prefer to have it as a Boogie flag that you can pass through from Dafny if you happen to know you really want it.

I think /prune:{0,1} is a nicer option (like we have for /normalizeDeclarationOrder, etc.), but there are a lot of scripts out there that call Boogie with /prune that would break and need to change to /prune:1.

[atomb]

I think I may be overestimating the likelihood of backward compatibility issues, having taken a look around at scripts that exist. So I'm now inclined to make this /prune:{0,1} if you're both on board with that.

[keyboardDrummer]

The main use case I have in mind is being able to pass /noprune to Dafny (which otherwise enables pruning by default) for experimentation and debugging

Why would you need a Boogie change for that? Seems like that would be a Dafny change

It's not something I want to generally expose as a Dafny option, though, so I'd prefer to have it as a Boogie flag that you can pass through from Dafny if you happen to know you really want it.

Does hiding the option, as Dafny does with the other Dafny-language-developer options, not work?

[keyboardDrummer]

I still don't understand the use-case, but this seems fine to me.

[atomb]

It's not something I want to generally expose as a Dafny option, though, so I'd prefer to have it as a Boogie flag that you can pass through from Dafny if you happen to know you really want it.

Does hiding the option, as Dafny does with the other Dafny-language-developer options, not work?

That would also work, but this is more general. It ensures that, at the Boogie level, you can always choose specifically whether you want pruning or not, whatever the default is (or however it happened to be set earlier in whatever pipeline you're using). I think it's similar to the reasoning for /normalizeNames and so on.

[keyboardDrummer]

That would also work, but this is more general. It ensures that, at the Boogie level

Do you mean when you invoke the Boogie CLI?

, you can always choose specifically whether you want pruning or not, whatever the default is (or however it happened to be set earlier in whatever pipeline you're using).

You could already do that by adding or removing /prune to your CLI invocation, right?

[atomb]

That would also work, but this is more general. It ensures that, at the Boogie level

Do you mean when you invoke the Boogie CLI?

Or anything that passes on CLI arguments to Boogie, like Dafny.

, you can always choose specifically whether you want pruning or not, whatever the default is (or however it happened to be set earlier in whatever pipeline you're using).

You could already do that by adding or removing /prune to your CLI invocation, right?

In principle, yes. But a frequent case I encounter is the use of scripts that pass one set of arguments to Boogie and then allow additional arguments to the script to add to the built-in set. When doing that, it's often useful to add an argument that reverses a previous argument. Because of this, I generally like all tools to have the ability to set boolean flags explicitly to true or false, rather than just a flag that toggles away from the default.

The way Dafny uses Boogie as a library also works essentially like that script setup.

[keyboardDrummer]

But a frequent case I encounter is the use of scripts that pass one set of arguments to Boogie and then allow additional arguments to the script to add to the built-in set. When doing that, it's often useful to add an argument that reverses a previous argument. Because of this, I generally like all tools to have the ability to set boolean flags explicitly to true or false, rather than just a flag that toggles away from the default.

The way Dafny uses Boogie as a library also works essentially like that script setup.

I see. Even though Dafny invokes Boogie as a library, it still allows passing CLI arguments to Boogie, and those can override options that were set programatically.