Cram test support seems too limited for Coq

[rlepigre]

Desired Behavior

Cram tests where Coq code is built (with dune) against a coq theory from a local package (explicit dependency being given) fails by not finding the library. Ideally, this would just work as the analogous code in OCaml (see #6011).

Example

An example (in the form of a reproducing test case) is given in #6014.

[rlepigre]

I noticed that I need to do the following manually in cram tests to make them work:

export COQPATH="$DUNE_SOURCEROOT/_build/install/default/lib/coq/user-contrib"

Maybe we should ensure that the COQPATH is extended in cram tests when requiring a library that includes Coq theories?

[Alizter]

@rlepigre That seems sensible. As of today, cram tests have no special support for Coq tests, but it doesn't have to be that way.

[ejgallego]

I agree, let's fix this. I suggest we only extend ROCQPATH/ROCQLIB if Rocq mode is enabled.

We also should ensure this works when Rocq itself is vendored.

[gmalecha]

This comment probably shows my lack of understanding of what dune is actually doing, but wouldn't it be nicer to build the cram test as if it was a new library that depends on the library that is being tested? This would mean that you wouldn't need to install the dependency right?

Personally, I have seen a lot of issues with needing to run dune clean when I change worktrees that are adding files that get built and then installed and then produce broken symlinks in the install directory.

[ejgallego]

Hi @gmalecha ,

wouldn't it be nicer to build the cram test as if it was a new library that depends on the library that is being tested?

I'm not expert on CRAM, but isn't that the idea that you get a fully working environment after the build of your project, where you can use the shell to test? What would "building the cram test" as a Rocq theory mean here?

Personally, I have seen a lot of issues with needing to run dune clean when I change worktrees that are adding files that get built and then installed and then produce broken symlinks in the install directory.

Oh, that's certainly a bug, dune build should clean up by itself, please open an issue next time you see this problem.

[gmalecha]

@ejgallego Thanks for the explanation, that makes a lot of sense. I guess the situation that we have is a little bit strange. The main reason that we want to use CRAM tests is to test things like printing notation and error messages. For example,

Notation foo x := (x + x)
Definition x := 1 + 1.
Print x.

Here, the cram test setup is really useful because if we break our notation printing then the test fails. Maybe this is really a limitation of Rocq where you can't do this sort of test inside Rocq itself, which would probably be ideal. Perhaps a command like:

TestOuput Print x
Outputs "foo 1".

would be a better way to achieve this.

[Alizter]

This recent proposal might be of interest: rocq-prover/rfcs#107

[ejgallego]

@gmalecha , Dune output tests could be a better fit for that use case.

[ejgallego]

where you can't do this sort of test inside Rocq itself, which would probably be ideal.

I agree that it would be nice to do this inside Rocq, however for things to work well, Rocq would need integration with Dune's test runner, as done for other testing frameworks.