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

Add missing directories to build-sequence #1095

Open
dnezam opened this issue Nov 22, 2024 · 1 comment
Open

Add missing directories to build-sequence #1095

dnezam opened this issue Nov 22, 2024 · 1 comment
Labels
dev experience Makes tasks developing cakeml itself easier refactoring

Comments

@dnezam
Copy link
Contributor

dnezam commented Nov 22, 2024

At the moment, it appears that there are some directories that contain a Holmakefile, but are not mentioned in developers/build-sequence and hence not part of the regression suite. This lead to some directories having bit-rotted away.

The goal of this issue is to add all missing directories to build-sequence. If some directories cannot be built, they should either be fixed or removed*, potentially creating an issue if there is demand to add it back in the future.

For the future, ideally a linter would make sure that no directory can slip past the regression suite.

* Exceptions may apply.

@dnezam dnezam added dev experience Makes tasks developing cakeml itself easier refactoring labels Nov 22, 2024
@xrchz
Copy link
Member

xrchz commented Nov 22, 2024

There's apparently something called check_builds in HOL4 that does the linting thing

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
dev experience Makes tasks developing cakeml itself easier refactoring
Projects
None yet
Development

No branches or pull requests

2 participants