Should the KernelHaveFPU/CONFIG_HAVE_FPU seL4 configuration option be replaced with architecture specific ones?

There is a kernel configuration option KernelHaveFPU (CONFIG_HAVE_FPU in source code) which roughly implies that the kernel is compiled with some level of FPU support. This means that if KernelHaveFPU isn’t enabled, user level images that are compiled assuming access to an FPU will not work.

On arm architectures it is well defined what this setting is for and what it does, but on x86 it is forced set and the arch specific code doesn’t query the option. The RISC-V kernel arch assumes that the floating point ISA extensions aren’t present on the hardware or have been disabled in machine mode and so the option is also not queried.

The question is whether KernelHaveFPU is generic enough to be a valid option for all architectures, or should be replaced by arch specific options.