Deployment setup

[ejgallego]

We need some minimal information about how the deployment of the script is working, so we can start documenting / improving the workflow.

I am taking the freedom to assign this to @maximedenes as discussed in the WG.

[maximedenes]

As I said during the WG, I'm not up-to-date on how the deployment is done since @ppedrot worked on it, so assigning to him.

[ejgallego]

Thanks @maximedenes , sorry I misunderstood. It is you maybe who has to give me access to the machines tho?

@ppedrot let me know when you can any info you have, thanks!

[maximedenes]

Thanks @maximedenes , sorry I misunderstood.

No problem, I think you simply missed the moment during the WG when @ppedrot reminded us he had worked on improving the deployment of the script.

It is you maybe who has to give me access to the machines tho?

Yes, this I can do. Let's talk offline.

[ejgallego]

@ppedrot ping.

[ppedrot]

That's pretty trivial, the shell script run on Jenkins invokes the update.sh script before running, and the latter is responsible for pulling the latest version of the the bench. FTR, this is currently the script used on Jenkins:

. ~/.opam/opam-init/init.sh
~/git/coq-bench/update.sh origin master
~/git/coq-bench/two_points_on_the_same_branch.sh

and this is the update.sh script:

#! /bin/sh -e

remote=$1
branch=$2

cd `dirname $0`
git fetch "$1"
git reset --hard "$remote/$branch"

[ejgallego]

Not relevant anymore.