Use `dynamic_include` to include the generated file dune.inc

[Halbaroth]

This PR uses the new feature dynamic_include to include our generated file dune.inc.

Pros:

• We do not push dune.inc anymore!
• The output of dune.inc depends on the plateform. This is the main motivation of this PR because Windows does not use the same convention for paths.

Cons:

• We need Dune >= 3.14
• We cannot use the stanza subdir in dune.inc, which means we have to ensure we do not use twice the same name for two tests even if there are not in the same directory. See issue https://github.com/ocaml/dune/issues/10405
• We have to use a strange trick to avoid cyclic dependency between directories: https://dune.readthedocs.io/en/latest/howto/rule-generation.html#using-dynamic-include

I also bump the version of nixpkgs.

[bclement-ocp]

Global comments:

The output of dune.inc depends on the plateform. This is the main motivation of this PR because Windows does not use the same convention for paths.

I think for this specific issue we could also simply x ^ "/" ^ y instead of Filename.concat x y in gentest.ml if we are not happy with the drawbacks of dynamic_include.

which means we have to ensure we do not use twice the same name for two tests even if there are not in the same directory

What would happen if we have two files with the same name? I think this is a deal-breaker if there is a silent failure. Does this only concern the generated files or also the source files? Could we work around it by mangling the names (e.g. by having a dune rule that generates ac__testfile-ac_arith001.ae from ac/testfile-ac_arith001.ae)?

We have to use a strange trick to avoid cyclic dependency between directories

Bummer that we need to add a dummy directory inside tests. Could we do something like this in the toplevel dune file instead:

(subdir tests
  (dynamic_include ../gentest/dune.inc))

(subdir gentest
  (rule
    (deps (source_tree ../tests))
    (action
      (with-stdout-to dune.inc (run ../tools/gentest.exe ../tests)))))

Edit: actually do we need to dummy directory? The example here only uses subdir to create virtual sub-directories, not actual sub-directories in the file system — possibly we can do the same?

[Halbaroth]

Edit: actually do we need to dummy directory? The example here only uses subdir to create virtual sub-directories, not actual sub-directories in the file system — possibly we can do the same?

I followed this example to write the dune file. The run and generate subdirs are virtual in my file too (there only exists in _build/default/tests).

What would happen if we have two files with the same name? I think this is a deal-breaker if there is a silent failure. Does this only concern the generated files or also the source files? Could we work around it by mangling the names (e.g. by having a dune rule that generates ac__testfile-ac_arith001.ae from ac/testfile-ac_arith001.ae)?

We got an error because there are several rules to produce the same file. Mangling their names is a better idea.

Bummer that we need to add a dummy directory inside tests. Could we do something like this in the toplevel dune file instead:

I got a cyclic dependency + this strange error message:

Error: Trying to build _build/tools/gentest.exe but build context tools
doesn't exist.
-> required by _build/default/gentest/dune.inc
-> required by dynamic_include gentest/dune.inc in directory tests

If I replace tests by a virtual directory run, I still got this message.

EDIT: I did a mistake. It works if we replace tests by run.

[bclement-ocp]

I followed this example to write the dune file. The run and generate subdirs are virtual in my file too (there only exists in _build/default/tests).

I was talking about the new input directory in tests which doesn't look like it would be necessary.

[bclement-ocp]

~I got a cyclic dependency + this strange error message:~

Error: Trying to build _build/tools/gentest.exe but build context tools
doesn't exist.
-> required by _build/default/gentest/dune.inc
-> required by dynamic_include gentest/dune.inc in directory tests

If I replace tests by a virtual directory run, I still got this message.

EDIT: I did a mistake. It works if we replace tests by run.

Ah yes because the name of the directory. No strong feeling on whether to put this at toplevel or in tests/dune but I'd prefer a solution without the input directory.

[Halbaroth]

Done :) Let's see if the CI succeeds. I will test on my PR for the Windows CI too.

[bclement-ocp]

Before:

After:

I am suspicious — the CI succeeds but I don't think the tests actually run.

[Halbaroth]

They ran on my computer and they ran too on my Windows CI: https://github.com/Halbaroth/alt-ergo/actions/runs/10316591153/job/28559137021

[Halbaroth]

In case of success, the expected output is:

dune build  @src/bin/text/all
ln -sf src/bin/text/Main_text.exe alt-ergo
dune build @runtest @runtest-quick

I do make clean and make runtest to be sure, and they run on my computer.

[bclement-ocp]

In case of success, the expected output is:

dune build  @src/bin/text/all
ln -sf src/bin/text/Main_text.exe alt-ergo
dune build @runtest @runtest-quick

I do make clean and make runtest to be sure, and they run on my computer.

We would get the same output if the tests are not actually run due to misconfiguration. Maybe there is a chance we don't run them b/c they have been ran previously in the dune cache? I don't see how this PR would reduce the time to run tests from 1min to 10s.

[bclement-ocp]

Maybe there is a chance we don't run them b/c they have been ran previously in the dune cache?

I think I'm convinced by this explanation, the tests do seem to run on my machine as well. LGTM once we patch gentest to have a mode where it only generates the .expected files.

[Halbaroth]

Done :)