Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

take L4V_PLAT into account in rebuilds #762

Open
lsf37 opened this issue Jun 4, 2024 · 0 comments
Open

take L4V_PLAT into account in rebuilds #762

lsf37 opened this issue Jun 4, 2024 · 0 comments
Assignees
Labels
build system related to building the proofs or kernel

Comments

@lsf37
Copy link
Member

lsf37 commented Jun 4, 2024

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?

@lsf37 lsf37 added the build system related to building the proofs or kernel label Jun 4, 2024
@lsf37 lsf37 self-assigned this Jun 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
build system related to building the proofs or kernel
Projects
None yet
Development

No branches or pull requests

1 participant