Some extra comments:

* I have to really really prevent myself from just making the <operating-system>
field KERNEL a list.  Because that's what happens at runtime anyway.
It's just an union of those things, then it runs depmod.  The separation
into KERNEL and KERNEL-LOADABLE-MODULES is artificial.

* There's a collision warning:

warning: collision encountered:
  /gnu/store/3ar8aym8khxh1rdjf5gxqsk0hv7r9p96-linux-module-database/lib/modules/5.4.22-gnu/modules.symbols.bin
  /gnu/store/4r0fz0f37bp1zqbqclgrq1l4sm1acy4p-linux-libre-5.4.22/lib/modules/5.4.22-gnu/modules.symbols.bin
warning: choosing /gnu/store/3ar8aym8khxh1rdjf5gxqsk0hv7r9p96-linux-module-database/lib/modules/5.4.22-gnu/modules.symbols.bin

I think that's because the Linux kernel linux-libre we build already has those
files.  Those files in linux-libre are stale cache files when you have extra
modules (because they don't list those extra modules).

@Ludo: You said I should remove the null? case (check if there are no extra modules).

I did, so actually, these modules.*.bin files in linux-libre are useless since
the profile-derivation of linux-module-database will rebuild them anyway (via
depmod), also in the case with no extra modules.

The reason I had the null? case before is in order to leave the case with no
extra modules unchanged from before (defensive programming).

But now that we don't do that, should we make linux-libre not invoke depmod?
Or should we filter those files out manually in the profile hook?