Change the --extractTarget option into a command

[keyboardDrummer]

Touchup PR for #5621

Description

• Change the --extractTarget option into a hidden command
• Make --help work when used on hidden commandds

How has this been tested?

• Manually ran make extract in DafnyCore. This feature needs some tests but I'm leaving that out of scope of this PR.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[atomb]

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

[keyboardDrummer]

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

It's a hidden command, so I think we're free to change the name/options later without having to be backwards compatible.

[atomb]

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

It's a hidden command, so I think we're free to change the name/options later without having to be backwards compatible.

Good point. Given that, I'm happy with this.