Description
Currently, the cspec/c Makefile is insensitive to changes in L4V_PLAT in the sense that it will not necessarily rebuild correctly when you change the value of L4V_PLAT. This is no problem in CI since that always starts from a clean slate, but it is annoying when working manually and incrementally.
The immediate reason for this is that L4V_PLAT is an env variable and the Makfile of course only tracks file system changes. It'd be easy enough to make such changes visible in the file system by making e.g. the build path not just build/$L4V_ARCH/, but build/${L4V_ARCH}_${L4V_PLAT}/. This leads to correct rebuilds.
But: as seen in #761 Isabelle's ROOT file parsing and the external_file command (as well as install_C_file) do not allow this pattern. Env substitution seems to have to be on an entire path segment, not in a substring.
Therefore we could do for instance build/$L4V_ARCH/$L4V_PLAT, but this would mean that $L4V_PLAT always has to be set, which is currently not the case. We could choose defaults in the Makefile so that usage via run_tests and make wouldn't change, but usage via isabelle build directly would need to set L4V_PLAT manually.
I guess we could add the default L4V_PLAT computation also to the provided etc/settings file, which would also help, but it will still make the main instructions to run anything directly via isabelle build one step harder. Then again, you do have to use make anyway if you want to do CKernel or related images, since it has to build the kernel source first.
Any opinions or other ideas before I go and implement the build/$L4V_ARCH/$L4V_PLAT variant and defaults for L4V_PLAT in make and etc/settings?