@gasche? @dra27?

For the sake of our poor CI and so that it becomes green again.

(You know how pathologically attached I am to colors, don't you? ;-) )

Thinking more about this PR, I realize that I don't understand the implications of inheriting these flags. For example, .depend contains

stdlib__array.cmo : \
    stdlib__seq.cmi \
    stdlib__array.cmi

Do I understand correctly that any Makefile-side flag set for stdlib__array.cmo will also apply to stdlib__array.cmi (as the documentation says) but also to stdlib__seq.cmi? This would mean that to correctly set the values to null when we don't want cmis to be impacted, we have to list not just the cmi files, but also all the interface-level dependencies of the module, which change over time.

I am now under the impression that #8601 is not the right way to go: it makes the system harder to understand and more fragile. With my current understanding (I would be happy to be reassured about the impact of inheritance), I would propose to revert #8601 rather than merge this followup PR.

For warnings you can use [@@@ocaml.warning "..."] attributes to specify warnings at the top of a source file.

In the past I proposed to allow toplevel directives at the beginning (only) of each source file, so that

#labels false;;
#alias-deps false;;

could be used to specify compilation options. This proposal has not had the enthusiastic following that I expected.

(I think it's important to have something that is only syntactically valid at the head of a source file, rather than anywhere in the file like extensions and attributes, to enforce the semantics that this header is interpreted by the compiler before the whole file, which is the only semantics that makes sense for global flags that affect the semantics of all the code in the module (for example -safe-string, -for-pack foo, -no-alias-deps), in opposition to settings that can be meaningfully changed from one sentence to the other (actually not many flags are properly supported in this mode).

@shindere let's go ahead reverting #8601; I'll let you do it, if that works with you. (I think you can push directly without an additional pull request, but you could write a comment in the PR to summarize the final decision.)