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

Simplifying Makefiles in test and examples #3594

Merged
merged 5 commits into from
Oct 24, 2024
Merged

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented Oct 24, 2024

This is a follow up to #3578. The test.mk makefile now "knows" about extraction, building executables, running them, getting output (both error output and program output) and comparing to .expected files. Previously we had rules for this scattered everywhere.

The key points are:

  • Usually all you have to do is set FSTAR_ROOT and inclued mk/test.mk. This will already cause that running make here verifies every file in dependency order.
  • If there are subdirectories, use SUBDIRS+= to add list them. They will be recursively built (but without imposing any order, maybe we could change this if we want to build modules or components separately).
  • Using the variables EXTRACT, BUILD, and RUN, we can state that some files are meant to be extracted (to OCaml), built (as an exe from a single ml file), or ran to check that they don't crash. Running generates a .out file with the output.
  • .extracted files anywhere are automatically picked up and added to the default rule. So, if X.fst and X.ml.expected exists, running make will extract X.fst and check that it matches exactly (modulo some whitespace) the contents of X.ml.expected.
  • The .expected suffix works for most other rules. Creating X.out.expected will trigger extracting + building + running of X.fst and compare the output of X.exe to the file.
  • The accept target sets all existing .expected files to their actual result. A git diff can be used to review and maybe commit the difference.
  • tests/bug-reports is now a lot simpler in that it has a closed subdir with closed issues which is checked (some files are ran too, exactly like now, but the makefile is much simpler) and an open directory that is unchecked. There's no need to update lists of files any more, just drop an fst where appropriate.
  • All output (touch files, .ml, .cmxs, .exe, etc) goes into _output.

@mtzguido mtzguido merged commit e8fcdde into FStarLang:master Oct 24, 2024
2 checks passed
@mtzguido mtzguido deleted the mk branch October 24, 2024 03:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant