Use dune's include stanza for generated tests (#729)

The current implementation of test generation is quite high friction:

 - When adding new tests, running tests directly with dune doesn't work,
   because the dune files must be generated by `make gentest`
   beforehand.  There is `make runtest`, but that always runs all the
   tests, and does not allow specifying only some tests to run (which,
   given that our test suite is quite big, is sometimes needed for quick
   iterations).

 - The generated dune files are not commited to the repository, which
   means that it is easy to forget to run `make gentest` when switching
   branches -- which either causes some tests to silently not run, or
   errors because some files are missing.

This patch solves both issues by integrating the test generation with
dune, using the `include` stanza. More precisely:

 - The test generation script (gentest.ml) is modified to write all the
   test cases on the standard output as a single file, rather than
   creating the dune test files by itself. The generated file makes use
   of the `subdir` stanza to locate the targets appropriately.

 - There is a new `dune.inc` file that is included by the `dune` file in
   `tests`, and a `diff` rule that generates the content of that
   `dune.inc` file using the `gentest.ml` script.  This is the way rules
   generation must work in dune, and it means that the `dune.inc` file
   must be commited to the repository --- which may not be such a bad
   thing, see above.

The rule generation is added to the `gentest`, `runtest`,
`runtest-quick` and `runtest-ci` aliases.

The advantage of the new approach is that since the dependency is known
to dune (and not only to make), running a command such as
`dune build @tests/issues/XXX/runtest-quick` will always regenerate the
tests, and also that we won't have to delete `dune` files manually when
switching branches, since everything is in the file that gets
re-generated.

It means that running tests is slightly slower, because it always
requires running the `gentest` script --- but that is probably fine,
until we have many more tests than currently.

.github/workflows/build.yml

@@ -48,9 +48,6 @@ jobs:
       - name: Build alt-ergo with opam
         run: opam exec -- opam reinstall .
 
-      - name: Generate tests
-        run: opam exec -- make gentest
-
       - name: Run tests
         run: opam exec -- make runtest-ci
 

.gitignore

@@ -41,8 +41,5 @@ alt-ergo.js
 alt-ergo-worker.js
 www/
 
-# Generated dune files by gentest
-tests/*/**/dune
-
 # Generated nix files
 /result*

Makefile

@@ -118,7 +118,7 @@ packages:
 # Generate new Dune tests from the problems in
 # the directory tests/.
 gentest: $(wildcard tests/**/*)
-	dune exec -- tools/gentest.exe tests/
+	dune build @tests/gentest --auto-promote
 
 # Run non-regression tests.
 runtest: gentest bin

tests/dune

@@ -1,3 +1,26 @@
 (cram
  (package alt-ergo)
  (deps %{bin:alt-ergo}))
+
+(include dune.inc)
+
+(rule
+ (deps (file ../tools/gentest.exe) (source_tree .))
+ (action
+  (with-stdout-to dune.inc.gen (run ../tools/gentest.exe .))))
+
+(rule
+ (alias gentest)
+ (action (diff dune.inc dune.inc.gen)))
+
+(rule
+ (alias runtest)
+ (action (diff dune.inc dune.inc.gen)))
+
+(rule
+ (alias runtest-quick)
+ (action (diff dune.inc dune.inc.gen)))
+
+(rule
+ (alias runtest-ci)
+ (action (diff dune.inc dune.inc.gen)))