From bca12ef1682a043ca98cec16c2d223261f821816 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Mon, 17 Oct 2022 20:54:00 -0400 Subject: [PATCH 01/25] Add install script for Avenir specifically for Ubuntu 20.04 --- install-avenir-ubuntu-20.04.sh | 49 ++++++++++++++++++++++++++++++++++ synthesis/README.md | 32 +++++++++++++++++++--- 2 files changed, 78 insertions(+), 3 deletions(-) create mode 100755 install-avenir-ubuntu-20.04.sh diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh new file mode 100755 index 00000000..d5fa444b --- /dev/null +++ b/install-avenir-ubuntu-20.04.sh @@ -0,0 +1,49 @@ +#! /bin/bash + +AVENIR_INSTALL_DIR="$HOME/forks/avenir" + +# Based on instructions found here: https://opam.ocaml.org/doc/Install.html + +sudo add-apt-repository ppa:avsm/ppa +sudo apt update +sudo apt install opam +opam --version + +# As of 2022-Oct-16 when I last ran this on an Ubuntu 20.04 system, +# this installed opam version 2.1.0 + +# The commands below are for +opam init +opam switch create . ocaml-base-compiler.4.09.0 +sudo apt-get install m4 +opam install merlin dune utop core ocamlformat +opam user-setup install +sudo apt-get install bubblewrap +opam install menhir + +# I tried 'sudo apt-get install z3' on Ubuntu 20.04 on 2022-Oct-16, +# but it install version 4.8.7 according to the output of `z3 +# --version`, which is older than the version 4.8.8 recommended by the +# Avenir README. + +# Download Z3 zip file +# unzip it +# maybe need to create a link from /usr/bin/z3 to where it is installed +INSTALL_DIR="$HOME/install/avenir" +Z3_INSTALL_DIR="$HOME/z3-4.8.17-x64-glibc-2.31/bin/z3" +sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 + +sudo apt-get install libgmp-dev +opam pin add z3 https://github.com/priyasrikumar/ocaml-z3.git + +# Install desired version of petr4 +cd ${INSTALL_DIR} +git clone https://github.com/cornell-netlab/petr4 +cd petr4 +git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 + +cd ${AVENIR_INSTALL_DIR}/synthesis +opam --yes install p4pp=0.1.4 +opam --yes pin add petr4 ${INSTALL_DIR}/petr4 + +dune external-lib-deps --missing @all diff --git a/synthesis/README.md b/synthesis/README.md index 242f898d..cf642ce5 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -24,10 +24,29 @@ opam install merlin dune utop core ocamlformat opam user-setup install ``` ++ [merlin](https://opam.ocaml.org/packages/merlin/) - Editor helper, + provides completion, typing and source browsing in Vim and Emacs ++ [dune](https://opam.ocaml.org/packages/dune/) - Fast, portable, and + opinionated build system + ++ [utop](https://opam.ocaml.org/packages/utop/) - utop is an improved + toplevel (i.e., Read-Eval-Print Loop or REPL) for OCaml. It can run + in a terminal or in Emacs. It supports line edition, history, + real-time and context sensitive completion, colors, and more. It + integrates with the Tuareg mode in Emacs. ++ [core](https://opam.ocaml.org/packages/core/) - Industrial strength + alternative to OCaml's standard library ++ [ocamlformat](https://opam.ocaml.org/packages/ocamlformat/) - + Auto-formatter for OCaml code + + + Install Menhir ++ [Menhir](https://opam.ocaml.org/packages/menhir/) is an LR(1) parser + generator. + ```bash -apt install bubblewrap +sudo apt-get install bubblewrap opam install menhir ``` @@ -48,6 +67,12 @@ opam pin add z3 https://github.com/priyasrikumar/ocaml-z3.git cd git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 ``` + +# TODO: What is the 'hybrid' directory mentioned here? +# There is no file named hybrid in the petr4 repo. +# There are several with that name in the avenir repo, but none that have a subdirectory named 'synthesis'. +# For now I will change to the avenir/synthesis directory, hoping that will work. + Then change back to the `hybrid/synthesis` directory. Install the version of the p4 preprocessor `p4pp` that works with this specific commit: ``` bash opam install p4pp=0.1.4 @@ -57,8 +82,9 @@ Then, pin the petr4 package to the local state. opam pin add petr4 ``` -+ Install any remaining dependencies (e.g. `async`) using `opam install` (e.g. - `opam install async`) that show up when you run the following command: ++ Install any remaining dependencies (e.g. `async`) using `opam + install` (e.g. `opam install async`) that show up when you run the + following command: ``` dune external-lib-deps --missing @all From af0d9f2fe1c248ffd5964002e37fdbb155a7ab58 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Mon, 17 Oct 2022 21:30:01 -0400 Subject: [PATCH 02/25] Update steps --- install-avenir-ubuntu-20.04.sh | 59 +++++++++++++++++++++++----------- 1 file changed, 41 insertions(+), 18 deletions(-) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index d5fa444b..ceec9f79 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -1,25 +1,28 @@ #! /bin/bash -AVENIR_INSTALL_DIR="$HOME/forks/avenir" +INSTALL_DIR=`pwd` # Based on instructions found here: https://opam.ocaml.org/doc/Install.html -sudo add-apt-repository ppa:avsm/ppa +sudo add-apt-repository --yes ppa:avsm/ppa sudo apt update -sudo apt install opam +sudo apt-get install --yes opam opam --version # As of 2022-Oct-16 when I last ran this on an Ubuntu 20.04 system, # this installed opam version 2.1.0 -# The commands below are for -opam init -opam switch create . ocaml-base-compiler.4.09.0 -sudo apt-get install m4 -opam install merlin dune utop core ocamlformat -opam user-setup install -sudo apt-get install bubblewrap -opam install menhir +# TODO: I have not yet tested 'opam --yes init' with the --yes option +# to see whether it avoids interactive prompting. Hopefully it does. +opam --yes init +eval $(opam env --switch=default) +opam --yes switch create . ocaml-base-compiler.4.09.0 +sudo apt-get install --yes m4 +opam --yes install merlin dune utop core ocamlformat +eval $(opam env) +opam --yes user-setup install +sudo apt-get install --yes bubblewrap +opam --yes install menhir # I tried 'sudo apt-get install z3' on Ubuntu 20.04 on 2022-Oct-16, # but it install version 4.8.7 according to the output of `z3 @@ -27,23 +30,43 @@ opam install menhir # Avenir README. # Download Z3 zip file +wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip # unzip it -# maybe need to create a link from /usr/bin/z3 to where it is installed -INSTALL_DIR="$HOME/install/avenir" -Z3_INSTALL_DIR="$HOME/z3-4.8.17-x64-glibc-2.31/bin/z3" +unzip -e z3-4.8.10-x64-ubuntu-18.04.zip +# create a link from /usr/bin/z3 to where it is installed +Z3_INSTALL_DIR="${INSTALL_DIR}/z3-4.8.10-x64-ubuntu-18.04" sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 -sudo apt-get install libgmp-dev -opam pin add z3 https://github.com/priyasrikumar/ocaml-z3.git +sudo apt-get install --yes libgmp-dev +opam --yes pin add z3 https://github.com/priyasrikumar/ocaml-z3.git # Install desired version of petr4 cd ${INSTALL_DIR} git clone https://github.com/cornell-netlab/petr4 cd petr4 git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 +PETR4_INSTALL_DIR=`pwd` -cd ${AVENIR_INSTALL_DIR}/synthesis +cd ${INSTALL_DIR} +git clone https://github.com/cornell-netlab/avenir +cd avenir +AVENIR_INSTALL_DIR=`pwd` + +cd synthesis opam --yes install p4pp=0.1.4 -opam --yes pin add petr4 ${INSTALL_DIR}/petr4 +# I experienced errors attempting to compile petr4 in the next step +opam --yes pin add petr4 ${PETR4_INSTALL_DIR} +# I got the following error message attempting the next command: +# dune external-lib-deps: This subcommand is no longer implemented. + +# This is the version of dune installed on my system: +# $ which dune +# /home/andy/install/_opam/bin/dune +# $ dune --version +# 3.4.1 dune external-lib-deps --missing @all + +# There are more commands to run from the synthesis/README.md file, +# but the errors above lead me to believe I am doing something wrong, +# or the steps in the README need updating. From 958793a3a07f20ee454e8f9cd3e0c29fb7200ee9 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Mon, 17 Oct 2022 21:35:05 -0400 Subject: [PATCH 03/25] Add 'set -x' for tracing of commands mingled with output --- install-avenir-ubuntu-20.04.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index ceec9f79..ff8a230b 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -1,5 +1,6 @@ #! /bin/bash +set -x INSTALL_DIR=`pwd` # Based on instructions found here: https://opam.ocaml.org/doc/Install.html From 1f90d0669567dbb44d1be56ffc1d3b59372ab854 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Mon, 17 Oct 2022 21:58:35 -0400 Subject: [PATCH 04/25] Try adding another eval $(opam env) command --- install-avenir-ubuntu-20.04.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index ff8a230b..4c0a347f 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -18,6 +18,7 @@ opam --version opam --yes init eval $(opam env --switch=default) opam --yes switch create . ocaml-base-compiler.4.09.0 +eval $(opam env) sudo apt-get install --yes m4 opam --yes install merlin dune utop core ocamlformat eval $(opam env) From 55a13148be0632d82a48f7ef6d73aa57fc396736 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 13:48:24 -0400 Subject: [PATCH 05/25] Attempt to use cstruct version 6.0.0 before pinning petr4 --- install-avenir-ubuntu-20.04.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index 4c0a347f..372926c2 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -56,6 +56,7 @@ AVENIR_INSTALL_DIR=`pwd` cd synthesis opam --yes install p4pp=0.1.4 +opam --yes install cstruct=6.0.0 # I experienced errors attempting to compile petr4 in the next step opam --yes pin add petr4 ${PETR4_INSTALL_DIR} From 6e14597c7e4213a1786c62136fe29abcfa734961 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 15:01:39 -0400 Subject: [PATCH 06/25] Updates to install script that get it further towards completion --- install-avenir-ubuntu-20.04.sh | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index 372926c2..ef1c1a1c 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -10,11 +10,9 @@ sudo apt update sudo apt-get install --yes opam opam --version -# As of 2022-Oct-16 when I last ran this on an Ubuntu 20.04 system, -# this installed opam version 2.1.0 +# As of 2022-Oct-16 when I last ran this on Ubuntu 18.04 and 20.04 +# systems, the commands above installed opam version 2.1.0 -# TODO: I have not yet tested 'opam --yes init' with the --yes option -# to see whether it avoids interactive prompting. Hopefully it does. opam --yes init eval $(opam env --switch=default) opam --yes switch create . ocaml-base-compiler.4.09.0 @@ -31,6 +29,9 @@ opam --yes install menhir # --version`, which is older than the version 4.8.8 recommended by the # Avenir README. +# Instead, install a pre-built version of z3 4.8.10 as distributed by +# the Z3 developers. + # Download Z3 zip file wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip # unzip it @@ -56,20 +57,19 @@ AVENIR_INSTALL_DIR=`pwd` cd synthesis opam --yes install p4pp=0.1.4 -opam --yes install cstruct=6.0.0 -# I experienced errors attempting to compile petr4 in the next step +opam --yes pin add cstruct 6.0.0 opam --yes pin add petr4 ${PETR4_INSTALL_DIR} # I got the following error message attempting the next command: # dune external-lib-deps: This subcommand is no longer implemented. -# This is the version of dune installed on my system: -# $ which dune -# /home/andy/install/_opam/bin/dune -# $ dune --version -# 3.4.1 -dune external-lib-deps --missing @all +# This error occured whiel running dune version 3.4.1. Apparently +# this 'extern-lib-deps' sub-command was removed in some version of +# dune since the Avenir install instructions were written, so skip +# this command. +# dune external-lib-deps --missing @all -# There are more commands to run from the synthesis/README.md file, -# but the errors above lead me to believe I am doing something wrong, -# or the steps in the README need updating. +# These should be the packages that need to be installed, according to +# the Avenir developers. +sudo apt-get install --yes pkt-config +opam --yes install async cohttp-async ipaddr shell From 89ba261c944266a3fd124869d4950c9178325d80 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 15:12:02 -0400 Subject: [PATCH 07/25] Add some checks for min RAM & disk space available, and supported OS versions --- install-avenir-ubuntu-20.04.sh | 105 +++++++++++++++++++++++++++++++-- 1 file changed, 101 insertions(+), 4 deletions(-) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index ef1c1a1c..f738b3da 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -1,9 +1,97 @@ #! /bin/bash +# Remember the current directory when the script was started: +INSTALL_DIR="${PWD}" + +THIS_SCRIPT_FILE_MAYBE_RELATIVE="$0" +THIS_SCRIPT_DIR_MAYBE_RELATIVE="${THIS_SCRIPT_FILE_MAYBE_RELATIVE%/*}" +THIS_SCRIPT_DIR_ABSOLUTE=`readlink -f "${THIS_SCRIPT_DIR_MAYBE_RELATIVE}"` + +ubuntu_version_warning() { + 1>&2 echo "This script has only been tested on these systems:" + 1>&2 echo " Ubuntu 18.04" + 1>&2 echo " Ubuntu 18.04 (TODO)" + 1>&2 echo "" + 1>&2 echo "Proceed installing manually at your own risk of" + 1>&2 echo "significant time spent figuring out how to make it all" + 1>&2 echo "work, or consider getting VirtualBox and creating an" + 1>&2 echo "Ubuntu virtual machine with one of the tested versions." +} + +abort_script=0 + +lsb_release >& /dev/null +if [ $? != 0 ] +then + 1>&2 echo "No 'lsb_release' found in your command path." + ubuntu_version_warning + exit 1 +fi + +distributor_id=`lsb_release -si` +ubuntu_release=`lsb_release -s -r` +if [ "${distributor_id}" = "Ubuntu" -a \( "${ubuntu_release}" = "18.04" -o "${ubuntu_release}" = "20.04" \) ] +then + echo "Found distributor '${distributor_id}' release '${ubuntu_release}'. Continuing with installation." +else + ubuntu_version_warning + 1>&2 echo "" + 1>&2 echo "Here is what command 'lsb_release -a' shows this OS to be:" + lsb_release -a + exit 1 +fi + +# Minimum required system memory is 2 GBytes, minus a few MBytes +# because from experiments I have run on several different Ubuntu +# Linux VMs, when you configure them with 2 Gbytes of RAM, the first +# line of /proc/meminfo shows a little less than that available, I +# believe because some memory occupied by the kernel is not shown. + +min_mem_MBytes=`expr 2 \* \( 1024 - 64 \)` +memtotal_KBytes=`head -n 1 /proc/meminfo | awk '{print $2;}'` +memtotal_MBytes=`expr ${memtotal_KBytes} / 1024` + +if [ "${memtotal_MBytes}" -lt "${min_mem_MBytes}" ] +then + memtotal_comment="too low" + abort_script=1 +else + memtotal_comment="enough" +fi + +echo "Minimum recommended memory to run this script: ${min_mem_MBytes} MBytes" +echo "Memory on this system from /proc/meminfo: ${memtotal_MBytes} MBytes -> $memtotal_comment" + +min_free_disk_MBytes=`expr 9 \* 1024` +free_disk_MBytes=`df --output=avail --block-size=1M . | tail -n 1` + +if [ "${free_disk_MBytes}" -lt "${min_free_disk_MBytes}" ] +then + free_disk_comment="too low" + abort_script=1 +else + free_disk_comment="enough" +fi + +echo "Minimum free disk space to run this script: ${min_free_disk_MBytes} MBytes" +echo "Free disk space on this system from df output: ${free_disk_MBytes} MBytes -> $free_disk_comment" + +if [ "${abort_script}" == 1 ] +then + echo "" + echo "Aborting script because system has too little RAM or free disk space" + exit 1 +fi + +echo "------------------------------------------------------------" +echo "Time and disk space used before installation begins:" set -x -INSTALL_DIR=`pwd` +date +df -h . +df -BM . -# Based on instructions found here: https://opam.ocaml.org/doc/Install.html +# This section for installing opam is based on instructions found +# here: https://opam.ocaml.org/doc/Install.html sudo add-apt-repository --yes ppa:avsm/ppa sudo apt update @@ -43,7 +131,7 @@ sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 sudo apt-get install --yes libgmp-dev opam --yes pin add z3 https://github.com/priyasrikumar/ocaml-z3.git -# Install desired version of petr4 +# Install recommended version of petr4 cd ${INSTALL_DIR} git clone https://github.com/cornell-netlab/petr4 cd petr4 @@ -53,7 +141,6 @@ PETR4_INSTALL_DIR=`pwd` cd ${INSTALL_DIR} git clone https://github.com/cornell-netlab/avenir cd avenir -AVENIR_INSTALL_DIR=`pwd` cd synthesis opam --yes install p4pp=0.1.4 @@ -73,3 +160,13 @@ opam --yes pin add petr4 ${PETR4_INSTALL_DIR} # the Avenir developers. sudo apt-get install --yes pkt-config opam --yes install async cohttp-async ipaddr shell + +make + +set +x +echo "------------------------------------------------------------" +echo "Time and disk space used when installation was complete:" +set -x +date +df -h . +df -BM . From 66dcd5ce675974cd09c1996ca15a662bc5e86b63 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 15:52:02 -0400 Subject: [PATCH 08/25] Reduce the check for required disk space to 5 GB --- install-avenir-ubuntu-20.04.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index f738b3da..95e1b65f 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -62,7 +62,7 @@ fi echo "Minimum recommended memory to run this script: ${min_mem_MBytes} MBytes" echo "Memory on this system from /proc/meminfo: ${memtotal_MBytes} MBytes -> $memtotal_comment" -min_free_disk_MBytes=`expr 9 \* 1024` +min_free_disk_MBytes=`expr 5 \* 1024` free_disk_MBytes=`df --output=avail --block-size=1M . | tail -n 1` if [ "${free_disk_MBytes}" -lt "${min_free_disk_MBytes}" ] From 93e20c619fdb0950fe404027133957a8f745ebcb Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:23:53 -0400 Subject: [PATCH 09/25] Correct Ubuntu package name in install script --- install-avenir-ubuntu-20.04.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh index 95e1b65f..2d4c835e 100755 --- a/install-avenir-ubuntu-20.04.sh +++ b/install-avenir-ubuntu-20.04.sh @@ -158,7 +158,7 @@ opam --yes pin add petr4 ${PETR4_INSTALL_DIR} # These should be the packages that need to be installed, according to # the Avenir developers. -sudo apt-get install --yes pkt-config +sudo apt-get install --yes pkg-config opam --yes install async cohttp-async ipaddr shell make From a3f6c3854ac221f42c9a54bd76a4592657ce82ae Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:24:10 -0400 Subject: [PATCH 10/25] Some corrections to install steps in README.md --- synthesis/README.md | 42 ++++++++---------------------------------- 1 file changed, 8 insertions(+), 34 deletions(-) diff --git a/synthesis/README.md b/synthesis/README.md index cf642ce5..aa6066e3 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -24,27 +24,8 @@ opam install merlin dune utop core ocamlformat opam user-setup install ``` -+ [merlin](https://opam.ocaml.org/packages/merlin/) - Editor helper, - provides completion, typing and source browsing in Vim and Emacs -+ [dune](https://opam.ocaml.org/packages/dune/) - Fast, portable, and - opinionated build system - -+ [utop](https://opam.ocaml.org/packages/utop/) - utop is an improved - toplevel (i.e., Read-Eval-Print Loop or REPL) for OCaml. It can run - in a terminal or in Emacs. It supports line edition, history, - real-time and context sensitive completion, colors, and more. It - integrates with the Tuareg mode in Emacs. -+ [core](https://opam.ocaml.org/packages/core/) - Industrial strength - alternative to OCaml's standard library -+ [ocamlformat](https://opam.ocaml.org/packages/ocamlformat/) - - Auto-formatter for OCaml code - - + Install Menhir -+ [Menhir](https://opam.ocaml.org/packages/menhir/) is an LR(1) parser - generator. - ```bash sudo apt-get install bubblewrap opam install menhir @@ -67,32 +48,23 @@ opam pin add z3 https://github.com/priyasrikumar/ocaml-z3.git cd git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 ``` - -# TODO: What is the 'hybrid' directory mentioned here? -# There is no file named hybrid in the petr4 repo. -# There are several with that name in the avenir repo, but none that have a subdirectory named 'synthesis'. -# For now I will change to the avenir/synthesis directory, hoping that will work. - -Then change back to the `hybrid/synthesis` directory. Install the version of the p4 preprocessor `p4pp` that works with this specific commit: +Then change back to the `avenir/synthesis` directory. Install the version of the p4 preprocessor `p4pp` that works with this specific commit: ``` bash opam install p4pp=0.1.4 +opam pin add cstruct 6.0.0 ``` Then, pin the petr4 package to the local state. ``` opam pin add petr4 ``` -+ Install any remaining dependencies (e.g. `async`) using `opam - install` (e.g. `opam install async`) that show up when you run the - following command: ++ Install the remaining dependencies with the commands below: ``` -dune external-lib-deps --missing @all +sudo apt-get install pkg-config +opam install async cohttp-async ipaddr shell ``` -The list of packages should be `async cohttp-async ipaddr shell`. If `z3`, -`petr4`, or `p4pp` show up here, repeat the previous steps untill they no longer appear when you run this command. If `menhir` appears in this list even when `opam` declares that it has been correctly installed, you may proceed. - + Run `make` to verify that `avenir` builds. + The makefile is currently a bit wonky, so for subsequent compilations, you may need to run `make rebuild` instead of `make build`. @@ -121,7 +93,8 @@ abstract insertions in `hello/inserts.csv`. To verify equivalence, run the following commands ``` cd hello -../avenir eq-real abstract.p4 target.p4 inserts.csv solution.csv fvs noassume -I1 includes -I2 includes +# TODO: The command below gives an error. What to use instead? +../avenir eq abstract.p4 target.p4 inserts.csv solution.csv fvs noassume -I1 includes -I2 includes ``` This will print the IR encoding of `abstract.p4` and `target.p4` followed by either `Equivalent`, or a counterexample. In this case you should see @@ -132,6 +105,7 @@ either `Equivalent`, or a counterexample. In this case you should see To synthesize the same insertions whose correctness we just verified, make sure you are still in the `hello` directory and run ``` +# TODO: The command below gives an error. What to use instead? ../avenir synth abstract.p4 target.p4 no_edits.csv no_edits.csv fvs -b 1000 -e 10 -data inserts.csv -I1 includes -I2 includes -P4 -p ``` You should again see the IR encoding of the pipeline programs, and then a line From bf1888ce95491dbecebeb846a3f5649c618403af Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:37:48 -0400 Subject: [PATCH 11/25] Correction to a sample command in README for hello example --- synthesis/README.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/synthesis/README.md b/synthesis/README.md index aa6066e3..fc91e62a 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -93,8 +93,7 @@ abstract insertions in `hello/inserts.csv`. To verify equivalence, run the following commands ``` cd hello -# TODO: The command below gives an error. What to use instead? -../avenir eq abstract.p4 target.p4 inserts.csv solution.csv fvs noassume -I1 includes -I2 includes +../avenir eq abstract.p4 target.p4 inserts.csv solution.csv fvs -I1 includes -I2 includes -P4 ``` This will print the IR encoding of `abstract.p4` and `target.p4` followed by either `Equivalent`, or a counterexample. In this case you should see From f4a7d8277a85b059949dc5c5cdf86a3c1c3568b2 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:40:42 -0400 Subject: [PATCH 12/25] Move and rename install script --- scripts/ubuntu-install.sh | 172 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100755 scripts/ubuntu-install.sh diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh new file mode 100755 index 00000000..2d4c835e --- /dev/null +++ b/scripts/ubuntu-install.sh @@ -0,0 +1,172 @@ +#! /bin/bash + +# Remember the current directory when the script was started: +INSTALL_DIR="${PWD}" + +THIS_SCRIPT_FILE_MAYBE_RELATIVE="$0" +THIS_SCRIPT_DIR_MAYBE_RELATIVE="${THIS_SCRIPT_FILE_MAYBE_RELATIVE%/*}" +THIS_SCRIPT_DIR_ABSOLUTE=`readlink -f "${THIS_SCRIPT_DIR_MAYBE_RELATIVE}"` + +ubuntu_version_warning() { + 1>&2 echo "This script has only been tested on these systems:" + 1>&2 echo " Ubuntu 18.04" + 1>&2 echo " Ubuntu 18.04 (TODO)" + 1>&2 echo "" + 1>&2 echo "Proceed installing manually at your own risk of" + 1>&2 echo "significant time spent figuring out how to make it all" + 1>&2 echo "work, or consider getting VirtualBox and creating an" + 1>&2 echo "Ubuntu virtual machine with one of the tested versions." +} + +abort_script=0 + +lsb_release >& /dev/null +if [ $? != 0 ] +then + 1>&2 echo "No 'lsb_release' found in your command path." + ubuntu_version_warning + exit 1 +fi + +distributor_id=`lsb_release -si` +ubuntu_release=`lsb_release -s -r` +if [ "${distributor_id}" = "Ubuntu" -a \( "${ubuntu_release}" = "18.04" -o "${ubuntu_release}" = "20.04" \) ] +then + echo "Found distributor '${distributor_id}' release '${ubuntu_release}'. Continuing with installation." +else + ubuntu_version_warning + 1>&2 echo "" + 1>&2 echo "Here is what command 'lsb_release -a' shows this OS to be:" + lsb_release -a + exit 1 +fi + +# Minimum required system memory is 2 GBytes, minus a few MBytes +# because from experiments I have run on several different Ubuntu +# Linux VMs, when you configure them with 2 Gbytes of RAM, the first +# line of /proc/meminfo shows a little less than that available, I +# believe because some memory occupied by the kernel is not shown. + +min_mem_MBytes=`expr 2 \* \( 1024 - 64 \)` +memtotal_KBytes=`head -n 1 /proc/meminfo | awk '{print $2;}'` +memtotal_MBytes=`expr ${memtotal_KBytes} / 1024` + +if [ "${memtotal_MBytes}" -lt "${min_mem_MBytes}" ] +then + memtotal_comment="too low" + abort_script=1 +else + memtotal_comment="enough" +fi + +echo "Minimum recommended memory to run this script: ${min_mem_MBytes} MBytes" +echo "Memory on this system from /proc/meminfo: ${memtotal_MBytes} MBytes -> $memtotal_comment" + +min_free_disk_MBytes=`expr 5 \* 1024` +free_disk_MBytes=`df --output=avail --block-size=1M . | tail -n 1` + +if [ "${free_disk_MBytes}" -lt "${min_free_disk_MBytes}" ] +then + free_disk_comment="too low" + abort_script=1 +else + free_disk_comment="enough" +fi + +echo "Minimum free disk space to run this script: ${min_free_disk_MBytes} MBytes" +echo "Free disk space on this system from df output: ${free_disk_MBytes} MBytes -> $free_disk_comment" + +if [ "${abort_script}" == 1 ] +then + echo "" + echo "Aborting script because system has too little RAM or free disk space" + exit 1 +fi + +echo "------------------------------------------------------------" +echo "Time and disk space used before installation begins:" +set -x +date +df -h . +df -BM . + +# This section for installing opam is based on instructions found +# here: https://opam.ocaml.org/doc/Install.html + +sudo add-apt-repository --yes ppa:avsm/ppa +sudo apt update +sudo apt-get install --yes opam +opam --version + +# As of 2022-Oct-16 when I last ran this on Ubuntu 18.04 and 20.04 +# systems, the commands above installed opam version 2.1.0 + +opam --yes init +eval $(opam env --switch=default) +opam --yes switch create . ocaml-base-compiler.4.09.0 +eval $(opam env) +sudo apt-get install --yes m4 +opam --yes install merlin dune utop core ocamlformat +eval $(opam env) +opam --yes user-setup install +sudo apt-get install --yes bubblewrap +opam --yes install menhir + +# I tried 'sudo apt-get install z3' on Ubuntu 20.04 on 2022-Oct-16, +# but it install version 4.8.7 according to the output of `z3 +# --version`, which is older than the version 4.8.8 recommended by the +# Avenir README. + +# Instead, install a pre-built version of z3 4.8.10 as distributed by +# the Z3 developers. + +# Download Z3 zip file +wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip +# unzip it +unzip -e z3-4.8.10-x64-ubuntu-18.04.zip +# create a link from /usr/bin/z3 to where it is installed +Z3_INSTALL_DIR="${INSTALL_DIR}/z3-4.8.10-x64-ubuntu-18.04" +sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 + +sudo apt-get install --yes libgmp-dev +opam --yes pin add z3 https://github.com/priyasrikumar/ocaml-z3.git + +# Install recommended version of petr4 +cd ${INSTALL_DIR} +git clone https://github.com/cornell-netlab/petr4 +cd petr4 +git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 +PETR4_INSTALL_DIR=`pwd` + +cd ${INSTALL_DIR} +git clone https://github.com/cornell-netlab/avenir +cd avenir + +cd synthesis +opam --yes install p4pp=0.1.4 +opam --yes pin add cstruct 6.0.0 +opam --yes pin add petr4 ${PETR4_INSTALL_DIR} + +# I got the following error message attempting the next command: +# dune external-lib-deps: This subcommand is no longer implemented. + +# This error occured whiel running dune version 3.4.1. Apparently +# this 'extern-lib-deps' sub-command was removed in some version of +# dune since the Avenir install instructions were written, so skip +# this command. +# dune external-lib-deps --missing @all + +# These should be the packages that need to be installed, according to +# the Avenir developers. +sudo apt-get install --yes pkg-config +opam --yes install async cohttp-async ipaddr shell + +make + +set +x +echo "------------------------------------------------------------" +echo "Time and disk space used when installation was complete:" +set -x +date +df -h . +df -BM . From 86fb0ffc9b717efa15a6d2493eec9fa417df965f Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:41:01 -0400 Subject: [PATCH 13/25] Delete old named install script --- install-avenir-ubuntu-20.04.sh | 172 --------------------------------- 1 file changed, 172 deletions(-) delete mode 100755 install-avenir-ubuntu-20.04.sh diff --git a/install-avenir-ubuntu-20.04.sh b/install-avenir-ubuntu-20.04.sh deleted file mode 100755 index 2d4c835e..00000000 --- a/install-avenir-ubuntu-20.04.sh +++ /dev/null @@ -1,172 +0,0 @@ -#! /bin/bash - -# Remember the current directory when the script was started: -INSTALL_DIR="${PWD}" - -THIS_SCRIPT_FILE_MAYBE_RELATIVE="$0" -THIS_SCRIPT_DIR_MAYBE_RELATIVE="${THIS_SCRIPT_FILE_MAYBE_RELATIVE%/*}" -THIS_SCRIPT_DIR_ABSOLUTE=`readlink -f "${THIS_SCRIPT_DIR_MAYBE_RELATIVE}"` - -ubuntu_version_warning() { - 1>&2 echo "This script has only been tested on these systems:" - 1>&2 echo " Ubuntu 18.04" - 1>&2 echo " Ubuntu 18.04 (TODO)" - 1>&2 echo "" - 1>&2 echo "Proceed installing manually at your own risk of" - 1>&2 echo "significant time spent figuring out how to make it all" - 1>&2 echo "work, or consider getting VirtualBox and creating an" - 1>&2 echo "Ubuntu virtual machine with one of the tested versions." -} - -abort_script=0 - -lsb_release >& /dev/null -if [ $? != 0 ] -then - 1>&2 echo "No 'lsb_release' found in your command path." - ubuntu_version_warning - exit 1 -fi - -distributor_id=`lsb_release -si` -ubuntu_release=`lsb_release -s -r` -if [ "${distributor_id}" = "Ubuntu" -a \( "${ubuntu_release}" = "18.04" -o "${ubuntu_release}" = "20.04" \) ] -then - echo "Found distributor '${distributor_id}' release '${ubuntu_release}'. Continuing with installation." -else - ubuntu_version_warning - 1>&2 echo "" - 1>&2 echo "Here is what command 'lsb_release -a' shows this OS to be:" - lsb_release -a - exit 1 -fi - -# Minimum required system memory is 2 GBytes, minus a few MBytes -# because from experiments I have run on several different Ubuntu -# Linux VMs, when you configure them with 2 Gbytes of RAM, the first -# line of /proc/meminfo shows a little less than that available, I -# believe because some memory occupied by the kernel is not shown. - -min_mem_MBytes=`expr 2 \* \( 1024 - 64 \)` -memtotal_KBytes=`head -n 1 /proc/meminfo | awk '{print $2;}'` -memtotal_MBytes=`expr ${memtotal_KBytes} / 1024` - -if [ "${memtotal_MBytes}" -lt "${min_mem_MBytes}" ] -then - memtotal_comment="too low" - abort_script=1 -else - memtotal_comment="enough" -fi - -echo "Minimum recommended memory to run this script: ${min_mem_MBytes} MBytes" -echo "Memory on this system from /proc/meminfo: ${memtotal_MBytes} MBytes -> $memtotal_comment" - -min_free_disk_MBytes=`expr 5 \* 1024` -free_disk_MBytes=`df --output=avail --block-size=1M . | tail -n 1` - -if [ "${free_disk_MBytes}" -lt "${min_free_disk_MBytes}" ] -then - free_disk_comment="too low" - abort_script=1 -else - free_disk_comment="enough" -fi - -echo "Minimum free disk space to run this script: ${min_free_disk_MBytes} MBytes" -echo "Free disk space on this system from df output: ${free_disk_MBytes} MBytes -> $free_disk_comment" - -if [ "${abort_script}" == 1 ] -then - echo "" - echo "Aborting script because system has too little RAM or free disk space" - exit 1 -fi - -echo "------------------------------------------------------------" -echo "Time and disk space used before installation begins:" -set -x -date -df -h . -df -BM . - -# This section for installing opam is based on instructions found -# here: https://opam.ocaml.org/doc/Install.html - -sudo add-apt-repository --yes ppa:avsm/ppa -sudo apt update -sudo apt-get install --yes opam -opam --version - -# As of 2022-Oct-16 when I last ran this on Ubuntu 18.04 and 20.04 -# systems, the commands above installed opam version 2.1.0 - -opam --yes init -eval $(opam env --switch=default) -opam --yes switch create . ocaml-base-compiler.4.09.0 -eval $(opam env) -sudo apt-get install --yes m4 -opam --yes install merlin dune utop core ocamlformat -eval $(opam env) -opam --yes user-setup install -sudo apt-get install --yes bubblewrap -opam --yes install menhir - -# I tried 'sudo apt-get install z3' on Ubuntu 20.04 on 2022-Oct-16, -# but it install version 4.8.7 according to the output of `z3 -# --version`, which is older than the version 4.8.8 recommended by the -# Avenir README. - -# Instead, install a pre-built version of z3 4.8.10 as distributed by -# the Z3 developers. - -# Download Z3 zip file -wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip -# unzip it -unzip -e z3-4.8.10-x64-ubuntu-18.04.zip -# create a link from /usr/bin/z3 to where it is installed -Z3_INSTALL_DIR="${INSTALL_DIR}/z3-4.8.10-x64-ubuntu-18.04" -sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 - -sudo apt-get install --yes libgmp-dev -opam --yes pin add z3 https://github.com/priyasrikumar/ocaml-z3.git - -# Install recommended version of petr4 -cd ${INSTALL_DIR} -git clone https://github.com/cornell-netlab/petr4 -cd petr4 -git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 -PETR4_INSTALL_DIR=`pwd` - -cd ${INSTALL_DIR} -git clone https://github.com/cornell-netlab/avenir -cd avenir - -cd synthesis -opam --yes install p4pp=0.1.4 -opam --yes pin add cstruct 6.0.0 -opam --yes pin add petr4 ${PETR4_INSTALL_DIR} - -# I got the following error message attempting the next command: -# dune external-lib-deps: This subcommand is no longer implemented. - -# This error occured whiel running dune version 3.4.1. Apparently -# this 'extern-lib-deps' sub-command was removed in some version of -# dune since the Avenir install instructions were written, so skip -# this command. -# dune external-lib-deps --missing @all - -# These should be the packages that need to be installed, according to -# the Avenir developers. -sudo apt-get install --yes pkg-config -opam --yes install async cohttp-async ipaddr shell - -make - -set +x -echo "------------------------------------------------------------" -echo "Time and disk space used when installation was complete:" -set -x -date -df -h . -df -BM . From fac7e6f394df990a123249ac3ac5a42ff5283bcc Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:48:48 -0400 Subject: [PATCH 14/25] Change the install script to use the copy of the repo that it is within --- scripts/ubuntu-install.sh | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 2d4c835e..ed803333 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -138,11 +138,7 @@ cd petr4 git checkout cd556c1e2c20ccbd5b959f385cecebc43f5cfd72 PETR4_INSTALL_DIR=`pwd` -cd ${INSTALL_DIR} -git clone https://github.com/cornell-netlab/avenir -cd avenir - -cd synthesis +cd ${THIS_SCRIPT_DIR_ABSOLUTE}/../synthesis opam --yes install p4pp=0.1.4 opam --yes pin add cstruct 6.0.0 opam --yes pin add petr4 ${PETR4_INSTALL_DIR} From 9a824f5108b3d7ee9e84a72dcaeaa0a910a1377b Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 20:49:11 -0400 Subject: [PATCH 15/25] Mention the ubuntu-install.sh script in the README --- synthesis/README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/synthesis/README.md b/synthesis/README.md index fc91e62a..02be9bcc 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -1,5 +1,7 @@ # Getting Started +If you wish to automate these install steps on a freshly installed Ubuntu 18.04 or 20.04 system, run the script `./scripts/ubuntu-install.sh`. In whatever directory your shell is when you execute this script, it will create directories named `_opam`, `petr4`, one whose name begins with `z3-`. You may then skip down to the section [Running the code](#running-the-code). + + First, [install](https://opam.ocaml.org/doc/Install.html) OPAM version >2.0.4. If you already have OPAM >2.0.4 installed you can skip this step. If you have an earlier version of OPAM, upgrade it. + In the `synthesis` directory, run @@ -135,7 +137,7 @@ the retargeting experiment and the BMV2 simple-switch demonstration. ## Prerequisite software -The following packaged are required to run these evaluations: +The following packages are required to run these evaluations: - python2.7 - python-tk (via `apt`) - matplotlib (via `pip`) From 9f85c8b7f573d0cb402b5625e2f02fe7e1b16629 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 21:25:18 -0400 Subject: [PATCH 16/25] Update disk space required The disk space used at the end of the script's completion is less than this, but during some of the builds of OCaml programs, there is temporarily more disk space used, before it goes down at the end. --- scripts/ubuntu-install.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index ed803333..1407a2b0 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -62,7 +62,7 @@ fi echo "Minimum recommended memory to run this script: ${min_mem_MBytes} MBytes" echo "Memory on this system from /proc/meminfo: ${memtotal_MBytes} MBytes -> $memtotal_comment" -min_free_disk_MBytes=`expr 5 \* 1024` +min_free_disk_MBytes=`expr 8 \* 1024` free_disk_MBytes=`df --output=avail --block-size=1M . | tail -n 1` if [ "${free_disk_MBytes}" -lt "${min_free_disk_MBytes}" ] From 93ba0fb7f3d2e98f3eac1198cb15ba4985850486 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 21:26:17 -0400 Subject: [PATCH 17/25] Attempt to make the instructions clearer --- synthesis/README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/synthesis/README.md b/synthesis/README.md index 02be9bcc..1eecb473 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -1,6 +1,12 @@ # Getting Started -If you wish to automate these install steps on a freshly installed Ubuntu 18.04 or 20.04 system, run the script `./scripts/ubuntu-install.sh`. In whatever directory your shell is when you execute this script, it will create directories named `_opam`, `petr4`, one whose name begins with `z3-`. You may then skip down to the section [Running the code](#running-the-code). +If you wish to automate these install steps on a freshly installed Ubuntu 18.04 or 20.04 system, run the script `avenir/scripts/ubuntu-install.sh`. Running this script will create several directories in your current directory from which you execute the script, with the following names: + ++ `_opam` ++ `petr4` ++ one whose name begins with `z3-` and includes a version number + +After the install script completes, you may then skip down to the section [Verification](#verification). + First, [install](https://opam.ocaml.org/doc/Install.html) OPAM version >2.0.4. If you already have OPAM >2.0.4 installed you can skip this step. If you have an earlier version of OPAM, upgrade it. From b3fe94b526cfc47473d9c4c7db66d2d7da29c131 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Tue, 18 Oct 2022 23:48:57 -0400 Subject: [PATCH 18/25] Add debug for when output of 'opam env' changes --- scripts/ubuntu-install.sh | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 1407a2b0..95aa9cac 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -102,11 +102,14 @@ opam --version # systems, the commands above installed opam version 2.1.0 opam --yes init +opam env --switch=default > opam-env-1.txt eval $(opam env --switch=default) opam --yes switch create . ocaml-base-compiler.4.09.0 +opam env > opam-env-2.txt eval $(opam env) sudo apt-get install --yes m4 opam --yes install merlin dune utop core ocamlformat +opam env > opam-env-3.txt eval $(opam env) opam --yes user-setup install sudo apt-get install --yes bubblewrap @@ -140,8 +143,14 @@ PETR4_INSTALL_DIR=`pwd` cd ${THIS_SCRIPT_DIR_ABSOLUTE}/../synthesis opam --yes install p4pp=0.1.4 +opam env > opam-env-4.txt +eval $(opam env) opam --yes pin add cstruct 6.0.0 +opam env > opam-env-5.txt +eval $(opam env) opam --yes pin add petr4 ${PETR4_INSTALL_DIR} +opam env > opam-env-6.txt +eval $(opam env) # I got the following error message attempting the next command: # dune external-lib-deps: This subcommand is no longer implemented. @@ -156,6 +165,8 @@ opam --yes pin add petr4 ${PETR4_INSTALL_DIR} # the Avenir developers. sudo apt-get install --yes pkg-config opam --yes install async cohttp-async ipaddr shell +opam env > opam-env-7.txt +eval $(opam env) make From b912c98938028ac209cf89690c9a5959d20e0244 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Wed, 19 Oct 2022 00:32:23 -0400 Subject: [PATCH 19/25] Put all opam env debug output files in the same directory --- scripts/ubuntu-install.sh | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 95aa9cac..3d4c094a 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -3,6 +3,9 @@ # Remember the current directory when the script was started: INSTALL_DIR="${PWD}" +OPAMENV="${INSTALL_DIR}/opam-env" +mkdir -p ${OPAMENV} + THIS_SCRIPT_FILE_MAYBE_RELATIVE="$0" THIS_SCRIPT_DIR_MAYBE_RELATIVE="${THIS_SCRIPT_FILE_MAYBE_RELATIVE%/*}" THIS_SCRIPT_DIR_ABSOLUTE=`readlink -f "${THIS_SCRIPT_DIR_MAYBE_RELATIVE}"` @@ -102,14 +105,14 @@ opam --version # systems, the commands above installed opam version 2.1.0 opam --yes init -opam env --switch=default > opam-env-1.txt +opam env --switch=default > ${OPAMENV}/opam-env-1.txt eval $(opam env --switch=default) opam --yes switch create . ocaml-base-compiler.4.09.0 -opam env > opam-env-2.txt +opam env > ${OPAMENV}/opam-env-2.txt eval $(opam env) sudo apt-get install --yes m4 opam --yes install merlin dune utop core ocamlformat -opam env > opam-env-3.txt +opam env > ${OPAMENV}/opam-env-3.txt eval $(opam env) opam --yes user-setup install sudo apt-get install --yes bubblewrap @@ -143,13 +146,13 @@ PETR4_INSTALL_DIR=`pwd` cd ${THIS_SCRIPT_DIR_ABSOLUTE}/../synthesis opam --yes install p4pp=0.1.4 -opam env > opam-env-4.txt +opam env > ${OPAMENV}/opam-env-4.txt eval $(opam env) opam --yes pin add cstruct 6.0.0 -opam env > opam-env-5.txt +opam env > ${OPAMENV}/opam-env-5.txt eval $(opam env) opam --yes pin add petr4 ${PETR4_INSTALL_DIR} -opam env > opam-env-6.txt +opam env > ${OPAMENV}/opam-env-6.txt eval $(opam env) # I got the following error message attempting the next command: @@ -165,7 +168,7 @@ eval $(opam env) # the Avenir developers. sudo apt-get install --yes pkg-config opam --yes install async cohttp-async ipaddr shell -opam env > opam-env-7.txt +opam env > ${OPAMENV}/opam-env-7.txt eval $(opam env) make From 3fef24aaaecb17f3dfaef04069eecde75664ca45 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Wed, 19 Oct 2022 13:10:58 -0400 Subject: [PATCH 20/25] Force location of _opam directory relative to avenir directory in install script --- scripts/ubuntu-install.sh | 38 +++++++++++++++++++++++++++++++------- 1 file changed, 31 insertions(+), 7 deletions(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 3d4c094a..96d23d6e 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -1,19 +1,24 @@ #! /bin/bash -# Remember the current directory when the script was started: -INSTALL_DIR="${PWD}" - -OPAMENV="${INSTALL_DIR}/opam-env" -mkdir -p ${OPAMENV} - THIS_SCRIPT_FILE_MAYBE_RELATIVE="$0" THIS_SCRIPT_DIR_MAYBE_RELATIVE="${THIS_SCRIPT_FILE_MAYBE_RELATIVE%/*}" THIS_SCRIPT_DIR_ABSOLUTE=`readlink -f "${THIS_SCRIPT_DIR_MAYBE_RELATIVE}"` +# Install the new directories as siblings of the avenir repo directory. +# I believe that the _opam directory created during installation must be +# in a directory that is somewhere above the avenir/synthesis directory, +# otherwise Ocaml builds will use the ~/.opam directory contents, which +# are not the desired version of the OCaml compiler. +cd ${THIS_SCRIPT_DIR_ABSOLUTE}/../.. +INSTALL_DIR="${PWD}" + +OPAMENV="${INSTALL_DIR}/avenir-install-details" +mkdir -p ${OPAMENV} + ubuntu_version_warning() { 1>&2 echo "This script has only been tested on these systems:" 1>&2 echo " Ubuntu 18.04" - 1>&2 echo " Ubuntu 18.04 (TODO)" + 1>&2 echo " Ubuntu 20.04 (TODO)" 1>&2 echo "" 1>&2 echo "Proceed installing manually at your own risk of" 1>&2 echo "significant time spent figuring out how to make it all" @@ -86,6 +91,25 @@ then exit 1 fi +Z3_DIR_NAME="z3-4.8.10-x64-ubuntu-18.04" + +1>&2 echo "" +1>&2 echo "Install directory: ${INSTALL_DIR}" +1>&2 echo "" +1>&2 echo "Inside that directory, this script will create new directories" +1>&2 echo "with these names:" +1>&2 echo " _opam" +1>&2 echo " petr4" +1>&2 echo " ${Z3_DIR_NAME}" + +if [ -e "_opam" -o -e "peter4" -o -e ${Z3_DIR_NAME} ] +then + 1>&2 echo "" + 1>&2 echo "One or more files with those names already exist." + 1>&2 echo "Remove or rename them, then try this script again." + exit 1 +fi + echo "------------------------------------------------------------" echo "Time and disk space used before installation begins:" set -x From 55247fe52c732329cd1dd3f0232b6a77142f1465 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Wed, 19 Oct 2022 15:20:55 -0400 Subject: [PATCH 21/25] Simplify README description of install script because many of the details are now printed by the install script itself. --- synthesis/README.md | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/synthesis/README.md b/synthesis/README.md index 245e9da1..8f5bab18 100644 --- a/synthesis/README.md +++ b/synthesis/README.md @@ -1,12 +1,6 @@ # Getting Started -If you wish to automate these install steps on a freshly installed Ubuntu 18.04 or 20.04 system, run the script `avenir/scripts/ubuntu-install.sh`. Running this script will create several directories in your current directory from which you execute the script, with the following names: - -+ `_opam` -+ `petr4` -+ one whose name begins with `z3-` and includes a version number - -After the install script completes, you may then skip down to the section [Verification](#verification). +If you wish to automate these install steps on a freshly installed Ubuntu 18.04 or 20.04 system, run the script `avenir/scripts/ubuntu-install.sh`. After the install script completes, you may then skip down to the section [Verification](#verification). + First, [install](https://opam.ocaml.org/doc/Install.html) OPAM version >2.0.4. If you already have OPAM >2.0.4 installed you can skip this step. If you have an earlier version of OPAM, upgrade it. From c5df50f08b5ac243caaf8324b3ae2551c782b228 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Wed, 19 Oct 2022 21:13:28 -0400 Subject: [PATCH 22/25] Change version of z3 installed by script from 4.8.10 to 4.8.8 Apparently 4.8.10 is different enough that it causes some problems when interacting with Avenir. --- scripts/ubuntu-install.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 96d23d6e..fc7d9104 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -91,7 +91,7 @@ then exit 1 fi -Z3_DIR_NAME="z3-4.8.10-x64-ubuntu-18.04" +Z3_DIR_NAME="z3-4.8.8-x64-ubuntu-16.04" 1>&2 echo "" 1>&2 echo "Install directory: ${INSTALL_DIR}" @@ -147,15 +147,15 @@ opam --yes install menhir # --version`, which is older than the version 4.8.8 recommended by the # Avenir README. -# Instead, install a pre-built version of z3 4.8.10 as distributed by +# Instead, install a pre-built version of z3 4.8.8 as distributed by # the Z3 developers. # Download Z3 zip file -wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip +wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip # unzip it -unzip -e z3-4.8.10-x64-ubuntu-18.04.zip +unzip -e z3-4.8.8-x64-ubuntu-16.04.zip # create a link from /usr/bin/z3 to where it is installed -Z3_INSTALL_DIR="${INSTALL_DIR}/z3-4.8.10-x64-ubuntu-18.04" +Z3_INSTALL_DIR="${INSTALL_DIR}/z3-4.8.8-x64-ubuntu-16.04" sudo ln ${Z3_INSTALL_DIR}/bin/z3 /usr/bin/z3 sudo apt-get install --yes libgmp-dev From a694f52a32d28ba9527a9c11dfc01f4605412382 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Thu, 20 Oct 2022 00:31:30 -0400 Subject: [PATCH 23/25] Add 'sudo ldconfig' just before make Seems to be needed for 'make' to succeed on Ubuntu 20.04 --- scripts/ubuntu-install.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index fc7d9104..1cee39a3 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -194,6 +194,7 @@ sudo apt-get install --yes pkg-config opam --yes install async cohttp-async ipaddr shell opam env > ${OPAMENV}/opam-env-7.txt eval $(opam env) +sudo ldconfig make From 1f5c349236b57148bf197315467cee7366c1ce00 Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Thu, 20 Oct 2022 01:21:36 -0400 Subject: [PATCH 24/25] Add g++ package installation This seems to help building avenir on Ubuntu 20.04 systems --- scripts/ubuntu-install.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 1cee39a3..12276653 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -190,7 +190,7 @@ eval $(opam env) # These should be the packages that need to be installed, according to # the Avenir developers. -sudo apt-get install --yes pkg-config +sudo apt-get install --yes pkg-config g++ opam --yes install async cohttp-async ipaddr shell opam env > ${OPAMENV}/opam-env-7.txt eval $(opam env) From 390ddbf75ce534be61318f18caf1e90346a6f7be Mon Sep 17 00:00:00 2001 From: Andy Fingerhut Date: Thu, 20 Oct 2022 10:22:02 -0400 Subject: [PATCH 25/25] Now tested successfully with Ubuntu 20.04 and 22.04 --- scripts/ubuntu-install.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/ubuntu-install.sh b/scripts/ubuntu-install.sh index 12276653..07bf8659 100755 --- a/scripts/ubuntu-install.sh +++ b/scripts/ubuntu-install.sh @@ -18,7 +18,8 @@ mkdir -p ${OPAMENV} ubuntu_version_warning() { 1>&2 echo "This script has only been tested on these systems:" 1>&2 echo " Ubuntu 18.04" - 1>&2 echo " Ubuntu 20.04 (TODO)" + 1>&2 echo " Ubuntu 20.04" + 1>&2 echo " Ubuntu 22.04" 1>&2 echo "" 1>&2 echo "Proceed installing manually at your own risk of" 1>&2 echo "significant time spent figuring out how to make it all" @@ -38,7 +39,7 @@ fi distributor_id=`lsb_release -si` ubuntu_release=`lsb_release -s -r` -if [ "${distributor_id}" = "Ubuntu" -a \( "${ubuntu_release}" = "18.04" -o "${ubuntu_release}" = "20.04" \) ] +if [ "${distributor_id}" = "Ubuntu" -a \( "${ubuntu_release}" = "18.04" -o "${ubuntu_release}" = "20.04" -o "${ubuntu_release}" = "22.04" \) ] then echo "Found distributor '${distributor_id}' release '${ubuntu_release}'. Continuing with installation." else