CakeML / CakeML/cakeml

Lint Holmakefile format more

Open
#586 0 comments 0 reactions 0 assignees View on GitHub
dev experience enhancement tooling
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.