use configargparse to process halmos.toml

[karmacoma-eth]

No description provided.

[daejunpark]

could you explain in which order options are applied? we now have four sources of options:

1. default option values
2. config file
3. halmos custom natspec
4. command line

i think the above order makes sense. wdyt?

[daejunpark]

what's the semantics of sections? can we have multiple sections in a toml file, and choose which section to use when running halmos? do sections inherit from their parents? if so, what's the naming convention for section inheritance?

[daejunpark]

perhaps for the next pr: instead of having an example file here, it would be better to provide a running toml file in the test directories, under the examples/ and tests/, where foundry.toml exists.

[karmacoma-eth]

yes!

[karmacoma-eth]

could you explain in which order options are applied? we now have four sources of options:

1. default option values

2. config file

3. halmos custom natspec

4. command line

i think the above order makes sense. wdyt?

almost but IMO it should be:

1. defaults
2. config
3. command line
4. natspec

natspec feels more specific to a contract/function than the command line, which applies to the whole repo

[karmacoma-eth]

what's the semantics of sections? can we have multiple sections in a toml file, and choose which section to use when running halmos? do sections inherit from their parents? if so, what's the naming convention for section inheritance?

left for future work, currently there is a single supported [global] section

but going forward I think it would be nice to support profiles, so you could have [ci] and [ci-long] sections for instance, and then you can enable them via an env var

[daejunpark]

almost but IMO it should be:

1. defaults
2. config
3. command line
4. natspec

natspec feels more specific to a contract/function than the command line, which applies to the whole repo

makes sense. that's also the existing behavior before this pr, right?

actually i was wondering what if users want to quickly override the natspec options using command line, but that might not worth supporting.

[daejunpark]

tests seem to become flaky. ci failed due to z3 model not found, and that also happened intermittently in my local:

z3.z3types.Z3Exception: model is not available

[karmacoma-eth]

I'm not happy with the hackiness and the flakiness, I'll close this one and put up something cleaner