Setup Google Compute Engine Instance

1. Make a disk based off a LTS Ubuntu image
2. Create or re-use a static ip

https://console.cloud.google.com/networking/addresses/list?project=defthm-acl2

1. Hook it up to an instance template

The GUI console doesn't let us assigned a static IP to a preemptive instance, so we have to use the GCloud command line tool, documented at https://cloud.google.com/sdk/gcloud/reference/compute/instance-templates/create#--image

gcloud compute instance-templates create jenkins-2019-05-18-instance-template --machine-type=n1-highmem-8 --network-interface=address=104.154.94.144 --preemptible --region=us-central1-c --disk=name=jenkins-2019-05-18-disk,boot=yes,auto-delete=no --tags=http-server,https-server

1. Make a managed instance group that keeps that template at one

Setup the firewall (for Ubuntu)

sudo ufw allow 22;
sudo ufw enable;
sudo ufw allow 8080/tcp;

There are no ufw commands for setting up the port forwards, so it must be done via configuraton files. Add the lines below to /etc/ufw/before.rules, before the filter section, right at the top of the file:

*nat
:PREROUTING ACCEPT [0:0]
-A PREROUTING -p tcp --dport 80 -j REDIRECT --to-port 8080
COMMIT

Then restart and enable ufw to start on boot: sudo ufw enable

sudo ufw status

from https://serverfault.com/questions/238563/can-i-use-ufw-to-setup-a-port-forward

Install Java 8

sudo apt install openjdk-8-jre

Install jenkins

Follow the Linux, Debian/Ubuntu instructions at https://jenkins.io/doc/book/installing/

I'm trying out updating Jenkins using apt instead of manually downloading the war image. I think it'll work, because the instructions directly add and use the jenkins apt repository.

Jenkins plugins

First time around, I installed a bunch of plugins. I was still learning. Unfortunately, lots of plugins also meant lots of security vulnerabilities, and lots of manual updating of our Jenkins installation. This time around, I'm trying to install as few plugins as possible. Here's what I've installed. The versions are only included as a way to help determine which plugin I mean, since the plugin namespace is a mess.

"GitHub" v1.29.4 Ansi Color

Account Info

Jenkins used to use [email protected] and github's acl2jenkins account to push changes. In 2019, I changed it such that it uses [email protected] and github's acl2buildserver account to push changes. It seemed better to generalize the name.

Kestrel SMTP server

mail.kestrel.edu, port 2525

/var/lib/jenkins/env.sh

It contained the following, but I suspect it needs to be changed to reference the acl2 build server instead

#!/bin/bash

export STARTJOB='bash'
git config --global user.email "[email protected]"
git config --global user.name "David L. Rager"

Installing CCL

sudo apt install make sudo apt install m4 sudo apt install gcc # for as tool, required to build lisp kernel

It's debatable where CCL should be installed. Since CCL's ccl.git/scripts/ccl64 file expects it to be installed into /usr/local/src/ccl, I put it there. Ideally you want to clone it into your home directory, so that it has all of "your" permissions, and then just mv the ccl directory to /usr/local/src. This way, when you rebuild ccl, you have permissions to do so.

git clone https://github.com/Clozure/ccl.git ccl
curl -L -O https://github.com/Clozure/ccl/releases/download/v1.12-dev.5/linuxx86.tar.gz
cd ccl
tar xf ../linuxx86.tar.gz

For good measure, rebuild ccl (there have been problems in the past when we don't rebuild the kernel. Though, those problems may not be a real concern anymore)

cd /usr/local/src/ccl/lisp-kernel/linuxx8664
make # make sure it finishes
cd ../..
./scripts/ccl64
(rebuild-ccl :full t)
(quit)
./scripts/ccl64
(rebuild-ccl :full t)
(quit)

Add the ccl to the path by putting a symlink to it in /usr/local/bin

cd /usr/local/bin
sudo ln -s /usr/local/src/ccl/scripts/ccl64 ccl

Install Glucose

sudo apt install g++
sudo apt install zlib1g-dev
wget https://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup-4.1.tgz # put it wherever you want
tar xzvf glucose-syrup-4.1.tgz
cd glucose-syrup-4.1/simp
make
cd ../..
sudo mv glucose-syrup-4.1 /usr/local/src
cd /usr/local/bin
ln -s /usr/local/src/glucose-syrup-4.1/simp/glucose glucose

Install Z3

Instructions are nicely documented at http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=SMT____Z3-INSTALLATION

sudo apt install unzip
cd ~/src/ # pick a place to unzip it
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04.zip
sudo mv z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04 /usr/local/src
cd /usr/local/bin
sudo ln -s /usr/local/src/z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04/bin/z3

Install SBCL

Making ACL2 work with SBCL requires some manual intervention. We use the version of SBCL that comes with ubuntu to bootstrap building the source code downloaded from sourceforge.

sudo apt install sbcl
cd ~/src
git clone git://git.code.sf.net/p/sbcl/sbcl
cd sbcl
sh make.sh --with-sb-thread --without-immobile-space --without-immobile-code --without-compact-instance-header
sudo apt remove sbcl sudo sh install.sh

I then had to create a wrapper for SBCL to call the sbcl core with a particular flag. The wrapper contained

#!/bin/sh
<sbcl-dir-path>/src/runtime/sbcl --core <sbcl-dir-path>/output/sbcl.core --dynamic-space-size 2000 "$@"

To do that, I moved sbcl to sbcl-exe, and then created the wrapper. The wrapper will probably need to be re-created any time that sbcl is upgraded and install.sh is called.

Also see http://www.cs.utexas.edu/users/moore/acl2/v8-2/HTML/installation/requirements.html#Obtaining-SBCL

Install GCL

The following should have worked, but even though it is verion 2.6.12, the compiled GCL isn't ansi-compliant by default: sudo apt install gcl

Instead I had to do:

git clone git://git.sv.gnu.org/gcl.git
cd gcl/gcl
git checkout Version_2_6_13pre
./configure --enable-ansi && make
make install # by default installs to /usr/local

Setup jenkins builds

Mimic the pdf that will hopefully be attached at some point

Setup Jenkins credentials

I tried using a personal access tokens, but it wanted me to setup the PAT to be used in a section of the Github plugin that talked about adding pre/post-receive hooks and other nonsense that I have no interest in giving jenkins the incentive to perform. As such, I decided to try just using an ssh key.

I ended up creating an ssh key+pair (on my laptop) for the github user [email protected]. The git repo needed an ssh:// in front of its name. I only needed to use the credential in the testing build, and the build that merges "master" commits into the "testing" branch.