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

Lint building of *Lib.sml files #1116

Open
dnezam opened this issue Dec 14, 2024 · 0 comments
Open

Lint building of *Lib.sml files #1116

dnezam opened this issue Dec 14, 2024 · 0 comments
Labels
dev experience Makes tasks developing cakeml itself easier tooling Things like building, linters and LSP

Comments

@dnezam
Copy link
Contributor

dnezam commented Dec 14, 2024

Since *Lib.sml files seem to only get built when theories depend on them, it is possible for them to bitrot without being caught by the regression test suite. This issues tracks the creation of a tool/linter that can catch these untested files and recommends to either delete them, or create a theory that depends on them.

One potential way to get this to work is to use build-sequence and the ability of Holmake to create a dependency graph, to create a list of all *Lib.sml files that are currently tested. Then, one should be hopefully able to find all *Lib.sml files that are currently flying under the radar. The basic idea is similar to what is being done in #1115.

@dnezam dnezam added dev experience Makes tasks developing cakeml itself easier tooling Things like building, linters and LSP labels Dec 14, 2024
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 tooling Things like building, linters and LSP
Projects
None yet
Development

No branches or pull requests

1 participant