Optimization flags should not be package specific

[xubaiw]

lake/Lake/Package.lean

Lines 179 to 184 in 111a47f

	/--
	Additional arguments to pass to `leanc`
	while compiling the C source files generated by `lean`.
	Defaults to `-O3` and `-DNDEBUG`.
	-/
	leancArgs : Array String := #["-O3", "-DNDEBUG"]

Lake is currently specifying default optimization flags to -O3 -DNDEBUG, which would cause a problem when there is package dependencies, since a package cannot override the leancArgs of the package it depends on. Optimization level should be a global choice and users can simply change it using command line args.

[tydeu]

@xubaiw @Kha I am a bit confused as to the logic here. Why would you want to modify the the compilation of dependent packages (without its permission)? If a dependent package states that it is to be compiled with -O3, -DNDEBUG (or any other flags) I think it would be very concerning for the parent package to override that. Furthermore, just because one wants to build the package they are developing with a low optimization level and debug symbols that doesn't mean they want to build all dependencies that way as well.

However, if a dependent package wants to make the optimization level of a package modifiable by end users, it could so with something like:

package A (dir) (args) {
  leancArgs := if args.isEmpty then #["-O3", "-DNDEBUG"] else args.toArray
  ...
}

package B {
  dependencies := #{{name := `A, args := #["-O1"], ...}]
  ...
}

[xubaiw]

So debug info of the dependencies is unnecessary? Maybe I have mistaken it, I see cargo just rebuilds all dependencies when I switch from cargo build --release to cargo build. Are we assuming there's no bug in dependent packages?

Besides, something like profile in cargo and build type in cmake is a higher level concept than compiler flags. Although it's unrealistic and unnecessary to modify the flags of dependent packages, some standard profiles (which can be configured by the dependent package) like Debug, Release, MinSizeRelease can be helpful. Should we have something alike, or is this considered a bad practice for Lean?

[Kha]

Yes, offering a choice of build profiles independent from the specific package configuration is standard practice in any package manager for a compiled language. Whether dependencies should be built in debug mode as well (and whether debug or release should be the default) seems to be a contentious topic, but "make as much of the program debuggable as possible in debug mode" looks like a fine default to me. Bad enough that most languages only ship a precompiled, optimized stdlib... :) .

[tydeu]

@xubaiw @Kha I don't disagree that build profiles are good. But as you mentioned @Kha, enforcing them on dependencies is questionable. More important, this is the leanc build we are talking about -- i.e., the compilation of the resulting .c files produced by Lean. So, unless Lean itself has bug (or you are debugging an external FFI), there should not be a need to debug these programs. Thus, when/if Lake supports build profiles I would expect them to apply to compiling the Lean code itself, not its intermediary results.

[xubaiw]

Yes, it's too early to talk about debugging in Lean. You can close this issue if Kha has no further questions.

[Kha]

Debug symbols is not the primary reason cargo defaults to the debug profile, it's speed. Something like 75% of compilation time for Lean is spent inside LLVM, so this is just as true for us.

Thus, when/if Lake supports build profiles I would expect them to apply to compiling the Lean code itself, not its intermediary results.

All parts of the pipeline will likely need to adhere to the build profile. If Lean ever outputs sensible DWARF metadata, LLVM optimizations should be disabled to make the most out of them.

[Kha]

I think for now the most important part is to ensure that introducing build profiles is backward compatible. Users shouldn't need to change their package configuration for this, nor should they hard-code -O3 -NDEBUG when changing leancArgs. The latter could be done by always prefixing these flags for now, which can be negated by the user using -O0 -UDEBUG.