Make Jenkins testing script runnable locally without Jenkins environment setup

[ehildenb]

The script is organized slightly (so that parameters come at the top), and more notifications about build process are produced.

Also, the rv-match testing is done differently. Instead of cloning to subdirectory $WORKSPACE/k-pr, we're cloning directly to $WORKSPACE. K-Exercises tests are unaffected, but rv-match is now cloned to a subdirectory $WORKSPACE/rv-match, and we use manually update the K submodule inside RV-match to point directly at the HEAD of the checkout of K at $WORKSPACE. (so no more rm ... ; cp ... going on, just git ... operation).

[dwightguth]

Also what does -ff do? Unless this option cleans submodules then this is still not going to work.

[ehildenb]

From man git clean:

       -f, --force
           If the Git configuration variable clean.requireForce is not set to false, git clean will
           refuse to delete files or directories unless given -f, -n or -i. Git will refuse to delete
           directories with .git sub directory or file unless a second -f is given.

[ehildenb]

So it makes sure that the rv-match and k-exercises repositories are actually deleted along with any other junk.

[dwightguth]

Has this been tested in the case it fails? I ask because the last time you wrote something in approximately this syntax I had to change it because it didn't actually work.

[ehildenb]

[dev@arch-ehildenb k-pr]$ exit_status='0'
[dev@arch-ehildenb k-pr]$ echo "$exit_status"
0
[dev@arch-ehildenb k-pr]$ ( cd k-distribution/
> false
> ) || exit_status="$?"
[dev@arch-ehildenb k-pr]$ echo $exit_status
1
[dev@arch-ehildenb k-pr]$ 

The parenthesis spawn a sub-shell (so that any cd that happen don't get carried over past that part of the script). The semantics of $? is that the last command run (in sub-shell or otherwise) by the bash interpreter will be stored in $?. So if cd ... fails, then we'll get the exit_status set to the failure code of cd, and if cd succeeds and make fails, then exit_status will be whatever make returns.

[dwightguth]

What is this? I liked it better when we were just copying the directory into place. This feels error prone to me.

[ehildenb]

The reason to do this is because we want the rv-match tests to be runnable from directly in the K directory (without having to move to a temporary directory or work from one directory up like we were before).

The git fetch ../../ will fetch the current HEAD of the repository at ../../, which is the current checkout of K. git fetch with an anonymous remote (here ../../) updates FETCH_HEAD to whatever the remote HEAD is. Nothing too fancy here.

Benefits of this approach:

• Jenkins script is directly runnable from the K repo directory (trying to use cp to do this would result in recursively copying the rv-match repo into itself).
• We are sure that the rv-match submodule is updated to exactly the version of K that is being tested, because we fetch it directly.

[ehildenb]

Jenkins: test this please.