runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
508 stars 143 forks source link

Introduce verbosity levels for `foundry-kompile` #1950

Open palinatolmach opened 1 year ago

palinatolmach commented 1 year ago

Related: https://github.com/runtimeverification/pyk/issues/521

Currently, the --verbose option in kevm foundry-kompile is not showing the detailed output for the kompile command that is invoked within foundry-kompile. Now that the --verbose flag is available in kompile (https://github.com/runtimeverification/pyk/pull/523), we might introduce different verbosity levels for foundry-kompile.

E.g., -v might include only foundry-kompile logs, -vv — logs produced by both foundry-kompile and kompile, etc.

ehildenb commented 1 year ago

We have generally been using --verbose and --debug instead of -v and -vv. But are you suggesting that we need a level of verbosity between --verbose and --debug? Indeed, --debug is very verbose, often too verbose for anything practical.

palinatolmach commented 1 year ago

Thanks, I didn't realize we have the --debug option! I agree, we can include showing verbose kompile logs into --debug. In general, the purpose of providing this additional verbosity level is to include the kompile logs which (as we found out recently) are necessary to investigate foundry-kompile executions that take too long; in this context, I would still be in favor of having an option that includes this info and not the rest of the logs printed out by --debug, as you also suggested. Besides, as highlighted by @radumereuta (who came up with this idea), -v/-vv options are also used to control verbosity in ercx, and Foundry uses them too:

          Verbosity of the EVM.

          Pass multiple times to increase the verbosity (e.g. -v, -vv, -vvv).

          Verbosity levels:
          - 2: Print logs for all tests
          - 3: Print execution traces for failing tests
          - 4: Print execution traces for all tests, and setup traces for failing tests
          - 5: Print execution and setup traces for all tests