packages with a validate target should have a run-test

[JasonGross]

Apparently opam has --with-test. The doc on making opam packages should suggest filling this field, and the packages which have validate targets available should get this field.

[palmskog]

I agree that it's nice for packages to provide a run-test clause or similar in their opam files that can be run with --with-test, but to be honest I wouldn't recommend having it for pure Coq projects. The behavior of something like make validate or a coqchk command for "testing" of pure Coq projects is in my view so unpredictable right now (e.g., in terms of time/memory) that it shouldn't be widely used. And almost nobody even knows that make validate exists, much less what it does.

[Alizter]

Do you know of a way we can pass the validate target through opam? The coq repo bench for instance tests opam packages, so it would be nice to be able to call the validate job via opam somehow.

Jason's suggestion would work, but I think a lot of packages have other things that would count as tests so I wouldn't want that to be enforced in general.

[palmskog]

With the usual assumptions about opam, the only way to run a command for a project through opam is when the opam package provides a way to run it, e.g., in the build clause, run-test clause, or install clause. You might be able to convince key project maintainers to add something like the following:

run-test: [make "validate"]

But this assumes they are using coq_makefile under the hood. And it means we would potentially run the validation step every time someone submits a package change for that project. So I'm not sure it's a good idea.

It may be better to introduce some kind of flag that can conditionally run validation:

build: [
  make "-j%{jobs}"
  make "validate" {my_flag:true}
]

This would be far less intrusive and maintainable.

[JasonGross]

Does the CI here run the testing step / use --with-test?

How do custom opam flags work?

[palmskog]

I'm not sure opam can currently define custom flags on the fly, but you could always do a package similar to coq-native, i.e., a virtual package that indicates some capability. And then you check something analogous to {coq-native:installed}.