Apply `--safe` and `--without-k` on a library level

[MatthewDaggitt]

Now that Agda 2.6.2 has been released, we don't need the OPTIONS pragmas everywhere, we can instead specify the default options in the standard-library.agda file. This should zap several hundred lines of code in the process 🎉 (not to mention avoid many wasted hours of tests failing when I forget to add them to new modules)

[gallais]

Surely local flags cannot invalidate the ones set globally?

[jespercockx]

Yes they can, see agda/agda#5265 (comment)

[gallais]

So this means that we cannot trust a --safe in the lib file. This is distressing.

[jespercockx]

I think --safe currently has a special status that means it is treated differently from other flags. In particular there is no way to disable --safe explicitly so it's not possible to turn it off once it has been turned on explicitly (be it in the file, on the command line, or in the agda-lib file). However, for other flags such as --without-K this is currently not the case, which is what that issue is about.

[MatthewDaggitt]

Hmm, so sounds like we need two different fields in the library file default-flags which can be overridden and absolute-flags which can't? I'll open an Agda issue to discuss.