Lint Holmakefile format more
- Dominant language
- Standard ML
- Stars
- 1.2k
- Forks
- 104
- Avg merge
- 2d 21h
- Merged PRs (30d)
- 16
Description
The linting functionality of `readme_gen` currently checks that `Holmakefile`s have a reasonable-looking `all` as their first target. This issue is to add more checks, specifically:
- Ensure `all` is a `.PHONY` target.
- Ensure the `README.md` target is set up correctly (there are 4 lines of boilerplate for this). This would be helped by HOL-Theorem-Prover/HOL#511.
- Related to the above, ensure that `protect` and `dprot` are used appropriately around `CAKEMLDIR`. (If the `README.md` lines are required verbatim this is a non-issue).
- Ensure `--qof` does not appear in `CLINE_OPTIONS`, and `OPTIONS` is not used.
- Check that `INCLUDES`, `all`, `CLINE_OPTIONS` (if present), and `README.md` appear in the right order.
- Ensure `HOLHEAP` is not used.
- Optionally, check that the `INCLUDES` use `CAKEMLDIR` appropriately.
- Check line widths (if this isn't done already).
(Probably we can get by without HOL's Holmakefile parser, but being able to tap into it could be nice.)
One way to achieve this issue may be to do a quite restrictive matching against a fixed template for the first several lines of the `Holmakefile`.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.