setup instructions for sail server

setup.sh

# pseudo-setup script, obviously replace djenson with your id everywhere

# login; don't do any computation/data moving on the head node, you'll get cancelled
ssh [email protected]

# generate ssh keys (on sc head node)
# NOTE: just press enter and skip adding a password (it's fine)
# https://docs.github.com/en/authentication/connecting-to-github-with-ssh/generating-a-new-ssh-key-and-adding-it-to-the-ssh-agent
ssh-keygen -t ed25519 -C "[email protected]"
cat ~/.ssh/id_rsa.pub # copy output and add it on github: https://github.com/settings/keys

# start a process on a data node (you can do scq2)
srun --account=thrun --partition=thrun --nodelist scq1 --gres gpu:0 --cpus-per-task 16 --mem 30GB --pty bash

# change to a scratch directory and create a folder for yourself
cd /scr1/
mkdir djenson
cd djenson
git clone [email protected]:danjenson/CoqGym-GNN.git

# Install (run each command until it succeds)
cd CoqGym-GNN
opam init
opam switch create 4.07.1+flambda && eval $(opam env)
source install.sh
cd coq_projects && make && cd ..

# download data.tar.gz, sexp_cache.tar.gz, and projs_split.json here:
https://drive.google.com/drive/folders/149m_17VkYYkl0kdSB4AI8zodCuTmPaA6?usp=sharing

# Upload data from your local computer (note you'll have to be logged in elsewhere to be able to copy to scq1{2})
scp data.tar.gz [email protected]:/scr1/djenson/
scp sexp_cache.tar.gz [email protected]:/scr1/djenson/
scp projs_split.json [email protected]:/scr1/djenson/

# Download & upload our already extracted train.tgz and valid.tgz proofs:
https://drive.google.com/drive/u/0/folders/1ksvPJPH63JPNYOOX5uN4B410jR-Ydro8

# Upload the extracted proofs to the server
scp train.tgz [email protected]:/scr1/djenson/
scp valid.tgz [email protected]:/scr1/djenson/

# copy (DON'T MOVE) the data into the coq directory (if you need to nuke your Coq, you still have the data and can copy back in)
cd /scr1/djenson
cp data.tar.gz sexp_cache.tar.gz projs_split.json CoqGym-GNN/
mkdir CoqGym-GNN/ASTactic/proof_steps_gnn
cp train.tgz valid.tgz CoqGym-GNN/ASTactic/proof_steps_gnn/

# unzip data
python unzip_data.py

# extract our proofs
cd /scr1/djenson/CoqGym-GNN/ASTactic/proof_steps_gnn
tar xvzf train.tgz
tar xvzf valid.tgz

# setup python
curl https://pyenv.run | bash
pyenv install 3.7.1
cd /scr1/djenson/CoqGym-GNN
pyenv local 3.7.1
pip install numpy ipython lark-parser==0.6.5 lmdb==0.94 pandas==0.24.2 pexpect==4.6.0 sexpdata==0.0.3 progressbar2
pip install pyg_lib torch_scatter torch_sparse torch_cluster torch_spline_conv torch_geometric -f https://data.pyg.org/whl/torch-1.13.0+cu117.html

# validate installation (if this doesn't work, go back to install.sh)
python eval_env.py