2019-05-09 12:0:40 (GMT)
Hi,
I'll start working with Petar on Zipperposition and consequently having access rights for the GitHub repository would be useful. My GitHub profile name is 0function.
Regards, Visa
2019-05-09 13:44:23 (GMT)
Which github? The MPI one or the normal one?
2019-05-09 13:58:30 (GMT)
For now, the normal one is enough. @Simon Cruanes
The problem with the MPI one is that Petar and Simon don't have access there either. Do you think we could add all of them?
2019-05-09 14:3:33 (GMT)
Adding them all is possible. However, I am tempted to say that the better way is to convince @Sophie to use the normal Github.
Two reasons in favour of changing:
* The MPI Github will probably get ditched at some point this year to be replaced by Gitlab. Let's see how that will go.
* It is easier to contribute with people, instead of having to wait two days (or more) before an account is created.
But it is up to you to decide that. I don't care.
2019-05-09 14:8:59 (GMT)
Well, the advantage with MPI GitHub is the testing infrastructure that you set up.
2019-05-09 14:9:27 (GMT)
But maybe it's possible to do that with Travis on the normal GitHub, too?
2019-05-09 14:11:27 (GMT)
Could all of them also get a VPN account?
2019-05-09 14:15:48 (GMT)
There are two things about the testing infrastructure:
2019-05-09 14:16:6 (GMT)
I think a VPN account is the same as a normal account
2019-05-09 14:17:0 (GMT)
but the testing itself does not care where the repo is located. So you can switch to Github.
oh really? I thought that was why we moved to the MPI GitHub!
2019-05-09 14:17:58 (GMT)
The only issue is if you want to print the status of the build on the repository itself. Except that I never managed to make that work.
2019-05-09 14:19:34 (GMT)
(badges like: https://github.com/dwyl/repo-badges require access to the server from outside, which does not work)
2019-05-09 14:20:43 (GMT)
Ok, that's not necessary.
2019-05-09 14:21:21 (GMT)
Do you have experience with Travis? Do you think it would be possible to set up something similar there?
2019-05-09 14:21:43 (GMT)
(I'm not saying that you should do it of course!)
2019-05-09 14:22:16 (GMT)
Then we would be independent of the MPI acoounts.
2019-05-09 14:23:28 (GMT)
@Haniel Barbosa as far as I know, CVC4 is using Travis. Are you using it for testing? Or just to test if it compiles?
2019-05-09 14:24:21 (GMT)
We use it for testing, yes
2019-05-09 14:24:30 (GMT)
It runs a series of regression testes
2019-05-09 14:25:22 (GMT)
How much time to you get for free? Or can you run the entire SMT comp?
2019-05-09 14:25:35 (GMT)
We've recently reduced the number of builds and of regressions we run with travis because it was getting too slow. Currently it's 3 builds and the quickest regressions
2019-05-09 14:26:17 (GMT)
I don't think there is a time limit, it's more a matter of how many / how fast machines
2019-05-09 14:26:46 (GMT)
Our bottleneck is that we only merge pull requests that pass travis
2019-05-09 14:27:0 (GMT)
If it takes too long it slows down development
2019-05-09 14:27:18 (GMT)
We do more extensive testing in a dedicated cluster during the nights
2019-05-09 14:28:14 (GMT)
Ok, that dedicated cluster corresponds to the MPI server for us then :-)
2019-05-09 14:29:45 (GMT)
And it might make sense that the cluster sends an email if something fails, instead of forcing the user to look up. That way, people don't even need an MPI account to see if something is broken.
2019-05-09 14:30:9 (GMT)
That's the setup we have
2019-05-09 14:31:41 (GMT)
Ok, I think we should stop using the MPI GitHub then, but it would be great if we could use the Jenkins for the normal GitHub.
2019-05-09 14:32:4 (GMT)
(and get VPN & Jenkins accounts for all developers)
2019-05-09 15:6:45 (GMT)
Haven't looked at jenkins recently, but can't it post updates to github (rather than being accessible from it), assuming proper credentials?
2019-05-10 5:47:22 (GMT)
I think @Petar Vukmirovic already has an MPI-github account. For the others, It would be better for me if we wait until next week to start the process.
2019-05-10 5:49:56 (GMT)
And indeed, the MPI-github should become an MPI-gitlab at some point in the (near) future. @Mathias Fleury : Will that be a problem for Jenkins (or rather for you to setup jenkins again)?
2019-05-10 8:5:9 (GMT)
But Mathias said that Jenkins could also use the normal GIthub. Then we wouldn't need to use MPI-github or MPI-gitlab.
Actually, I can have a look if I can set this up right now.
2019-05-10 8:6:10 (GMT)
All we need are VPN & Jenkins accounts for Petar, Simon and Visa then.
2019-05-10 8:47:1 (GMT)
Yes, it looks like it works! We don't need MPI GitHub then.
2019-05-10 9:16:5 (GMT)
For the others, It would be better for me if we wait until next week to start the process.
Ok, there is no hurry.
2019-05-10 10:36:10 (GMT)
@Sophie The current setup is repo agnostic. It is only pulling every 30 minutes to see if anything changes. The setup could be better (with badges, ...), but I never understood how to make that work (partly because MPI-Github cannot communicate with jenkins and partly because I did not spend too much time on that).
2019-05-10 11:7:12 (GMT)
So changing the repo is changing one line in the settings
2019-05-10 12:21:0 (GMT)
Can we get Visa access rights to official GitHub? :)
Thanks
2019-05-10 12:55:33 (GMT)
@Simon Cruanes
2019-05-10 12:56:26 (GMT)
@Simon Cruanes did you consider giving Alex or Petar admin rights?
2019-05-10 13:30:27 (GMT)
Good point, if they're ready to accept the big responsibilities that come with such power :wink:
2019-05-10 14:35:44 (GMT)
Of course :)
2019-05-10 14:43:9 (GMT)
Hmmm it seems I cannot make other people admins on my own repo (if you find how, I'm interested). An option would therefore be to have a github organization where Zipperposition can live (and possibly other related tools)?