How to test Coq libraries?

[liyishuai]

Desired Behavior

A simpler way to test Coq libraries than: https://github.com/liyishuai/coq-json/blob/master/test/dune

Example

I have a Coq library that defines several computations. I then write tests like:

Goal myFunc foo = bar.
Proof. reflexivity. Qed.

These examples may spread across multiple files in the test/ directory. I'd expect test/dune to be as simple as:

(coq.test
 (deps
  (package coq-my-package)))

[Alizter]

For an example in the wild, see Coq-HoTT:

• https://github.com/HoTT/Coq-HoTT/tree/master/test/dune
• https://github.com/HoTT/Coq-HoTT/tree/master/dune

Note that you can change what gets added to the default alias. Have a look at https://dune.readthedocs.io/en/stable/reference/aliases/default.html