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.
This is a follow up to #3578. The
test.mkmakefile now "knows" about extraction, building executables, running them, getting output (both error output and program output) and comparing to.expectedfiles. Previously we had rules for this scattered everywhere.The key points are:
FSTAR_ROOTand inclued mk/test.mk. This will already cause that runningmakehere verifies every file in dependency order.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).EXTRACT,BUILD, andRUN, 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.outfile with the output..extractedfiles anywhere are automatically picked up and added to the default rule. So, ifX.fstandX.ml.expectedexists, runningmakewill extractX.fstand check that it matches exactly (modulo some whitespace) the contents ofX.ml.expected..expectedsuffix works for most other rules. CreatingX.out.expectedwill trigger extracting + building + running ofX.fstand compare the output ofX.exeto the file.accepttarget sets all existing.expectedfiles to their actual result. Agit diffcan be used to review and maybe commit the difference.tests/bug-reportsis now a lot simpler in that it has aclosedsubdir with closed issues which is checked (some files are ran too, exactly like now, but the makefile is much simpler) and anopendirectory that is unchecked. There's no need to update lists of files any more, just drop an fst where appropriate.