New flag --profile replaces verbosity option -vprofile

[nad]

I noticed that -vprofile:7 overrides -vprofile.definitions:10 and -vprofile.modules:10:

agda/src/full/Agda/TypeChecking/Monad/Benchmark.hs

Lines 60 to 64 in ff82d4a

	return $ case (internal, defs, modules) of
	(True, _, _) -> B.BenchmarkSome isInternalAccount
	(_, True, _) -> B.BenchmarkSome isDefAccount
	(_, _, True) -> B.BenchmarkSome isModuleAccount
	_ -> B.BenchmarkOff

Is this intentional? It is not documented.

[nad]

I guess the reason is that the current implementation cannot handle several of these options at once: if you activate both -vprofile:7 and -vprofile.modules:10 (say), then the output for modules will be incorrect, because only the innermost call to billTo "counts".

I see some ways forward:

• Make the code work.
• Make Agda complain if two or more of these options are activated at the same time. However, that would mean that Agda complains if you use -vprofile:10. An alternative is to use dedicated options for profiling.
• Update the documentation.

Given that I think this bug has low priority I don't want to spend too much time on it. I suggest that we simply update the documentation.

[andreasabel]

The usual semantics if -v is cumulative, so more instances of this flag can only add more output.

[UlfNorell]

The usual semantics if -v is cumulative, so more instances of this flag can should only add more output.

Indeed, the use of -v for profiling is a bit of a hack, and we really should have a separate flag for it. How about

--profile=internal|definitions|modules|...

Aside from those three we also have sharing, serialize, metas, constraints, interactive, iface, and ticks. I believe those aren't using the billing system so they can all coexist without problems.

[nad]

Sounds good to me.