Deducteam / Logipedia

An encyclopedia of proofs
56 stars 11 forks source link

draft circle configuration (type checks the dk proof library) #8

Closed rprimet closed 5 years ago

francoisthire commented 5 years ago

Why did you choose to use CircleCI than Travis?

rprimet commented 5 years ago

Hi François,

Right now, we are not sure of whatever solution is the best, and hence are exploring our options. We started with CircleCI because, among other things,

Other options that we are also considering are Travis, and Gitlab CI (which would let us provide our own build machines -- this may come in handy during deployment).

But as I said, we picked what we thought was a sensible starting point to explore / prototype.

Is there any compelling reason for using something else? (Travis or otherwise?)

francoisthire commented 5 years ago

I can check that everything is OK? How can I run CircleCI?

rprimet commented 5 years ago

You can go to circleci.com, log in using your github credentials and enable circleCI for the Deducteam/Logipedia project. Not sure whether this will run a CI job for the current pull request, but you can check that it completed correctly on the branch here.

Unfortunately I do not have the credentials to enable CircleCI on the Deducteam org.

If you want to merge the branch locally and run the job on your own machine, instructions are available here (but I can also fix issues if they arise after the merge).

francoisthire commented 5 years ago

It should be fine now, can you confirm?

Le mar. 28 mai 2019 à 16:36, Romain Primet notifications@github.com a écrit :

You can go to circleci.com, log in using your github credentials and enable circleCI for the Deducteam/Logipedia project. Not sure whether this will run a CI job for the current pull request, but you can check that it completed correctly on the branch here https://circleci.com/gh/rprimet/Logipedia/3.

Unfortunately I do not have the credentials to enable CircleCI on the Deducteam org.

If you want to merge the branch locally and run the job on your own machine, instructions are available here https://circleci.com/docs/2.0/local-cli/ (but I can also fix issues if they arise after the merge).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/Deducteam/Logipedia/pull/8?email_source=notifications&email_token=AATJVK5VT3HADYJAJ3JYOKLPXU7QHA5CNFSM4HP36DXKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODWMKVDI#issuecomment-496544397, or mute the thread https://github.com/notifications/unsubscribe-auth/AATJVKY22KUS6ZXOXGHY2I3PXU7QHANCNFSM4HP36DXA .

rprimet commented 5 years ago

Yep, thanks! Although I cannot see the builds for the Dedukteam org except by manual probing...e.g. going to https://circleci.com/gh/Deducteam/Logipedia/2

But that's something I should try to figure out.

Would it be also possible to enable Github checks for Circle too? This would bring a nicer integration (e.g. we'd get build results attached to pull requests...)

Thanks!