Run opam install with -t to run tests

[LasseBlaauwbroek]

No description provided.

[erikmd]

Thanks @LasseBlaauwbroek − but I believe this use case was already addressed by this feature?

https://github.com/coq-community/docker-coq-action#export

[LasseBlaauwbroek]

I guess so, but I would say that running tests is an integral part of CI. So it should be enabled by default.

[liyishuai]

We may default OPAMWITHTEST to true and allow users to set it to false.
Having -t in command line will disallow users to configure.

[LasseBlaauwbroek]

Yes, that's what I was thinking of as well.

[gares]

oops, I did not see this when I opened #52 .
I think --with-test should not be padded to dependencies.
I like the suggestion of @liyishuai to make it configurable defaulting to on (for the package, not the deps)

[erikmd]

Hi all, thanks for your comments. To sum up:

• the feature proposed in Run opam install with -t to run tests #48 and in [build] pass --with-test for the current package #52 is already available (as an "opt-in"), cf. the export field;
• so the discussion just amounts to: should we enable the feature by default as an "opt-out"?
• from a CI perspective, I agree with this idea!
• however I'm not favorable with merging Run opam install with -t to run tests #48 because it would trigger tests for dependencies as well, while the focus is especially on the $PACKAGE, not on its dependencies (the test-suite of which being possibly broken, and this is orthogonal to developing/testing the $PACKAGE itself);
• [build] pass --with-test for the current package #52 is better from that viewpoint, however it can't easily be seen as "opt-out", because disabling the tests running would require to redefine the whole script field;
• hence the suggestion by @liyishuai to hardcode a default value for OPAMWITHTEST;
• however it is not fully satisfactory either, as it would impact the dependencies as well…

Maybe we'll find another simple solution to achieve this; in the meantime I propose to postpone the merge of #52, e.g. to the next major/minor release of docker-coq-action.

[liyishuai]

IIUC dependencies are not tested by opam install --deps-only -t blah: https://opam.ocaml.org/doc/man/opam-install.html

-t, --with-test, --build-test
Build and run the package unit-tests. This only affects packages listed on the command-line.

In other words, -t and OPAMWITHTEST are ignored given -deps-only.

[erikmd]

@liyishuai OK I see.

Worth doing a small test anyway! :)
e.g. doing export OPAMWITHTEST=true then installing a package that depends on a package with a test specified… would you have the time to check this?

in which case, we could indeed think about a PR that asserts OPAMWITHTEST=true by default − except if passed otherwise like this:

  - uses: coq-community/docker-coq-action@v1
    with:
      opam_file: 'folder/coq-proj.opam'
      coq_version: 'dev'
      ocaml_version: '4.07-flambda'
      export: 'OPAMWITHTEST'
    env:
      OPAMWITHTEST: 'false'

[liyishuai]

Yes I've just examined that OPAMWITHTEST=true does not test dependencies.

[gares]

See also rocq-prover/opam#1625

[LasseBlaauwbroek]

Sounds indeed like OPAMWITHTEST is the way to go.