Git and KTest

Many of us don't want to run ktest on the computers where we write code, perhaps because they are slow laptops. This is a note on how to set up git to help you easily test changes on a fast computer, without breaking the build. I'll suppose you have an ssh account kdev on server.example.com.

Setup

The first step is to make a new empty git repository on the server, and change a setting to make it easy to push your changes to it.

git init k-framework-testing
cd k-framework-testing
git config receive.denyCurrentBranch false

The next step is to set up your working copy of K so you can easily push changes to the server. Suppose the full path to the testing repository on the server is /home/kdev/k-framework-testing. Then in your K checkout on your working machine, run

git remote add server ssh://[email protected]/home/kdev/k-framework-testing
git config remote.server.push +master

Use

Whenever you want to test your latest local commits, run

git push server

in your working directory, then in the testing directory on the server run

git reset --hard

to update the checked-out files with your changes, before running ktest or whatever

Variations

If you work with many branches, you replace the "refspec" +master with something else, or perhaps set up the master to push as a mirror, as document in the git-remote and git-push (and maybe git-config) man pages.

You might name this remote "origin" and the remote for github something else, to avoid accidentally pushing to github after all.

If you already have and sometimes work directly in a K checkout on fslwork, you might want to configure a second directory as a "bare repository".