Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Run opam install with -t to run tests #48

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

LasseBlaauwbroek
Copy link

No description provided.

@erikmd
Copy link
Member

erikmd commented Dec 18, 2020

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

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

@LasseBlaauwbroek
Copy link
Author

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

@liyishuai
Copy link
Member

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
Copy link
Author

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

@gares
Copy link

gares commented Feb 11, 2021

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
Copy link
Member

erikmd commented Feb 11, 2021

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

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
Copy link
Member

liyishuai commented Feb 11, 2021

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
Copy link
Member

erikmd commented Feb 11, 2021

@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 added a commit to liyishuai/coq-itree-io that referenced this pull request Feb 12, 2021
@liyishuai
Copy link
Member

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

@gares
Copy link

gares commented Feb 12, 2021

See also coq/opam#1625

@LasseBlaauwbroek
Copy link
Author

Sounds indeed like OPAMWITHTEST is the way to go.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants