Open Ivan-Velickovic opened 1 year ago
Agreed. At least compiling does definitely male sense, yes.
This should be relatively easy to achieve and should only need the corresponding entries in the platforms.yml file.
Actually, RPI3 and RPI4 are in the test and have been built regularly for quite a while. Have you checked the build logs for the rest of the list? (or the platforms.yml file -- disabled
means no hardware test, but still build. Only no_hw_build
excludes a platform from the build).
Can you point me to a run where they were built? I can't see it as part of the CI that runs for the kernel itself, e.g https://github.com/seL4/seL4/actions/runs/7380751924/job/20078457216.
Nevermind, my browser did not load the log file properly. I can see RPi3 being built for 32-bit and RPi4 being built for 64-bit. I think when I created the issue I meant to say that since we have both of those platforms we should also do run-time tests, but that can be a separate issue.
Basically just wanted a list of everything that either needs to be tested at run-time as well if we have the hardware, or only build-time if we don't.
I believe the current status of the CI (for sel4test at least) is that not all platforms that claim to be supported are tested. Obviously we cannot buy all the hardware to actually run the tests, but just compiling them to eliminate any build errors is trivial.
Here's what I've seen missing so far: