TestSetup.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "c7c9dc74",
   "metadata": {},
   "outputs": [],
   "source": [
    "from preprocess import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a86c01b8",
   "metadata": {},
   "source": [
    "# VerCors\n",
    "VerCors is installed it in the shared folder in the VM. However, we made a symlink towards `/vercors`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "33e54199",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[34m[build.sc] [1/52] scriptSources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [3/52] cliImports \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [15/52] compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [16/52] enclosingClasspath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [20/52] resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [23/52] mill.scalalib.ZincWorkerModule.zincLogDebug \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [24/52] mill.scalalib.ZincWorkerModule.worker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [26/52] sources.super.mill.scalalib.JavaModule.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [47/52] zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[3/654] vercors.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[6/654] mill.scalalib.ZincWorkerModule.zincLogDebug \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[7/654] mill.scalalib.ZincWorkerModule.worker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[11/654] hre.pprofProto.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[13/654] mill.contrib.scalapblib.ScalaPBWorkerApi.scalaPBWorker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[17/654] hre.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[25/654] hre.pprofProto.scalaPBIncludePath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[45/654] hre.pprofProto.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[57/654] hre.pprofProto.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[75/654] hre.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[76/654] foreign-modules.project.fetchJars.z3.classPath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[88/654] hre.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[93/654] foreign-modules.project.colMeta.proto.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[97/654] foreign-modules.project.colMeta.meta.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[101/654] foreign-modules.project.colMeta.meta.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[117/654] foreign-modules.project.colMeta.meta.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[129/654] foreign-modules.project.colMeta.meta.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[139/654] foreign-modules.project.colMeta.meta.nodeDefinitions \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[141/654] foreign-modules.project.colMeta.meta.protobuf \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[149/654] foreign-modules.project.colMeta.proto.scalaPBIncludePath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[169/654] foreign-modules.project.colMeta.proto.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[181/654] foreign-modules.project.colMeta.proto.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[185/654] col.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[186/654] foreign-modules.project.colMeta.meta.helpers \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[202/654] col.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[214/654] col.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[219/654] rewrite.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[235/654] rewrite.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[247/654] rewrite.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[252/654] parsers.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[254/654] foreign-modules.project.fetchJars.antlr.classPath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[255/654] foreign-modules.project.antlr.c.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[256/654] foreign-modules.project.antlr.c.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[257/654] foreign-modules.project.antlr.c.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[260/654] foreign-modules.project.antlr.cpp.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[261/654] foreign-modules.project.antlr.cpp.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[262/654] foreign-modules.project.antlr.cpp.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[265/654] foreign-modules.project.antlr.java.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[266/654] foreign-modules.project.antlr.java.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[267/654] foreign-modules.project.antlr.java.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[270/654] foreign-modules.project.antlr.pvl.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[271/654] foreign-modules.project.antlr.pvl.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[272/654] foreign-modules.project.antlr.pvl.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[275/654] foreign-modules.project.antlr.llvm.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[276/654] foreign-modules.project.antlr.llvm.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[277/654] foreign-modules.project.antlr.llvm.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[279/654] parsers.generatedSources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[294/654] parsers.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[306/654] parsers.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[314/654] foreign-modules.project.viper.viper.silver.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[329/654] foreign-modules.project.viper.viper.silver.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[341/654] foreign-modules.project.viper.viper.silver.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[348/654] foreign-modules.project.viper.viper.silicon.common.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[363/654] foreign-modules.project.viper.viper.silicon.common.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[375/654] foreign-modules.project.viper.viper.silicon.common.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[379/654] foreign-modules.project.viper.viper.silicon.buildInfo.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[398/654] foreign-modules.project.viper.viper.silicon.buildInfo.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[410/654] foreign-modules.project.viper.viper.silicon.buildInfo.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[413/654] foreign-modules.project.viper.viper.silicon.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[428/654] foreign-modules.project.viper.viper.silicon.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[440/654] foreign-modules.project.viper.viper.silicon.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[446/654] foreign-modules.project.viper.viper.carbon.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[461/654] foreign-modules.project.viper.viper.carbon.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[473/654] foreign-modules.project.viper.viper.carbon.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[476/654] foreign-modules.project.viper.viper.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[491/654] foreign-modules.project.viper.viper.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[503/654] foreign-modules.project.viper.viper.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[507/654] viperApi.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[523/654] viperApi.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[535/654] viperApi.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[539/654] vercors.buildInfo.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[559/654] vercors.buildInfo.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[571/654] vercors.buildInfo.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[575/654] vercors.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[591/654] vercors.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[603/654] vercors.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[606/654] hre.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[608/654] hre.pprofProto.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[610/654] col.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[612/654] foreign-modules.project.colMeta.proto.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[614/654] rewrite.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[616/654] parsers.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[618/654] viperApi.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[620/654] foreign-modules.project.viper.viper.silver.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[622/654] foreign-modules.project.viper.viper.carbon.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[624/654] foreign-modules.project.viper.viper.silicon.buildInfo.resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[626/654] foreign-modules.project.viper.viper.silicon.buildInfo.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[628/654] foreign-modules.project.viper.viper.silicon.common.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[630/654] foreign-modules.project.viper.viper.silicon.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[632/654] foreign-modules.project.viper.viper.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[634/654] vercors.buildInfo.resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[636/654] vercors.buildInfo.resources \u001b[39m\n",
      "VerCors 2.0.0\n",
      "Usage: VerCors [options] [<path>...]\n",
      "\n",
      "  -h, --help               Prints this usage text\n",
      "  --help-hidden            Show hidden options (intended for VerCors experts, proceed with caution!)\n",
      "  --version                Prints version and build information\n",
      "  --help-passes            Lists the pass keys available for options that take a pass key.\n",
      "  -q, --quiet              Instruct VerCors to only log errors.\n",
      "  -v, --verbose            Instruct VerCors to output debug information\n",
      "  -p, --progress           Print progress information, even if stdout is not a tty.\n",
      "  --profile                Output profiling information in the current directory in the pprof format (https://github.com/google/pprof)\n",
      "\n",
      "Verification Mode\n",
      "  --verify                 Enable verification mode: instruct VerCors to verify the given files (default)\n",
      "  -m, --more               Always print the maximum amount of information about errors.\n",
      "  --table                  Always information about errors in table format.\n",
      "  --lang {cpp|silver|pvl|llvm|ipp|i|java|c|systemc}\n",
      "                           Do not detect the language from the file extension, but force a specific language parser for all files\n",
      "  --backend {silicon|carbon}\n",
      "                           Set the backend to verify with (default: silicon)\n",
      "  --backend-file-base <path>\n",
      "                           In addition to verification, output the resulting ASTs for the backend to files, appended with -<number>.<extension>\n",
      "  --backend-debug          Instruct the backend to print as much debugging information as possible\n",
      "  --output-after-pass:<pass>=<path>\n",
      "                           Print the AST after a pass key\n",
      "  --output-before-pass:<pass>=<path>\n",
      "                           Print the AST before a pass key\n",
      "  --backend-option <value>\n",
      "                           Provide custom flags to Viper\n",
      "  --skip-backend           Stop VerCors successfully before the backend is used to verify the program\n",
      "  --skip-translation       Stop VerCors successfully immediately after the file is parsed and resolved, and do no further processing\n",
      "  --skip-translation-after <pass>\n",
      "                           Stop VerCors successfully after executing the transformation pass with the supplied key\n",
      "  --skip-pass <pass>       Skip the passes that have the supplied keys\n",
      "  --silicon-print-quantifier-stats <amount>\n",
      "                           Print quantifier instantiation statistics from Z3 via silicon, every <amount> instantiations, every 5 seconds. Implies --dev-silicon-num-verifiers 1\n",
      "  --silicon-quiet          Disable various diagnostics of the silicon backend.\n",
      "  --bip-report-file <path>\n",
      "                           Write JavaBIP verification report to file, or standard out if \"-\" is used\n",
      "  --no-infer-heap-context-into-frame\n",
      "                           Disables smart inference of contextual heap into frame statements using `forperm`\n",
      "  --c-define <macro>=<defn>,...\n",
      "                           Pass -D options to the C preprocessor\n",
      "  --paths-simplify <simplify.pvl>,...\n",
      "                           Specify a chain of files to use that contain axiomatic simplification rules\n",
      "  --paths-simplify-after-relations <simplify.pvl>,...\n",
      "                           Specify a chain of files to use the contain axiomatic simplification rules, which will be applied after quantified integer relations are simplified\n",
      "  --path-adt <path>        Use a custom directory that contains definitions for all internal types encoded as axiomatic datatypes (array, option, any, etc.)\n",
      "  --path-cc <path>         Set the C compiler to use for preprocessing\n",
      "  --path-c-system <path>   Set the include path for system headers (-isystem)\n",
      "  --no-std-class-path      Remove the @jre (the default path to specified classes in the java runtime) and @source (the sources root computed via the package entry of submitted sources) entry\n",
      "  --class-path <path>|@jre|@source\n",
      "                           Add an entry to the sources class path\n",
      "  --path-z3 <path>         Set the location of the z3 binary\n",
      "  --path-boogie <path>     Set the location of the boogie binary\n",
      "  --path-c-preprocessor <path>\n",
      "                           Set the location of the C preprocessor binary\n",
      "\n",
      "VeyMont Mode\n",
      "  --veymont                Enable VeyMont mode: decompose the global program from the input files into several local programs that can be executed in parallel\n",
      "  --veymont-output <path>\n",
      "\n",
      "VeSUV Mode\n",
      "  --vesuv                  Enable VeSUV mode: transform SystemC designs to PVL to be deductively verified\n",
      "  --vesuv-output <path>\n",
      "\n",
      "Batch Testing Mode\n",
      "  --test                   Enable batch testing mode: execute all tests in a directory\n",
      "  --test-dir <path>        The directory from which to run all tests\n",
      "  --test-filter-backend <backend>,...\n",
      "  --test-filter-include-suite <suite>,...\n",
      "  --test-filter-exclude-suite <suite>,...\n",
      "  --test-workers <value>   Number of threads to start to run tests (default: 1)\n",
      "  --test-coverage          Generate a coverage report\n",
      "  --test-failing-first     When run twice with this option, VerCors will run the tests that failed the previous time first (cancelling a run is safe)\n",
      "  --test-generate-failing-run-configs\n",
      "                           Generates Intellij IDEA run configurations for tests that fail (and deletes recovered tests, cancelling a run is safe)\n",
      "  --test-ci-output         Tailor the logging output for a CI run\n",
      "\n",
      "\n",
      "  <path>...                List of input files to process\n"
     ]
    }
   ],
   "source": [
    "!/vercors/vct --help"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "309d0e4d",
   "metadata": {},
   "source": [
    "# Halide & Haliver\n",
    "We build and installed in HaliVer/Halide in `\\haliver`.\n",
    "Let's see if we can write an Halide program and compile it"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "5b13014c",
   "metadata": {},
   "outputs": [],
   "source": [
    "halide_program = \"\"\"\n",
    "#include \"Halide.h\"\n",
    "#include <stdio.h>\n",
    "\n",
    "using namespace Halide;\n",
    "int main(int argc, char *argv[]) {\n",
    "\n",
    "  ImageParam inp(type_of<int>(), 1, \"inp\"); \n",
    "  Func f(\"f\");\n",
    "  Var x(\"x\");\n",
    "  \n",
    "  inp.requires(inp(_0) > 1);\n",
    "  f(x) = inp(x)*inp(x);\n",
    "  f.ensures(f(x) > 1);\n",
    "  \n",
    "  std::vector<Annotation> pipeline_anns = {\n",
    "   requires(inp.dim(0).extent() == f.output_buffer().dim(0).extent()),\n",
    "   requires(inp.dim(0).min() == f.output_buffer().dim(0).min())\n",
    "  };\n",
    "  \n",
    "  f.translate_to_pvl(\"test_front.pvl\", {inp}, {});\n",
    "  f.compile_to_c(\"test_back.c\", {inp}, pipeline_anns, \"f\");\n",
    "} \n",
    "\"\"\"\n",
    "with open(\"test/test.cpp\", 'w') as f:\n",
    "    f.write(halide_program)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "9f1bea1c",
   "metadata": {},
   "outputs": [],
   "source": [
    "# This should compile the program without errors\n",
    "!g++ test/test.cpp -g -I /haliver/include -L  /haliver/lib -lHalide -lpthread -ldl -o test/test"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "9b68880a",
   "metadata": {},
   "outputs": [],
   "source": [
    "# This should generate the source files\n",
    "!cd test && LD_LIBRARY_PATH=/haliver/lib ./test"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "4feb333d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "test  test_back.c  test.cpp  test_front.log  test_front.pvl\r\n"
     ]
    }
   ],
   "source": [
    "!ls test"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "9a649c84",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[34m[build.sc] [1/52] scriptSources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [3/52] cliImports \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [15/52] compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [16/52] enclosingClasspath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [20/52] resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [23/52] mill.scalalib.ZincWorkerModule.zincLogDebug \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [24/52] mill.scalalib.ZincWorkerModule.worker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [26/52] sources.super.mill.scalalib.JavaModule.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[build.sc] [47/52] zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[3/654] vercors.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[6/654] mill.scalalib.ZincWorkerModule.zincLogDebug \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[7/654] mill.scalalib.ZincWorkerModule.worker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[11/654] hre.pprofProto.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[13/654] mill.contrib.scalapblib.ScalaPBWorkerApi.scalaPBWorker \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[17/654] hre.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[25/654] hre.pprofProto.scalaPBIncludePath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[45/654] hre.pprofProto.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[57/654] hre.pprofProto.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[75/654] hre.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[76/654] foreign-modules.project.fetchJars.z3.classPath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[88/654] hre.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[93/654] foreign-modules.project.colMeta.proto.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[97/654] foreign-modules.project.colMeta.meta.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[101/654] foreign-modules.project.colMeta.meta.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[117/654] foreign-modules.project.colMeta.meta.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[129/654] foreign-modules.project.colMeta.meta.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[139/654] foreign-modules.project.colMeta.meta.nodeDefinitions \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[141/654] foreign-modules.project.colMeta.meta.protobuf \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[149/654] foreign-modules.project.colMeta.proto.scalaPBIncludePath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[169/654] foreign-modules.project.colMeta.proto.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[181/654] foreign-modules.project.colMeta.proto.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[185/654] col.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[186/654] foreign-modules.project.colMeta.meta.helpers \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[202/654] col.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[214/654] col.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[219/654] rewrite.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[235/654] rewrite.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[247/654] rewrite.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[252/654] parsers.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[254/654] foreign-modules.project.fetchJars.antlr.classPath \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[255/654] foreign-modules.project.antlr.c.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[256/654] foreign-modules.project.antlr.c.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[257/654] foreign-modules.project.antlr.c.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[260/654] foreign-modules.project.antlr.cpp.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[261/654] foreign-modules.project.antlr.cpp.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[262/654] foreign-modules.project.antlr.cpp.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[265/654] foreign-modules.project.antlr.java.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[266/654] foreign-modules.project.antlr.java.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[267/654] foreign-modules.project.antlr.java.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[270/654] foreign-modules.project.antlr.pvl.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[271/654] foreign-modules.project.antlr.pvl.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[272/654] foreign-modules.project.antlr.pvl.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[275/654] foreign-modules.project.antlr.llvm.depsRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[276/654] foreign-modules.project.antlr.llvm.lexerRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[277/654] foreign-modules.project.antlr.llvm.parserRef \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[279/654] parsers.generatedSources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[294/654] parsers.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[306/654] parsers.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[314/654] foreign-modules.project.viper.viper.silver.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[329/654] foreign-modules.project.viper.viper.silver.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[341/654] foreign-modules.project.viper.viper.silver.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[348/654] foreign-modules.project.viper.viper.silicon.common.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[363/654] foreign-modules.project.viper.viper.silicon.common.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[375/654] foreign-modules.project.viper.viper.silicon.common.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[379/654] foreign-modules.project.viper.viper.silicon.buildInfo.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[398/654] foreign-modules.project.viper.viper.silicon.buildInfo.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[410/654] foreign-modules.project.viper.viper.silicon.buildInfo.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[413/654] foreign-modules.project.viper.viper.silicon.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[428/654] foreign-modules.project.viper.viper.silicon.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[440/654] foreign-modules.project.viper.viper.silicon.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[446/654] foreign-modules.project.viper.viper.carbon.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[461/654] foreign-modules.project.viper.viper.carbon.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[473/654] foreign-modules.project.viper.viper.carbon.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[476/654] foreign-modules.project.viper.viper.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[491/654] foreign-modules.project.viper.viper.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[503/654] foreign-modules.project.viper.viper.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[507/654] viperApi.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[523/654] viperApi.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[535/654] viperApi.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[539/654] vercors.buildInfo.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[559/654] vercors.buildInfo.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[571/654] vercors.buildInfo.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[575/654] vercors.sources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[591/654] vercors.compileResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[603/654] vercors.zincReportCachedProblems \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[606/654] hre.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[608/654] hre.pprofProto.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[610/654] col.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[612/654] foreign-modules.project.colMeta.proto.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[614/654] rewrite.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[616/654] parsers.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[618/654] viperApi.packedResources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[620/654] foreign-modules.project.viper.viper.silver.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[622/654] foreign-modules.project.viper.viper.carbon.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[624/654] foreign-modules.project.viper.viper.silicon.buildInfo.resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[626/654] foreign-modules.project.viper.viper.silicon.buildInfo.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[628/654] foreign-modules.project.viper.viper.silicon.common.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[630/654] foreign-modules.project.viper.viper.silicon.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[632/654] foreign-modules.project.viper.viper.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[634/654] vercors.buildInfo.resources.super.mill.scalalib.JavaModule.resources \u001b[39m\n",
      "\u001b[1A\u001b[2K\u001b[9999D\u001b[34m[636/654] vercors.buildInfo.resources \u001b[39m\n",
      "\u001b[0J\u001b[0J[INFO] Starting verification\n",
      "\u001b[0J[0.0%] [▊                                                                    ]\n",
      "VerCors › Parsing\n",
      "\u001b[2A\u001b[0J[70.5%] [████████████████████████████████████████████████▏                   ]\n",
      "VerCors › Transformation › simplify › (\\forall int … ) ==> f_498665901(x) > 1)\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\u001b[2A\u001b[0J[70.5%] [████████████████████████████████████████████████▏                   ]\n",
      "VerCors › Transformation › simplify\n",
      "\u001b[2A\u001b[0J[WARN] The binder `test_front.pvl:75:10`:`(\\forall int x; 0 < f_min_0_124573125() + f_extent_0_553688150() ==> 1 < f_1972256518(x))` contains no triggers\n",
      "[70.5%] [████████████████████████████████████████████████▏                   ]\n",
      "VerCors › Transformation › simplify\n",
      "\u001b[2A\u001b[0J[70.8%] [████████████████████████████████████████████████▍                   ]\n",
      "VerCors › Transformation › simplify\n",
      "\u001b[2A\u001b[0J[71.2%] [████████████████████████████████████████████████▋                   ]\n",
      "VerCors › Transformation › classToRef\n",
      "\u001b[2A\u001b[0J[71.3%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Transformation › adtPointer\n",
      "\u001b[2A\u001b[0J[71.4%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Transformation › adtNothing\n",
      "\u001b[2A\u001b[0J[71.4%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Transformation › adtViper_order\n",
      "\u001b[2A\u001b[0J[71.4%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Transformation › adtTypeArgs\n",
      "\u001b[2A\u001b[0J[71.4%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Verification › Task 1\n",
      "\u001b[2A\u001b[0J[71.4%] [████████████████████████████████████████████████▊                   ]\n",
      "VerCors › Verification › Task 1 › Verifying `ensures \\res ... inp(int x0);`\n",
      "\u001b[2A\u001b[0J[81.2%] [███████████████████████████████████████████████████████▎            ]\n",
      "VerCors › Verification › Task 1 › Verifying `decreases; p ... =0 ? 0 : a/b;`\n",
      "\u001b[2A\u001b[0J[89.8%] [█████████████████████████████████████████████████████████████▏      ]\n",
      "VerCors › Verification › Task 1 › Verifying `decreases; p ... nt(x + 0.5f);`\n",
      "\u001b[2A\u001b[0J[94.5%] [████████████████████████████████████████████████████████████████▎   ]\n",
      "VerCors › Verification › Task 1 › Verifying `decreases; p ... = 0 ? x : -x;`\n",
      "\u001b[2A\u001b[0J[94.8%] [████████████████████████████████████████████████████████████████▌   ]\n",
      "VerCors › Verification › Task 1\n",
      "\u001b[2A\u001b[0J[95.2%] [████████████████████████████████████████████████████████████████▊   ]\n",
      "VerCors › Verification › Task 1\n",
      "├─ [41.0%] Verifying `decreases; p ... rat(1.0f, x);`\n",
      "├─ [34.4%] Verifying `decreases; p ... =0 ? 0 : a%b;`\n",
      "├─ [1.0%] Verifying `decreases; p ... =0 ? 0 : a/b … ses; p ... =0 ? 0 : a/b;`\n",
      "├─ [0.0%] Verifying `decreases; p ... ride_0() = 1 … ses; p ... ride_0() = 1;`\n",
      "├─ [27.1%] Executing `decreases; p ... nt(x + 0.5f);`\n",
      "└─ [10.9%] Executing `decreases; p ... p_extent_0( … › /*state consolidation*/\n",
      "\u001b[8A\u001b[0J[INFO] Verification completed successfully.\n",
      "[95.2%] [████████████████████████████████████████████████████████████████▊   ]\n",
      "VerCors › Verification › Task 1\n",
      "├─ [41.0%] Verifying `decreases; p ... rat(1.0f, x);`\n",
      "├─ [34.4%] Verifying `decreases; p ... =0 ? 0 : a%b;`\n",
      "├─ [1.0%] Verifying `decreases; p ... =0 ? 0 : a/b … ses; p ... =0 ? 0 : a/b;`\n",
      "├─ [0.0%] Verifying `decreases; p ... ride_0() = 1 … ses; p ... ride_0() = 1;`\n",
      "├─ [27.1%] Executing `decreases; p ... nt(x + 0.5f);`\n",
      "└─ [10.9%] Executing `decreases; p ... p_extent_0( … › /*state consolidation*/\n"
     ]
    }
   ],
   "source": [
    "# This should verify the front-end. It should say somewhere:\n",
    "# `[INFO] Verification completed successfully.`\n",
    "# Note that it is quite verbose\n",
    "!/vercors/vct test/test_front.pvl"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "ea83428e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "^C\r\n"
     ]
    }
   ],
   "source": [
    "# Same for the back-end. It should say somewhere:\n",
    "# `[INFO] Verification completed successfully.`\n",
    "!/vercors/vct test/test_back.c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "f556fd10",
   "metadata": {},
   "outputs": [
    {
     "ename": "KeyboardInterrupt",
     "evalue": "",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mKeyboardInterrupt\u001b[0m                         Traceback (most recent call last)",
      "\u001b[0;32m/tmp/ipykernel_18044/3306672611.py\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[1;32m      3\u001b[0m \u001b[0;31m# For VerCors Verification Succes=0, Verification Fail=1, Error=2, TimeOut=3\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      4\u001b[0m \u001b[0;31m# You can inspect the actual output in the log_file you provide.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 5\u001b[0;31m \u001b[0mrunCommand\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcommand\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m'/vercors/vct'\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'test/test_front.pvl'\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mlog_file\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;34m'test/test_front.log'\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mverbose\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;32mFalse\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/exp/preprocess.py\u001b[0m in \u001b[0;36mrunCommand\u001b[0;34m(command, log_file, verbose, timeout)\u001b[0m\n\u001b[1;32m    137\u001b[0m     \u001b[0merr_out\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0mOptional\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mstr\u001b[0m\u001b[0;34m]\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    138\u001b[0m     \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 139\u001b[0;31m         \u001b[0mp\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mrun\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcommand\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mcapture_output\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;32mTrue\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtext\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    140\u001b[0m     \u001b[0;32mexcept\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mTimeoutExpired\u001b[0m \u001b[0;32mas\u001b[0m \u001b[0mto\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    141\u001b[0m         \u001b[0mend\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mtime\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtime\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/usr/lib/python3.10/subprocess.py\u001b[0m in \u001b[0;36mrun\u001b[0;34m(input, capture_output, timeout, check, *popenargs, **kwargs)\u001b[0m\n\u001b[1;32m    503\u001b[0m     \u001b[0;32mwith\u001b[0m \u001b[0mPopen\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0mpopenargs\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mas\u001b[0m \u001b[0mprocess\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    504\u001b[0m         \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 505\u001b[0;31m             \u001b[0mstdout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstderr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcommunicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minput\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    506\u001b[0m         \u001b[0;32mexcept\u001b[0m \u001b[0mTimeoutExpired\u001b[0m \u001b[0;32mas\u001b[0m \u001b[0mexc\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    507\u001b[0m             \u001b[0mprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mkill\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/usr/lib/python3.10/subprocess.py\u001b[0m in \u001b[0;36mcommunicate\u001b[0;34m(self, input, timeout)\u001b[0m\n\u001b[1;32m   1152\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   1153\u001b[0m             \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 1154\u001b[0;31m                 \u001b[0mstdout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstderr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_communicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minput\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m   1155\u001b[0m             \u001b[0;32mexcept\u001b[0m \u001b[0mKeyboardInterrupt\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   1156\u001b[0m                 \u001b[0;31m# https://bugs.python.org/issue25942\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/usr/lib/python3.10/subprocess.py\u001b[0m in \u001b[0;36m_communicate\u001b[0;34m(self, input, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m   2019\u001b[0m                             'failed to raise TimeoutExpired.')\n\u001b[1;32m   2020\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 2021\u001b[0;31m                     \u001b[0mready\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mselector\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mselect\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m   2022\u001b[0m                     \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_check_timeout\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0morig_timeout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstdout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstderr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   2023\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/usr/lib/python3.10/selectors.py\u001b[0m in \u001b[0;36mselect\u001b[0;34m(self, timeout)\u001b[0m\n\u001b[1;32m    414\u001b[0m         \u001b[0mready\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    415\u001b[0m         \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 416\u001b[0;31m             \u001b[0mfd_event_list\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_selector\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mpoll\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    417\u001b[0m         \u001b[0;32mexcept\u001b[0m \u001b[0mInterruptedError\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    418\u001b[0m             \u001b[0;32mreturn\u001b[0m \u001b[0mready\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mKeyboardInterrupt\u001b[0m: "
     ]
    }
   ],
   "source": [
    "# Since the output is so verbose, for the actual tests we use some scripting from preprocess.py\n",
    "# The output gives back a tupple with (time, result). result is based of the error code of the command.\n",
    "# For VerCors Verification Succes=0, Verification Fail=1, Error=2, TimeOut=3\n",
    "# You can inspect the actual output in the log_file you provide.\n",
    "runCommand(command=['/vercors/vct', 'test/test_front.pvl'], log_file='test/test_front.log', verbose=False)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "022d0203",
   "metadata": {},
   "source": [
    "# Experiments from Paper"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "54dd9751",
   "metadata": {},
   "outputs": [],
   "source": [
    "# The experiments use the `Experiments` class, which run the produced files from cmake.\n",
    "# The files are made via cmake, let's check if everything generates okay\n",
    "# Warnings about clock skew you can ignore\n",
    "!cmake -B build -S .\n",
    "!cmake --build build"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "432a58ba",
   "metadata": {},
   "outputs": [],
   "source": [
    "# if this does not work, run \n",
    "#!rm -r build && mkdir build && cmake -B build -S . && cmake --build build"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "1be1e9c8",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 1 # repetitions Normally set to 5, but 1 should be sufficient here\n",
    "t = 1*60 # timeout in seconds\n",
    "vercors_loc = '/vercors/vct'\n",
    "silicon_loc = '/vercors/silicon'\n",
    "# These are the versions\n",
    "versions: Dict[str, List[str]] = {\n",
    "    'blur' : ['0','1','2','3'],\n",
    "    'hist' : ['0','1','2','3'],\n",
    "    'conv_layer' : ['0','1','2','3'],\n",
    "    'gemm' : ['0','1','2','3'],\n",
    "    'auto_viz' : ['0','1','2','3'],\n",
    "}\n",
    "# these are the versions for memory only results\n",
    "versionsMem: Dict[str, List[str]] = {\n",
    "    'blur' : ['0','1','2','3'],\n",
    "    'hist' : ['0','1','2','3'],\n",
    "    'conv_layer' : ['0','1','2','3'],\n",
    "    'gemm' : ['0','1','2','3'],\n",
    "    'auto_viz' : ['0','1','2','3'],\n",
    "    'camera_pipe' : [''],\n",
    "    'bilateral_grid' : [''],\n",
    "    'depthwise_separable_conv' : [''],\n",
    "}\n",
    "# Set up experiments class\n",
    "experiments = Experiments(versions, versionsMem, vercors_loc=vercors_loc, \n",
    "                          silicon_loc=silicon_loc, repetitions = n, timeout = t)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "4ab3a329",
   "metadata": {},
   "outputs": [],
   "source": [
    "# You can run a front end example with\n",
    "experiments.front_end(name='blur')\n",
    "# A log of this run can be found in `logs/blur_front.pvl.txt`\n",
    "# It is verifying the file `build/blur_front.pvl`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "15d030fb",
   "metadata": {},
   "outputs": [],
   "source": [
    "# And a back-end example with\n",
    "experiments.back_end(name='blur', version='0')\n",
    "# A log of this run can be found in `logs/blur_0.c.txt`\n",
    "# It is verifying the file `build/blur_0.c`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2dc6cc4a",
   "metadata": {},
   "outputs": [],
   "source": [
    "# It takes the default values for timeout and repititions, but you can also set them directly.\n",
    "# Furthermore, if you do not specify a version, it will run all versions.\n",
    "# Note that the timeouts are actually set for the verification part of VerCors, for bigger files the \n",
    "# the tool takes 20 seconds to parse and translate before starting to verify.\n",
    "experiments.back_end(name='blur', timeout=2, repetitions=1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "c4f6b91d",
   "metadata": {},
   "outputs": [],
   "source": [
    "# With the `mem` option set to True you run the mem versions\n",
    "experiments.back_end(name='blur', version='1', mem=True, repetitions=2)\n",
    "# A log of this run can be found in `logs/blur_0_mem.c.txt`"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "68863b64",
   "metadata": {},
   "source": [
    "# Generate Table 1 & 2 by Loading"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "4943fb22",
   "metadata": {},
   "outputs": [],
   "source": [
    "# The results can also be loaded. The results of the paper are located in\n",
    "#'2023-10-09-18-59_results_verification.json' and\n",
    "# `2023-10-09-18-59_line_info.json`\n",
    "load_prefix = \"results/2023-10-09-18-59\"\n",
    "experiments.load_results(load_prefix)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "b46566f2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "inconsistent results for 'gemm_2_mem.c'\n",
      "avr_total, passes, fails,  timeouts, passtime, failtime: (196.43292951583862, 4, 1, 0, 196.250727891922, 197.16173601150513)\n"
     ]
    }
   ],
   "source": [
    "# It will warn about inconsistent results, as mentioned in the paper as well\n",
    "mem_table = make_mem_table(experiments) # This is table 1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "71fc2f23",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\begin{tabular}{l l \\vbar \\vbar r \\vbar r \\vbar r r r r}\n",
      "\\hline \\textbf{Name} & & \\multicolumn{1}{l\\vbar}{\\textbf{\\halide}} & \\textbf{\\textbf{Sched}}. & \\multicolumn{3}{l}{\\textbf{\\c}} & \\\\\n",
      "& & \\textbf{LoC} & \\textbf{Dir.} & \\textbf{LoC} & \\textbf{Ann.} & \\textbf{Loops} & \\textbf{T. (s).} \\\\ \\hline \\hline\n",
      "blur & V0 & 36 & 0 & 178 &60 &2 & 18\\\\ \\hline\n",
      " & V1-\\{f,p\\} & \\ditto &2 &172 &56 &1 & 19\\\\ \\hline\n",
      " & V2-\\{c,p,r,s\\} & \\ditto &6 &212 &74 &6 & 29\\\\ \\hline\n",
      " & V3-\\{c,p,s,st,u\\} & \\ditto &8 &211 &72 &5 & 24\\\\ \\hline\n",
      "\\hline\n",
      "hist & V0 & 71 & 2 & 299 &98 &11 & 30\\\\ \\hline\n",
      " & V1-\\{c,p,r,u\\} & \\ditto &4 &308 &99 &11 & 38\\\\ \\hline\n",
      " & V2-\\{c,p,r,u\\} & \\ditto &6 &311 &105 &13 & 48\\\\ \\hline\n",
      " & V3-\\{c,p,r,u\\} & \\ditto &13 &312 &101 &13 & 48\\\\ \\hline\n",
      "\\hline\n",
      "conv\\_ & V0 & 44 & 0 & 273 &148 &7 & 90\\\\ \\hline\n",
      "layer & V1-\\{c,f,p,u\\} & \\ditto &4 &281 &145 &8 & 97\\\\ \\hline\n",
      " & V2-\\{p,r,s,u\\} & \\ditto &6 &302 &166 &10 & 209\\\\ \\hline\n",
      " & V3-\\{c,p,r,s,u\\} & \\ditto &15 &279 &148 &7 & 168\\\\ \\hline\n",
      "\\hline\n",
      "gemm & V0 & 70 & 0 & 218 &105 &3 & 41\\\\ \\hline\n",
      " & V1-\\{c,p,r,s\\} & \\ditto &8 &274 &136 &10 & 89\\\\ \\hline\n",
      " & V2-\\{c,p,r,s\\} & \\ditto &16 &342 &173 &19 & 196$^{\\dag}$\\\\ \\hline\n",
      " & V3-\\{c,f,p,r,s,u\\} & \\ditto &24 &451 &221 &31 & F\\\\ \\hline\n",
      "\\hline\n",
      "auto\\_ & V0 & 112 & 0 & 443 &118 &19 & 35\\\\ \\hline\n",
      "viz & V1-\\{c\\} & \\ditto &9 &402 &139 &23 & 180\\\\ \\hline\n",
      " & V2-\\{c,p\\} & \\ditto &12 &440 &156 &27 & 170\\\\ \\hline\n",
      " & V3-\\{c,p,r,s\\} & \\ditto &27 &443 &152 &25 & 105\\\\ \\hline\n",
      "\\hline\n",
      "\\multicolumn{2}{l \\vbar \\vbar}{camera\\_pipe-\\{c,p,r,s,st\\} } & 346 & 27 & 701 &236 &25 & F\\\\ \\hline\n",
      "\\hline\n",
      "\\multicolumn{2}{l \\vbar \\vbar}{bilateral\\_grid-\\{c,p,r,u\\} } & 88 & 18 & 562 &180 &39 & 140\\\\ \\hline\n",
      "\\hline\n",
      "\\multicolumn{2}{l \\vbar \\vbar}{depthwise\\_separable\\_conv-\\{c,p,r,s\\} } & 94 & 13 & 562 &315 &44 & 480\\\\ \\hline\n",
      "\\hline\n",
      "\\end{tabular}\n"
     ]
    }
   ],
   "source": [
    "# This the actual latex table code\n",
    "print(mem_table)\n",
    "# We can write it to file\n",
    "with open(\"result_table_mem.tex\", \"w\") as f:\n",
    "    f.write(mem_table)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "aeaca623",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "inconsistent results for 'blur_3.c'\n",
      "avr_total, passes, fails,  timeouts, passtime, failtime: (96.95583856105804, 4, 0, 1, 96.95583856105804, None)\n",
      "inconsistent results for 'auto_viz_0.c'\n",
      "avr_total, passes, fails,  timeouts, passtime, failtime: (151.5906184911728, 2, 0, 3, 151.5906184911728, None)\n",
      "inconsistent results for 'auto_viz_2.c'\n",
      "avr_total, passes, fails,  timeouts, passtime, failtime: (229.82511369387308, 3, 0, 2, 229.82511369387308, None)\n",
      "inconsistent results for 'auto_viz_3.c'\n",
      "avr_total, passes, fails,  timeouts, passtime, failtime: (192.47571301460266, 4, 0, 1, 192.47571301460266, None)\n",
      "\\begin{tabular}{l l \\vbar \\vbar r r \\vbar r \\vbar r \\vbar r r r r \\vbar \\vbar r}\n",
      "\\hline Name & & \\multicolumn{2}{l\\vbar}{\\halide} & \\multicolumn{1}{l\\vbar}{Fr-end} & Sched. & \\multicolumn{3}{l}{\\C} & & LoA \\\\\n",
      "& & LoC & LoA & T. (s) & LoC & LoC & LoA & Loops & T. (s) & incr. \\\\ \\hline \\hline\n",
      "blur & V0 & 36 & 2 & 8 & 0 & 178 &63 &2 & 21 & 31.5x\\\\ \\hline\n",
      " & V1-\\{f,p\\} & \\ditto & \\ditto & \\ditto &2 &172 &58 &1 & 23 & 29.0x\\\\ \\hline\n",
      " & V2-\\{c,p,r,s\\} & \\ditto & \\ditto & \\ditto &6 &212 &83 &6 & 52 & 41.5x\\\\ \\hline\n",
      " & V3-\\{c,p,s,st,u\\} & \\ditto & \\ditto & \\ditto &8 &211 &79 &5 & 97$^{\\dag}$ & 39.5x\\\\ \\hline\n",
      "\\hline\n",
      "hist & V0 & 71 & 10 & 8 & 0 & 299 &118 &11 & 34 & 11.8x\\\\ \\hline\n",
      " & V1-\\{c,p,r,u\\} & \\ditto & \\ditto & \\ditto &4 &308 &118 &11 & 47 & 11.8x\\\\ \\hline\n",
      " & V2-\\{c,p,r,u\\} & \\ditto & \\ditto & \\ditto &6 &311 &123 &13 & 56 & 12.3x\\\\ \\hline\n",
      " & V3-\\{c,p,r,u\\} & \\ditto & \\ditto & \\ditto &13 &312 &125 &13 & 64 & 12.5x\\\\ \\hline\n",
      "\\hline\n",
      "conv\\_ & V0 & 44 & 7 & 8 & 0 & 273 &177 &7 & 111 & 25.3x\\\\ \\hline\n",
      "layer & V1-\\{c,f,p,u\\} & \\ditto & \\ditto & \\ditto &4 &281 &174 &8 & 108 & 24.9x\\\\ \\hline\n",
      " & V2-\\{p,r,s,u\\} & \\ditto & \\ditto & \\ditto &6 &302 &204 &10 & 283 & 29.1x\\\\ \\hline\n",
      " & V3-\\{c,p,r,s,u\\} & \\ditto & \\ditto & \\ditto &15 &279 &177 &7 & 207 & 25.3x\\\\ \\hline\n",
      "\\hline\n",
      "gemm & V0 & 70 & 12 & 7 & 0 & 218 &120 &3 & 43 & 10.0x\\\\ \\hline\n",
      " & V1-\\{c,p,r,s\\} & \\ditto & \\ditto & \\ditto &8 &274 &169 &10 & 133 & 14.1x\\\\ \\hline\n",
      " & V2-\\{c,p,r,s\\} & \\ditto & \\ditto & \\ditto &16 &342 &230 &19 & 368 & 19.2x\\\\ \\hline\n",
      " & V3-\\{c,f,p,r,s,u\\} & \\ditto & \\ditto & \\ditto &24 &451 &310 &31 & F & 25.8x\\\\ \\hline\n",
      "\\hline\n",
      "auto\\_ & V0 & 112 & 15 & 8 & 0 & 443 &158 &19 & 152$^{\\dag}$ & 10.5x\\\\ \\hline\n",
      "viz & V1-\\{c\\} & \\ditto & \\ditto & \\ditto &9 &402 &210 &23 & 216 & 14.0x\\\\ \\hline\n",
      " & V2-\\{c,p\\} & \\ditto & \\ditto & \\ditto &12 &440 &235 &27 & 230$^{\\dag}$ & 15.7x\\\\ \\hline\n",
      " & V3-\\{c,p,r,s\\} & \\ditto & \\ditto & \\ditto &27 &443 &229 &25 & 192$^{\\dag}$ & 15.3x\\\\ \\hline\n",
      "\\hline\n",
      "\\end{tabular}\n"
     ]
    }
   ],
   "source": [
    "# Same for Table 2 of the paper\n",
    "normal_table = make_normal_table(experiments)\n",
    "# This the actual latex table code\n",
    "print(normal_table)\n",
    "# We can write it to file\n",
    "with open(\"result_table.tex\", \"w\") as f:\n",
    "    f.write(normal_table)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "177fc15f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "pdflatex: unrecognized option '-quiet'\n",
      "This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2022/dev/Debian) (preloaded format=pdflatex)\n",
      " restricted \\write18 enabled.\n",
      "entering extended mode\n",
      "(./table.tex\n",
      "LaTeX2e <2021-11-15> patch level 1\n",
      "L3 programming layer <2022-01-21>\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls\n",
      "Document Class: article 2021/10/04 v1.4n Standard LaTeX document class\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo))\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty)\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/tools/xspace.sty)\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def)\n",
      "No file table.aux.\n",
      "(/usr/share/texlive/texmf-dist/tex/latex/base/t1cmtt.fd)\n",
      "(./result_table_mem.tex)\n",
      "Overfull \\hbox (77.70122pt too wide) in paragraph at lines 1--21\n",
      " [][] \n",
      "(./result_table.tex)\n",
      "Overfull \\hbox (90.03825pt too wide) in paragraph at lines 1--29\n",
      " [][] \n",
      "[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2] (./table.aux)\n",
      "\n",
      "LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.\n",
      "\n",
      " )\n",
      "\n",
      "kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 ecxc1000\n",
      "mktexpk: Running mf-nowin -progname=mf \\mode:=ljfour; mag:=1+0/600; nonstopmode; input ecxc1000\n",
      "This is METAFONT, Version 2.71828182 (TeX Live 2022/dev/Debian) (preloaded base=mf)\n",
      "\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecxc1000.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecxc.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excsc.mf\n",
      " Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [192] [193] [194] [195] [196] [197] [198] [199] [200] [201] [202] [203]\n",
      "[204] [205] [206] [207] [208] [209] [210] [211] [212] [213] [214] [215]\n",
      "[216] [217] [218] [219] [220] [221] [222] [223])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [128] [129] [130] [131] [132] [133] [134] [135] [136] [137] [138] [139]\n",
      "[140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151]\n",
      "[152] [153] [154] [155] [156] [157])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78]\n",
      "[79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbraces.mf\n",
      " Ok [94] [126] [23] [40] [41] [60] [124] [62] [91] [93] [92] [123] [125]\n",
      "[95] [127] [32])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expunct.mf\n",
      " Ok [14] [15] [19] [20] [13] [18] [33] [39] [42] [43] [44] [46] [47] [58]\n",
      "[59] [61] [96] [189] [17] [45] [16] [21] [22])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exsign.mf\n",
      " Ok [24] [34] [35] [36] [37] [64] [191] [159])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exromp.mf\n",
      " Ok [38] [63] [190])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrdigit.mf\n",
      " Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excspl.mf\n",
      " Ok [25] [26] [27] [28] [29] [30] [31] [158])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [97] [98] [99] [100] [101] [102] [103] [104] [105] [106] [107] [108]\n",
      "[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]\n",
      "[121] [122])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [224] [225] [226] [227] [228] [229] [230] [231] [232] [233] [234] [235]\n",
      "[236] [237] [238] [239] [240] [241] [242] [243] [244] [245] [246] [247]\n",
      "[248] [249] [250] [251] [252] [253] [254] [255])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [160] [161] [162] [163] [164] [165] [166] [167] [168] [169] [170] [171]\n",
      "[172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] [183]\n",
      "[184] [185] [186] [187] [188])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txpseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txaccent.mf\n",
      " Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excligtb.mf\n",
      " Ok) ) ) )\n",
      "(some charht values had to be adjusted by as much as 0.09453pt)\n",
      "Font metrics written on ecxc1000.tfm.\n",
      "Output written on ecxc1000.600gf (256 characters, 50664 bytes).\n",
      "Transcript written on ecxc1000.log.\n",
      "mktexpk: /home/tacas23/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ecxc1000.600pk: successfully generated.\n",
      "(see the transcript file for additional information) </home/tacas23/.texlive202\n",
      "1/texmf-var/fonts/pk/ljfour/jknappen/ec/ecxc1000.600pk>\n",
      "kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 ecbx1000\n",
      "mktexpk: Running mf-nowin -progname=mf \\mode:=ljfour; mag:=1+0/600; nonstopmode; input ecbx1000\n",
      "This is METAFONT, Version 2.71828182 (TeX Live 2022/dev/Debian) (preloaded base=mf)\n",
      "\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecbx1000.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecbx.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exroman.mf\n",
      " Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [192] [193] [194] [195] [196] [197] [198] [199] [200] [201] [202] [203]\n",
      "[204] [205] [206] [207] [208] [209] [210] [211] [212] [213] [214] [215]\n",
      "[216] [217] [218] [219] [220] [221] [222] [223])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlwest.mf\n",
      " Ok [224] [225] [226] [227] [228] [229] [230] [231] [232] [233] [234] [235]\n",
      "[236] [237] [238] [239] [240] [241] [242] [243] [244] [245] [246] [247]\n",
      "[248] [249] [250] [251] [252] [253] [254] [255])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [128] [129] [130] [131] [132] [133] [134] [135] [136] [137] [138] [139]\n",
      "[140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151]\n",
      "[152] [153] [154] [155] [156] [157])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrleast.mf\n",
      " Ok [158] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169] [170]\n",
      "[171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182]\n",
      "[183] [184] [185] [186] [187] [188])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbraces.mf\n",
      " Ok [94] [126] [23] [40] [41] [60] [124] [62] [91] [93] [92] [123] [125]\n",
      "[95] [127] [32])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expunct.mf\n",
      " Ok [14] [15] [19] [20] [13] [18] [33] [39] [42] [43] [44] [46] [47] [58]\n",
      "[59] [61] [96] [189] [17] [45] [16] [21] [22])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccent.mf\n",
      " Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exsign.mf\n",
      " Ok [24] [34] [35] [36] [37] [64] [191] [159])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlig.mf\n",
      " Ok [25] [26] [28] [27] [29] [30] [31])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exromp.mf\n",
      " Ok [38] [63] [190])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78]\n",
      "[79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrllett.mf\n",
      " Ok [97] [98] [99] [100] [101] [102] [103] [104] [105] [106] [107] [108]\n",
      "[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]\n",
      "[121] [122])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrdigit.mf\n",
      " Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrligtb.mf\n",
      " Ok) ) ) )\n",
      "Font metrics written on ecbx1000.tfm.\n",
      "Output written on ecbx1000.600gf (256 characters, 49864 bytes).\n",
      "Transcript written on ecbx1000.log.\n",
      "mktexpk: /home/tacas23/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ecbx1000.600pk: successfully generated.\n",
      " </home/tacas23/.texlive\n",
      "2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ecbx1000.600pk>\n",
      "kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 ectt1000\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "mktexpk: Running mf-nowin -progname=mf \\mode:=ljfour; mag:=1+0/600; nonstopmode; input ectt1000\n",
      "This is METAFONT, Version 2.71828182 (TeX Live 2022/dev/Debian) (preloaded base=mf)\n",
      "\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ectt1000.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ectt.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exroman.mf\n",
      " Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [192] [193] [194] [195] [196] [197] [198] [199] [200] [201] [202] [203]\n",
      "[204] [205] [206] [207] [208] [209] [210] [211] [212] [213] [214] [215]\n",
      "[216] [217] [218] [219] [220] [221] [222] [223])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlwest.mf\n",
      " Ok [224] [225] [226] [227] [228] [229] [230] [231] [232] [233] [234] [235]\n",
      "[236] [237] [238] [239] [240] [241] [242] [243] [244] [245] [246] [247]\n",
      "[248] [249] [250] [251] [252] [253] [254] [255])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [128] [129] [130] [131] [132] [133] [134] [135] [136] [137] [138] [139]\n",
      "[140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151]\n",
      "[152] [153] [154] [155] [156] [157])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrleast.mf\n",
      " Ok [158] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169] [170]\n",
      "[171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182]\n",
      "[183] [184] [185] [186] [187] [188])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbraces.mf\n",
      " Ok [94] [126] [23] [40] [41] [60] [124] [62] [91] [93] [92] [123] [125]\n",
      "[95] [127] [32])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expunct.mf\n",
      " Ok [14] [15] [19] [20] [13] [18] [33] [39] [42] [43] [44] [46] [47] [58]\n",
      "[59] [61] [96] [189] [17] [45] [16] [21] [22])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccent.mf\n",
      " Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exsign.mf\n",
      " Ok [24] [34] [35] [36] [37] [64] [191] [159])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlig.mf\n",
      " Ok [25] [26] [28] [27] [29] [30] [31])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exromp.mf\n",
      " Ok [38] [63] [190])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78]\n",
      "[79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrllett.mf\n",
      " Ok [97] [98] [99] [100] [101] [102] [103] [104] [105] [106] [107] [108]\n",
      "[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]\n",
      "[121] [122])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrdigit.mf\n",
      " Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exmligtb.mf\n",
      " Ok) ) ) )\n",
      "Font metrics written on ectt1000.tfm.\n",
      "Output written on ectt1000.600gf (256 characters, 43832 bytes).\n",
      "Transcript written on ectt1000.log.\n",
      "mktexpk: /home/tacas23/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ectt1000.600pk: successfully generated.\n",
      " </home/tacas23/.texl\n",
      "ive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ectt1000.600pk>\n",
      "kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 eccc1000\n",
      "mktexpk: Running mf-nowin -progname=mf \\mode:=ljfour; mag:=1+0/600; nonstopmode; input eccc1000\n",
      "This is METAFONT, Version 2.71828182 (TeX Live 2022/dev/Debian) (preloaded base=mf)\n",
      "\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/eccc1000.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/eccc.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excsc.mf\n",
      " Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [192] [193] [194] [195] [196] [197] [198] [199] [200] [201] [202] [203]\n",
      "[204] [205] [206] [207] [208] [209] [210] [211] [212] [213] [214] [215]\n",
      "[216] [217] [218] [219] [220] [221] [222] [223])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [128] [129] [130] [131] [132] [133] [134] [135] [136] [137] [138] [139]\n",
      "[140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151]\n",
      "[152] [153] [154] [155] [156] [157])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78]\n",
      "[79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbraces.mf\n",
      " Ok [94] [126] [23] [40] [41] [60] [124] [62] [91] [93] [92] [123] [125]\n",
      "[95] [127] [32])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expunct.mf\n",
      " Ok [14] [15] [19] [20] [13] [18] [33] [39] [42] [43] [44] [46] [47] [58]\n",
      "[59] [61] [96] [189] [17] [45] [16] [21] [22])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exsign.mf\n",
      " Ok [24] [34] [35] [36] [37] [64] [191] [159])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exromp.mf\n",
      " Ok [38] [63] [190])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrdigit.mf\n",
      " Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excspl.mf\n",
      " Ok [25] [26] [27] [28] [29] [30] [31] [158])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [97] [98] [99] [100] [101] [102] [103] [104] [105] [106] [107] [108]\n",
      "[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]\n",
      "[121] [122])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [224] [225] [226] [227] [228] [229] [230] [231] [232] [233] [234] [235]\n",
      "[236] [237] [238] [239] [240] [241] [242] [243] [244] [245] [246] [247]\n",
      "[248] [249] [250] [251] [252] [253] [254] [255])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [160] [161] [162] [163] [164] [165] [166] [167] [168] [169] [170] [171]\n",
      "[172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182] [183]\n",
      "[184] [185] [186] [187] [188])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txpseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/txaccent.mf\n",
      " Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/excligtb.mf\n",
      " Ok) ) ) )\n",
      "(some charht values had to be adjusted by as much as 0.06943pt)\n",
      "Font metrics written on eccc1000.tfm.\n",
      "Output written on eccc1000.600gf (256 characters, 51852 bytes).\n",
      "Transcript written on eccc1000.log.\n",
      "mktexpk: /home/tacas23/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/eccc1000.600pk: successfully generated.\n",
      " </home/tacas23/.t\n",
      "exlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/eccc1000.600pk>\n",
      "kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 ecrm1000\n",
      "mktexpk: Running mf-nowin -progname=mf \\mode:=ljfour; mag:=1+0/600; nonstopmode; input ecrm1000\n",
      "This is METAFONT, Version 2.71828182 (TeX Live 2022/dev/Debian) (preloaded base=mf)\n",
      "\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecrm1000.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbase.mf)\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/ecrm.mf\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exroman.mf\n",
      " Ok (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccess.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expseudo.mf\n",
      " Ok) (/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exruwest.mf\n",
      " Ok [192] [193] [194] [195] [196] [197] [198] [199] [200] [201] [202] [203]\n",
      "[204] [205] [206] [207] [208] [209] [210] [211] [212] [213] [214] [215]\n",
      "[216] [217] [218] [219] [220] [221] [222] [223])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlwest.mf\n",
      " Ok [224] [225] [226] [227] [228] [229] [230] [231] [232] [233] [234] [235]\n",
      "[236] [237] [238] [239] [240] [241] [242] [243] [244] [245] [246] [247]\n",
      "[248] [249] [250] [251] [252] [253] [254] [255])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrueast.mf\n",
      " Ok [128] [129] [130] [131] [132] [133] [134] [135] [136] [137] [138] [139]\n",
      "[140] [141] [142] [143] [144] [145] [146] [147] [148] [149] [150] [151]\n",
      "[152] [153] [154] [155] [156] [157])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrleast.mf\n",
      " Ok [158] [160] [161] [162] [163] [164] [165] [166] [167] [168] [169] [170]\n",
      "[171] [172] [173] [174] [175] [176] [177] [178] [179] [180] [181] [182]\n",
      "[183] [184] [185] [186] [187] [188])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exbraces.mf\n",
      " Ok [94] [126] [23] [40] [41] [60] [124] [62] [91] [93] [92] [123] [125]\n",
      "[95] [127] [32])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/expunct.mf\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " Ok [14] [15] [19] [20] [13] [18] [33] [39] [42] [43] [44] [46] [47] [58]\n",
      "[59] [61] [96] [189] [17] [45] [16] [21] [22])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exaccent.mf\n",
      " Ok [0] [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exsign.mf\n",
      " Ok [24] [34] [35] [36] [37] [64] [191] [159])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrlig.mf\n",
      " Ok [25] [26] [28] [27] [29] [30] [31])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exromp.mf\n",
      " Ok [38] [63] [190])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrulett.mf\n",
      " Ok [65] [66] [67] [68] [69] [70] [71] [72] [73] [74] [75] [76] [77] [78]\n",
      "[79] [80] [81] [82] [83] [84] [85] [86] [87] [88] [89] [90])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrllett.mf\n",
      " Ok [97] [98] [99] [100] [101] [102] [103] [104] [105] [106] [107] [108]\n",
      "[109] [110] [111] [112] [113] [114] [115] [116] [117] [118] [119] [120]\n",
      "[121] [122])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrdigit.mf\n",
      " Ok [48] [49] [50] [51] [52] [53] [54] [55] [56] [57])\n",
      "(/usr/share/texlive/texmf-dist/fonts/source/jknappen/ec/exrligtb.mf\n",
      " Ok) ) ) )\n",
      "(some charht values had to be adjusted by as much as 0.06586pt)\n",
      "Font metrics written on ecrm1000.tfm.\n",
      "Output written on ecrm1000.600gf (256 characters, 51184 bytes).\n",
      "Transcript written on ecrm1000.log.\n",
      "mktexpk: /home/tacas23/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ecrm1000.600pk: successfully generated.\n",
      " </home/tacas23\n",
      "/.texlive2021/texmf-var/fonts/pk/ljfour/jknappen/ec/ecrm1000.600pk></usr/share/\n",
      "texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb>\n",
      "Output written on table.pdf (2 pages, 45643 bytes).\n",
      "Transcript written on table.log.\n"
     ]
    }
   ],
   "source": [
    "# Make the pdf from the latex files\n",
    "!pdflatex -quiet table.tex"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "ba011f31",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<iframe src=table.pdf width=950 height=500></iframe>"
      ],
      "text/plain": [
       "<preprocess.PDF at 0x7fd4c06aab00>"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# View the pdf here\n",
    "PDF('table.pdf',size=(950,500))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "9f781bab",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}