Lean server `-D` settings

Stream: lean4

[Mac]

Does the Lean server not forward -D option settings onto its file workers? Is this a bug? To test, try passing something like -Dtrace.compiler.ir.result=true to the server and you will not see any compiler results.

[Mac]

From the code for the -D option in lean.cpp, it appears that they are not in fact forwarded to the workers (as they are not appended to the forwarded_args array). I imagine it would need a line like the following to do so:

forwarded_args.push_back(string_ref("-D" + std::string(optarg)));

[Wojciech Nawrocki]

Yep, only some options are forwarded and -D is not. It would probably be reasonable to forward it as well.