communicate_with_lean.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Communicating with Lean"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "toc": true
   },
   "source": [
    "<h1>Table of Contents<span class=\"tocSkip\"></span></h1>\n",
    "<div class=\"toc\"><ul class=\"toc-item\"><li><span><a href=\"#Communicating-with-Lean\" data-toc-modified-id=\"Communicating-with-Lean-1\"><span class=\"toc-item-num\">1&nbsp;&nbsp;</span>Communicating with Lean</a></span><ul class=\"toc-item\"><li><span><a href=\"#Lean-Server\" data-toc-modified-id=\"Lean-Server-1.1\"><span class=\"toc-item-num\">1.1&nbsp;&nbsp;</span>Lean Server</a></span></li><li><span><a href=\"#Testing-tactics-with-the-Lean-Server\" data-toc-modified-id=\"Testing-tactics-with-the-Lean-Server-1.2\"><span class=\"toc-item-num\">1.2&nbsp;&nbsp;</span>Testing tactics with the Lean Server</a></span><ul class=\"toc-item\"><li><span><a href=\"#Speed-and-robustness\" data-toc-modified-id=\"Speed-and-robustness-1.2.1\"><span class=\"toc-item-num\">1.2.1&nbsp;&nbsp;</span>Speed and robustness</a></span></li><li><span><a href=\"#Stepping-through-a-full-proof\" data-toc-modified-id=\"Stepping-through-a-full-proof-1.2.2\"><span class=\"toc-item-num\">1.2.2&nbsp;&nbsp;</span>Stepping through a full proof</a></span></li></ul></li><li><span><a href=\"#Creating-a-simple-Lean-solver-(with-breath-first-search)-in-Python\" data-toc-modified-id=\"Creating-a-simple-Lean-solver-(with-breath-first-search)-in-Python-1.3\"><span class=\"toc-item-num\">1.3&nbsp;&nbsp;</span>Creating a simple Lean solver (with breath first search) in Python</a></span></li><li><span><a href=\"#Custom-printing-of-Lean-expressions\" data-toc-modified-id=\"Custom-printing-of-Lean-expressions-1.4\"><span class=\"toc-item-num\">1.4&nbsp;&nbsp;</span>Custom printing of Lean expressions</a></span></li><li><span><a href=\"#Current-issues\" data-toc-modified-id=\"Current-issues-1.5\"><span class=\"toc-item-num\">1.5&nbsp;&nbsp;</span>Current issues</a></span><ul class=\"toc-item\"><li><span><a href=\"#Privately-defined-terms\" data-toc-modified-id=\"Privately-defined-terms-1.5.1\"><span class=\"toc-item-num\">1.5.1&nbsp;&nbsp;</span>Privately defined terms</a></span></li><li><span><a href=\"#Term-blowup\" data-toc-modified-id=\"Term-blowup-1.5.2\"><span class=\"toc-item-num\">1.5.2&nbsp;&nbsp;</span>Term blowup</a></span></li><li><span><a href=\"#Missing-@-symbols\" data-toc-modified-id=\"Missing-@-symbols-1.5.3\"><span class=\"toc-item-num\">1.5.3&nbsp;&nbsp;</span>Missing @ symbols</a></span></li><li><span><a href=\"#Extra-@-sysmbols-(or-maybe-a-missing-case-in-the-Lean-parser)\" data-toc-modified-id=\"Extra-@-sysmbols-(or-maybe-a-missing-case-in-the-Lean-parser)-1.5.4\"><span class=\"toc-item-num\">1.5.4&nbsp;&nbsp;</span>Extra <code>@</code> sysmbols (or maybe a missing case in the Lean parser)</a></span></li><li><span><a href=\"#Implicit-and-type-class-assumptions\" data-toc-modified-id=\"Implicit-and-type-class-assumptions-1.5.5\"><span class=\"toc-item-num\">1.5.5&nbsp;&nbsp;</span>Implicit and type class assumptions</a></span></li><li><span><a href=\"#Let-expressions\" data-toc-modified-id=\"Let-expressions-1.5.6\"><span class=\"toc-item-num\">1.5.6&nbsp;&nbsp;</span>Let expressions</a></span></li><li><span><a href=\"#Other\" data-toc-modified-id=\"Other-1.5.7\"><span class=\"toc-item-num\">1.5.7&nbsp;&nbsp;</span>Other</a></span></li></ul></li><li><span><a href=\"#TODOs\" data-toc-modified-id=\"TODOs-1.6\"><span class=\"toc-item-num\">1.6&nbsp;&nbsp;</span>TODOs</a></span></li><li><span><a href=\"#What-I-want-from-Lean-4\" data-toc-modified-id=\"What-I-want-from-Lean-4-1.7\"><span class=\"toc-item-num\">1.7&nbsp;&nbsp;</span>What I want from Lean 4</a></span></li></ul></li></ul></div>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is a hacky prototype showing how one can use Lean's server for communication between Lean and another program.  We have in mind implementing something like HOList for Lean. The main idea is that theorem proving is like a puzzle similar to the Rubik cube.  One has states and actions one can perform to move to other states.  This states are goals (or lists of goals) and the actions are tactics.  \n",
    "\n",
    "What we build here is an interface where one says to Lean \"apply this tactic to this goal\" and Lean says whether that tactic succeeds and if so what the new list of goals are.  It is written in a Python notebook, but the ideas transcend languages."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "import subprocess\n",
    "import tempfile\n",
    "import json\n",
    "from pprint import pprint\n",
    "import time\n",
    "from datetime import datetime\n",
    "import collections\n",
    "from IPython.display import display"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Lean Server\n",
    "This class starts up a Lean server and communicates with it.  There are a number of requests one can make to the Lean server, but we only need one or two.  To understand the Lean server, it is important to know it is not like a REPL, but more like the LSP.  It is designed to partial compile and comment on files as they are being written.  The use here is more of a hack (and it is unfortunately quite a bit slow we will see).\n",
    "\n",
    "One communicates to Lean by sending JSON requests and getting back responses.  We only need one or two request types for our purposes.  The first request we need is a \"sync\" request.  It sends a \"file\" to Lean to be synced.  (The file doesn't actually need to exist.)  The second request, an \"info\" request, asks Lean to provide more information about particular places in the code.  Unfortunately, the responses to the requests don't actually provide a lot of direct answers.  Especially for the \"sync\" request, one has to wait for an \"all_messages\" request to provide answers.  (And even then, it is difficult to determine that the response you got is up-to-date with the current Lean file.  We've employed a lot of tricks to make sure we are getting the most up-to-date information from Lean.)  Our class will store any \"all_messages\" responses it sees into a queue for latter processing.\n",
    "\n",
    "Ultimately, the \"info\" requests turned out not to be a reliable as we hoped, so we just use the \"sync\" request and only use the \"info\" request to prevent blocking of the channel."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "class LeanServer:\n",
    "    \"\"\"\n",
    "    Open up a Lean server and communicate with it.  \n",
    "    \n",
    "    Right now it only has support for the \"sync\" and \"info\" requests (and their)\n",
    "    corresponding responses.  It does however, store all \"all_messages\" response\n",
    "    into a queue for later processing.\n",
    "    \"\"\"\n",
    "    \n",
    "    def __init__(self):\n",
    "        self.cntr = -1\n",
    "        self.cntr2 = -1\n",
    "        self.all_messages = []\n",
    "        self.all_messages_time = -1\n",
    "        self.current_tasks = []\n",
    "        self.current_tasks_time = -1\n",
    "        self.proc = subprocess.Popen(['lean', '--server'], \n",
    "                    universal_newlines=True, \n",
    "                    stdin=subprocess.PIPE, # pipe STDIN and STDOUT to send and receive messages\n",
    "                    stdout=subprocess.PIPE, \n",
    "                    #stderr=subprocess.PIPE\n",
    "                )\n",
    "    \n",
    "    # make into a context manager so that it closes lean server automatically\n",
    "    def __enter__(self):\n",
    "        self.proc.__enter__()\n",
    "        return self\n",
    "    \n",
    "    def __exit__(self, type, value, traceback):\n",
    "        self.proc.__exit__(type, value, traceback)\n",
    "    \n",
    "    def seq_num(self):\n",
    "        self.cntr += 1\n",
    "        return self.cntr\n",
    "    \n",
    "    def send_request(self, request, expected_response, verbose=False, sleep=0.0):\n",
    "        seq_num = self.seq_num()\n",
    "        request1 = request.copy()\n",
    "        request1['seq_num'] = seq_num\n",
    "        j = json.dumps(request1)\n",
    "        \n",
    "        # TODO: Use logging instead\n",
    "        if verbose:\n",
    "            print()\n",
    "            print(\"=>:\", datetime.now().strftime('%H:%M:%S.%f'))\n",
    "            pprint(j)\n",
    "            print()\n",
    "        \n",
    "        # send\n",
    "        print(j, file=self.proc.stdin, flush=True)\n",
    "        \n",
    "        # wait for response\n",
    "        time.sleep(sleep)\n",
    "        while True:\n",
    "            self.cntr2 += 1\n",
    "            raw_output = self.proc.stdout.readline()\n",
    "            output = json.loads(raw_output)\n",
    "            if verbose:\n",
    "                print(\"<=:\", datetime.now().strftime('%H:%M:%S.%f'))\n",
    "                pprint(output)\n",
    "                print()\n",
    "            if 'response' in output:\n",
    "                if output['response'] == expected_response and output['seq_num'] == seq_num:\n",
    "                    return output\n",
    "                # TODO: Handle error differently.  It means the JSON is bad\n",
    "                elif output['response'] == 'error':\n",
    "                    return output\n",
    "                # record messages since they may point to errors in the lean code\n",
    "                elif output['response'] == 'all_messages':\n",
    "                    self.all_messages = output['msgs']\n",
    "                    self.all_messages_time = self.cntr2\n",
    "                # record tasks to know when Lean has stopped processing file\n",
    "                elif output['response'] == 'current_tasks':\n",
    "                    self.current_tasks = output['tasks']\n",
    "                    self.current_tasks_time = self.cntr2\n",
    "    \n",
    "    def send_sync_request(self, file_name, content, verbose=False):\n",
    "        request = {\n",
    "            'command':'sync',\n",
    "            'file_name': file_name,\n",
    "            \"content\": content,\n",
    "        }\n",
    "        \n",
    "        return self.send_request(request, expected_response='ok', verbose=verbose, sleep=0.0)\n",
    "    \n",
    "    def send_info_request(self, file_name, line, column, verbose=False):\n",
    "        request = {            \n",
    "            'command':'info',\n",
    "            'file_name': file_name,\n",
    "            'column': column,\n",
    "            'line': line\n",
    "        }\n",
    "        \n",
    "        return self.send_request(request, expected_response='ok', verbose=verbose, sleep=0.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'message': 'file invalidated', 'response': 'ok', 'seq_num': 0}"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "{'response': 'ok', 'seq_num': 1}"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "[{'caption': '',\n",
       "  'file_name': '/tmp/fake_lean_file.lean',\n",
       "  'pos_col': 0,\n",
       "  'pos_line': 1,\n",
       "  'severity': 'warning',\n",
       "  'text': \"declaration '[anonymous]' uses sorry\"}]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# sync file (the \"file\" doesn't need to exist)\n",
    "with LeanServer() as lean_server:\n",
    "    response1 = lean_server.send_sync_request(\n",
    "        file_name='/tmp/fake_lean_file.lean', \n",
    "        content='example (p: Prop) : p = p := begin sorry end')\n",
    "    time.sleep(1)\n",
    "    response2 = lean_server.send_info_request(\n",
    "        file_name='/tmp/fake_lean_file.lean', \n",
    "        line=1, \n",
    "        column=0)\n",
    "    \n",
    "    # the responses themselves aren't always useful\n",
    "    display(response1)\n",
    "    display(response2)\n",
    "    \n",
    "    # the \"all_messages\" responses are more useful\n",
    "    display(lean_server.all_messages)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In much of the code, use the optional parameter `verbose=True` to see the message traffic."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "=>: 10:45:37.131428\n",
      "('{\"content\": \"example (p: Prop) : p = p := begin sorry end\", \"file_name\": '\n",
      " '\"/tmp/fake_lean_file.lean\", \"seq_num\": 0, \"command\": \"sync\"}')\n",
      "\n",
      "<=: 10:45:37.387175\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:37.605599\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:37.808850\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:37.890468\n",
      "{'message': 'file invalidated', 'response': 'ok', 'seq_num': 0}\n",
      "\n",
      "\n",
      "=>: 10:45:37.890757\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"/tmp/fake_lean_file.lean\", \"seq_num\": '\n",
      " '1, \"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:37.891602\n",
      "{'response': 'ok', 'seq_num': 1}\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# sync file (the \"file\" doesn't need to exist)\n",
    "with LeanServer() as lean_server:\n",
    "    lean_server.send_sync_request(\n",
    "        file_name='/tmp/fake_lean_file.lean', \n",
    "        content='example (p: Prop) : p = p := begin sorry end',\n",
    "        verbose=True)\n",
    "    lean_server.send_info_request(\n",
    "        file_name='/tmp/fake_lean_file.lean', \n",
    "        line=1,\n",
    "        column=0,\n",
    "        verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Testing tactics with the Lean Server"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Again, tactic-based theorem proving is like a puzzle.  You go from state to state exploring.  What we need is a way to test if we can use a tactic on a goal and what the next goals are.  This is what the LeanTacticTestingInterface does.  (Note, it is much faster to ask the Lean server about multiple goal-tactic pairs instead of just one at a time.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "# For storing information about a Lean goal\n",
    "LeanGoal = collections.namedtuple('LeanGoal', ['universes', 'assumptions', 'conclusion'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "inspection_tools = r\"\"\"\n",
    "namespace inspection_tools\n",
    "\n",
    "def join (sep : string) : list string → string\n",
    "| [x]     := x\n",
    "| []      := \"\"\n",
    "| (x::xs) := x ++ sep ++ join xs\n",
    "\n",
    "meta def expr_to_string (e : expr bool.tt) : tactic string :=\n",
    "do\n",
    "  o ← tactic.get_options,\n",
    "  tactic.set_options (options.mk.set_bool `pp.all tt),\n",
    "  f ← tactic.pp e,\n",
    "  tactic.set_options o,  -- set back to before\n",
    "  return $ to_string f\n",
    "  \n",
    "meta def local_cxt_to_string (v : expr bool.tt) : tactic string := \n",
    "do \n",
    "  tp ← tactic.infer_type v,\n",
    "  v_str ← expr_to_string v,\n",
    "  tp_str ← expr_to_string tp,\n",
    "  return $ v_str ++ \"\\n\\n\" ++ tp_str\n",
    "\n",
    "meta def goal_to_string (g : expr) : tactic string :=\n",
    "do \n",
    "  tactic.set_goals [g],\n",
    "  goal ← tactic.target,\n",
    "  local_cxt ← tactic.local_context,\n",
    "  let local_cxt_len := list.length local_cxt,\n",
    "  goal_str ← expr_to_string goal,\n",
    "  local_cxt_strs ← (list.mmap local_cxt_to_string local_cxt),\n",
    "  let s1 := goal_str ++ \"\\n\\n\",\n",
    "  let s2 := \"Local Context Vars: \" ++ (to_string local_cxt_len) ++ \"\\n\\n\",\n",
    "  let s3 := join \"\\n\\n\" local_cxt_strs,\n",
    "  return $ s1 ++ s2 ++ s3\n",
    "\n",
    "meta def state_report : tactic string :=\n",
    "do \n",
    " gs ← tactic.get_goals,\n",
    " -- loop over all goals (has effect of resetting the goal each time)\n",
    " let gs_len := list.length gs,\n",
    " goal_strings ← gs.mmap goal_to_string,\n",
    " tactic.set_goals gs,  -- set goals back\n",
    " let s := \"Goals: \" ++ (to_string gs_len) ++ \"\\n\\n\" ++ (join \"\\n\\n\" goal_strings),\n",
    " return s\n",
    " \n",
    "meta def trace_goal_state : tactic unit :=\n",
    "do \n",
    " s ← state_report,\n",
    " tactic.trace s,\n",
    " return ()\n",
    "\n",
    "end inspection_tools\n",
    "\"\"\"\n",
    "\n",
    "default_custom_code = r\"\"\"\n",
    "namespace custom\n",
    " \n",
    "meta def trace_custom_state : tactic unit :=\n",
    "do \n",
    " tactic.trace \"\",  -- make more interesting\n",
    " return ()\n",
    "\n",
    "end custom\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "class LeanTacticTestingInterface:\n",
    "    \"\"\"\n",
    "    Interface to test a tactic on a goal (or multiple tactics on multiple goals)\n",
    "    \"\"\"\n",
    "    def __init__(self):\n",
    "        self.lean_server = LeanServer()\n",
    "        \n",
    "        self.msg_cntr = 0\n",
    "        self.file_name = 'dummy.lean'   # the name of the \"file\" being checked (not a real file)\n",
    "        self.dummy_file = 'dummy.lean'  # a file always kept empty \n",
    "        self.eval_line_pos = None       # used for checking that a file is complete\n",
    "        \n",
    "        # set up a dummy file for later use\n",
    "        self.lean_server.send_sync_request(file_name=self.dummy_file, content=\"\")\n",
    "        \n",
    "        # one can implement their own custom state trace.  This is the default.\n",
    "        self.custom_code = default_custom_code\n",
    "    \n",
    "     # make into a context manager so that it closes lean server automatically\n",
    "    def __enter__(self):\n",
    "        self.lean_server.__enter__()\n",
    "        return self\n",
    "    \n",
    "    def __exit__(self, type, value, traceback):\n",
    "        self.lean_server.__exit__(type, value, traceback)\n",
    "        \n",
    "    def parse_state(self, universes, goal_state):\n",
    "        \"\"\"\n",
    "        Parses the trace string returned by trace_goal_state\n",
    "        \"\"\"\n",
    "        lines = iter(' '.join(l.split()) for l in goal_state.split(\"\\n\\n\"))\n",
    "        \n",
    "        goal_cnt = int(next(lines).split()[-1])\n",
    "        \n",
    "        goals = []\n",
    "        for _ in range(goal_cnt):\n",
    "            target = next(lines)\n",
    "            assump_cnt = int(next(lines).split()[-1])\n",
    "            assumptions = []\n",
    "            for _ in range(assump_cnt):\n",
    "                v = next(lines)\n",
    "                tp = next(lines)\n",
    "                assumptions.append(v + \" : \" + tp)\n",
    "            goal = LeanGoal(universes, assumptions, target)\n",
    "            goals.append(goal)\n",
    "\n",
    "        return goals\n",
    "    \n",
    "    def check_content(self, content, verbose):\n",
    "        \"\"\"\n",
    "        Have Lean check the contents of a Lean \"file\". \n",
    "        \"\"\"\n",
    "        self.msg_cntr += 1\n",
    "        \n",
    "        # empty out the previous file for good measure\n",
    "        self.lean_server.send_sync_request(file_name=self.file_name, content=\"\", verbose=verbose)\n",
    "        \n",
    "        # use a few different file names to help avoid old data in the messages\n",
    "        self.file_name = 'fake_lean_file{}.lean'.format(self.msg_cntr % 10)\n",
    "        \n",
    "        # put an eval at the end to make sure the response is not from an old file\n",
    "        extended_content = content + \"\\n#eval \" + str(self.msg_cntr)\n",
    "        self.eval_line_pos = extended_content.count(\"\\n\") + 1\n",
    "        \n",
    "        if verbose:\n",
    "            print(\"-- {} --------------\".format(self.file_name))\n",
    "            for i, l in enumerate(extended_content.split('\\n')):\n",
    "                print(\"{:3}   {}\".format(i+1, l))\n",
    "            print(\"-------------------------\")\n",
    "            \n",
    "        # send the file\n",
    "        self.lean_server.send_sync_request(file_name=self.file_name, content=extended_content, verbose=verbose)\n",
    "        \n",
    "    def get_messages(self, verbose):\n",
    "        \"\"\"\n",
    "        Get messages for the current content being checked.\n",
    "        Return all the messages for that \"file\"\n",
    "        \n",
    "        This is really really hard to make robust.  How do I know Lean has finished\n",
    "        or worst that Lean isn't still providing information from an old\n",
    "        version of the file?\n",
    "        \"\"\"\n",
    "        \n",
    "        # wait for tasks to stop running\n",
    "        tasks_stopped_time = None\n",
    "        for _ in range(10000):  # lazy time-out mechanism\n",
    "            \n",
    "            # keep sending requests to a dummy file to collect more \"all_messages\" responses\n",
    "            self.lean_server.send_info_request(file_name=self.dummy_file, line=1, column=0, verbose=verbose)\n",
    "            \n",
    "            # check that tasks are complete for file_name\n",
    "            task_running = False\n",
    "            for task in self.lean_server.current_tasks:\n",
    "                if task['file_name'] == self.file_name:\n",
    "                    task_running = True\n",
    "                    break\n",
    "            if not task_running:\n",
    "                tasks_stopped_time = self.lean_server.current_tasks_time\n",
    "                break\n",
    "        else:\n",
    "            raise TimeoutError(\"Tasks still running for {}:\\n{}\".format('file_name', \"\\n\".join(self.lean_server.current_tasks)))\n",
    "            \n",
    "                \n",
    "        # check that messages are complete by looking at eval at the end\n",
    "        for _ in range(10000):  # lazy time-out mechanism\n",
    "            \n",
    "            # keep sending requests to a dummy file to collect more \"all_messages\" responses\n",
    "            self.lean_server.send_info_request(self.dummy_file, line=1, column=0, verbose=verbose)\n",
    "            \n",
    "            # wait until messages are after current tasks\n",
    "            #if self.lean_server.all_messages_time < tasks_stopped_time:\n",
    "            #    continue\n",
    "                \n",
    "            # filter the messages to those for this \"file\" \n",
    "            # and also check for the final the eval statement\n",
    "            filtered_messages = []\n",
    "            messages_are_complete = False\n",
    "            for msg in self.lean_server.all_messages:\n",
    "                if msg['file_name'] == self.file_name:\n",
    "                    if msg['pos_line'] < self.eval_line_pos:\n",
    "                        filtered_messages.append(msg)\n",
    "                    elif msg['pos_line'] == self.eval_line_pos and msg['caption'] == \"eval result\":\n",
    "                        if msg['text'] == str(self.msg_cntr):\n",
    "                            messages_are_complete = True\n",
    "                        else:\n",
    "                            break\n",
    "\n",
    "            # clear messages\n",
    "            self.lean_server.all_messages = []\n",
    "\n",
    "            if messages_are_complete:\n",
    "                return filtered_messages\n",
    "            \n",
    "        raise TimeoutError(\"Expecting eval result on line {} of file {} to be {}.  Run with verbose=True to check for error messages.\".format(\n",
    "                self.eval_line_pos, self.file_name, self.msg_cntr\n",
    "        ))\n",
    "    \n",
    "    def preamble(self, imports):\n",
    "        if imports:\n",
    "            import_line = \"import \" + \" \".join(imports) + \"\\n\"\n",
    "        else:\n",
    "            import_line = \"\"\n",
    "        \n",
    "        return import_line + inspection_tools + \"\\n\" + self.custom_code + \"\\n\"\n",
    "        \n",
    "    def example_block(self, goal, tactic):\n",
    "        block = \"\"\n",
    "        # line: preamble + 9 * n + 0\n",
    "        block += \"section example_block\\n\"\n",
    "        # line: preamble + 9 * n + 1\n",
    "        if goal.universes:\n",
    "            block += \"universes \" + \" \".join(goal.universes) + \"\\n\"\n",
    "        else:\n",
    "            block += \"--no universes\\n\"\n",
    "        # line: preamble + 9 * n + 2  \n",
    "        block += \"example \"\n",
    "        block += \" \".join(\"(\" + l.replace(\"\\n\", \" \").replace(\"…\", \"_redacted_code_too_long_\") + \")\" for l in goal.assumptions)\n",
    "        block += \" : \"\n",
    "        block += goal.conclusion.replace(\"\\n\", \" \").replace(\"…\", \"_redacted_code_too_long_\") + \" :=\\n\"\n",
    "        # line: preamble + 9 * n + 3\n",
    "        block += \"begin\\n\"  \n",
    "        # line: preamble + 9 * n + 4\n",
    "        block += tactic + \",\\n\"\n",
    "        # line: preamble + 9 * n + 5\n",
    "        block += 'inspection_tools.trace_goal_state,\\n' # goal state\n",
    "        # line: preamble + 9 * n + 6\n",
    "        block += 'custom.trace_custom_state,\\n'         # custom trace\n",
    "        # line: preamble + 9 * n + 7\n",
    "        block += \"end\\n\"\n",
    "        # line: preamble + 9 * n + 8\n",
    "        block += \"end example_block\\n\"\n",
    "\n",
    "        return block\n",
    "            \n",
    "    def apply_tactic_multiple(self, lean_goals, tactics, imports=[], verbose=False):\n",
    "        assert len(lean_goals) == len(tactics)\n",
    "        \n",
    "        # build content\n",
    "        preamble = self.preamble(imports)\n",
    "        \n",
    "        # this is the line (indexed from 1) that the first block will be on\n",
    "        preamble_length = preamble.count(\"\\n\") + 1\n",
    "        \n",
    "        content = preamble\n",
    "        for goal, tactic in zip(lean_goals, tactics):\n",
    "            content += self.example_block(goal, tactic)\n",
    "        \n",
    "        # start checking the file\n",
    "        self.check_content(content, verbose=verbose)\n",
    "            \n",
    "        # positions in the block\n",
    "        theorem_line = 2\n",
    "        tactic_line = 4\n",
    "        goals_line = 5\n",
    "        custom_state_line = 6\n",
    "        block_length = 9\n",
    "        \n",
    "        for _ in range(1000):  # lazy timeout method\n",
    "            # start checking the file\n",
    "            msgs = self.get_messages(verbose=verbose)\n",
    "        \n",
    "            # extract data from messages\n",
    "            results = [[None, None, [], []] for _ in lean_goals]\n",
    "            for msg in msgs:\n",
    "                block_line_pos = (msg['pos_line'] - preamble_length) % block_length\n",
    "                block_num = (msg['pos_line'] - preamble_length) // block_length\n",
    "\n",
    "                if msg['pos_line'] < preamble_length:\n",
    "                    continue\n",
    "                elif block_line_pos == goals_line and msg['severity'] == 'information':\n",
    "                    results[block_num][0] = msg['text']\n",
    "                elif block_line_pos == custom_state_line and msg['severity'] == 'information':\n",
    "                    results[block_num][1] = msg['text']\n",
    "                elif block_line_pos == tactic_line and msg['severity'] == 'error':\n",
    "                    results[block_num][2].append(msg['text'])\n",
    "                elif block_line_pos == theorem_line and msg['severity'] == 'error':\n",
    "                    results[block_num][3].append(msg['text'])\n",
    "\n",
    "            # parse data and check for completeness\n",
    "            final_results = []\n",
    "            complete = True\n",
    "            for i, ((goal_state, custom_state, tactic_errors, theorem_errors), prev_goal) in enumerate(zip(results, lean_goals)):\n",
    "                if theorem_errors:\n",
    "                    result = ('theorem_error', theorem_errors, '')\n",
    "                elif tactic_errors:\n",
    "                    result = ('tactic_failure', tactic_errors, '')\n",
    "                elif goal_state is not None and custom_state is not None:\n",
    "                    result = ('success', self.parse_state(prev_goal.universes, goal_state), custom_state.strip())\n",
    "                else:\n",
    "                    complete = False  # need to get messages again\n",
    "                    break\n",
    "\n",
    "                final_results.append(result)\n",
    "\n",
    "            if complete:\n",
    "                return final_results\n",
    "        \n",
    "        raise TimeoutError(\"Lean server sessages are not as expected:\\n{}\".format(\"\\n\".join(msgs)))\n",
    "        \n",
    "    def apply_tactic(self, lean_goal, tactic, imports=[], verbose=False):\n",
    "        \"\"\"\n",
    "        Apply tactic to a goal and see what you get.\n",
    "        \"\"\"\n",
    "        \n",
    "        result = self.apply_tactic_multiple([lean_goal], [tactic], imports=imports, verbose=verbose)\n",
    "        return result[0]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see if we apply `refl` to `p = p` we solve all the goals (hence the empty list returned)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal([], ['p q : Prop'],  'p = p')\n",
    "    display(lean_interface.apply_tactic(goal, 'refl'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One can also add universe levels, e.g. `u`, `v`, as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal(['u', 'v'], ['a b: Type u'],  'a = a')\n",
    "    display(lean_interface.apply_tactic(goal, 'refl'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Imports can also be added to the `apply_tactic` call:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal(['u'], ['α : Type u'],  'dlist.to_list (@dlist.empty α) = []')\n",
    "    display(lean_interface.apply_tactic(goal, 'refl', imports=['data.dlist']))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see what is going on, we show the logs with `verbose=True`.  This also prints the file being sent to Lean.  \n",
    "\n",
    "The main idea is that we encode everything we want to check into a Lean file, send that via a \"sync\" request, and read off the response from the messages."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "=>: 10:45:45.544907\n",
      "'{\"content\": \"\", \"file_name\": \"dummy.lean\", \"seq_num\": 1, \"command\": \"sync\"}'\n",
      "\n",
      "<=: 10:45:45.545603\n",
      "{'message': 'file unchanged', 'response': 'ok', 'seq_num': 1}\n",
      "\n",
      "-- fake_lean_file1.lean --------------\n",
      "  1   \n",
      "  2   namespace inspection_tools\n",
      "  3   \n",
      "  4   def join (sep : string) : list string → string\n",
      "  5   | [x]     := x\n",
      "  6   | []      := \"\"\n",
      "  7   | (x::xs) := x ++ sep ++ join xs\n",
      "  8   \n",
      "  9   meta def expr_to_string (e : expr bool.tt) : tactic string :=\n",
      " 10   do\n",
      " 11     o ← tactic.get_options,\n",
      " 12     tactic.set_options (options.mk.set_bool `pp.all tt),\n",
      " 13     f ← tactic.pp e,\n",
      " 14     tactic.set_options o,  -- set back to before\n",
      " 15     return $ to_string f\n",
      " 16     \n",
      " 17   meta def local_cxt_to_string (v : expr bool.tt) : tactic string := \n",
      " 18   do \n",
      " 19     tp ← tactic.infer_type v,\n",
      " 20     v_str ← expr_to_string v,\n",
      " 21     tp_str ← expr_to_string tp,\n",
      " 22     return $ v_str ++ \"\\n\\n\" ++ tp_str\n",
      " 23   \n",
      " 24   meta def goal_to_string (g : expr) : tactic string :=\n",
      " 25   do \n",
      " 26     tactic.set_goals [g],\n",
      " 27     goal ← tactic.target,\n",
      " 28     local_cxt ← tactic.local_context,\n",
      " 29     let local_cxt_len := list.length local_cxt,\n",
      " 30     goal_str ← expr_to_string goal,\n",
      " 31     local_cxt_strs ← (list.mmap local_cxt_to_string local_cxt),\n",
      " 32     let s1 := goal_str ++ \"\\n\\n\",\n",
      " 33     let s2 := \"Local Context Vars: \" ++ (to_string local_cxt_len) ++ \"\\n\\n\",\n",
      " 34     let s3 := join \"\\n\\n\" local_cxt_strs,\n",
      " 35     return $ s1 ++ s2 ++ s3\n",
      " 36   \n",
      " 37   meta def state_report : tactic string :=\n",
      " 38   do \n",
      " 39    gs ← tactic.get_goals,\n",
      " 40    -- loop over all goals (has effect of resetting the goal each time)\n",
      " 41    let gs_len := list.length gs,\n",
      " 42    goal_strings ← gs.mmap goal_to_string,\n",
      " 43    tactic.set_goals gs,  -- set goals back\n",
      " 44    let s := \"Goals: \" ++ (to_string gs_len) ++ \"\\n\\n\" ++ (join \"\\n\\n\" goal_strings),\n",
      " 45    return s\n",
      " 46    \n",
      " 47   meta def trace_goal_state : tactic unit :=\n",
      " 48   do \n",
      " 49    s ← state_report,\n",
      " 50    tactic.trace s,\n",
      " 51    return ()\n",
      " 52   \n",
      " 53   end inspection_tools\n",
      " 54   \n",
      " 55   \n",
      " 56   namespace custom\n",
      " 57    \n",
      " 58   meta def trace_custom_state : tactic unit :=\n",
      " 59   do \n",
      " 60    tactic.trace \"\",  -- make more interesting\n",
      " 61    return ()\n",
      " 62   \n",
      " 63   end custom\n",
      " 64   \n",
      " 65   section example_block\n",
      " 66   universes u v\n",
      " 67   example (a b: Type u) : a = a :=\n",
      " 68   begin\n",
      " 69   refl,\n",
      " 70   inspection_tools.trace_goal_state,\n",
      " 71   custom.trace_custom_state,\n",
      " 72   end\n",
      " 73   end example_block\n",
      " 74   \n",
      " 75   #eval 1\n",
      "-------------------------\n",
      "\n",
      "=>: 10:45:45.546283\n",
      "('{\"content\": \"\\\\nnamespace inspection_tools\\\\n\\\\ndef join (sep : string) : '\n",
      " 'list string \\\\u2192 string\\\\n| [x]     := x\\\\n| []      := \\\\\"\\\\\"\\\\n| '\n",
      " '(x::xs) := x ++ sep ++ join xs\\\\n\\\\nmeta def expr_to_string (e : expr '\n",
      " 'bool.tt) : tactic string :=\\\\ndo\\\\n  o \\\\u2190 tactic.get_options,\\\\n  '\n",
      " 'tactic.set_options (options.mk.set_bool `pp.all tt),\\\\n  f \\\\u2190 tactic.pp '\n",
      " 'e,\\\\n  tactic.set_options o,  -- set back to before\\\\n  return $ to_string '\n",
      " 'f\\\\n  \\\\nmeta def local_cxt_to_string (v : expr bool.tt) : tactic string := '\n",
      " '\\\\ndo \\\\n  tp \\\\u2190 tactic.infer_type v,\\\\n  v_str \\\\u2190 expr_to_string '\n",
      " 'v,\\\\n  tp_str \\\\u2190 expr_to_string tp,\\\\n  return $ v_str ++ '\n",
      " '\\\\\"\\\\\\\\n\\\\\\\\n\\\\\" ++ tp_str\\\\n\\\\nmeta def goal_to_string (g : expr) : tactic '\n",
      " 'string :=\\\\ndo \\\\n  tactic.set_goals [g],\\\\n  goal \\\\u2190 '\n",
      " 'tactic.target,\\\\n  local_cxt \\\\u2190 tactic.local_context,\\\\n  let '\n",
      " 'local_cxt_len := list.length local_cxt,\\\\n  goal_str \\\\u2190 expr_to_string '\n",
      " 'goal,\\\\n  local_cxt_strs \\\\u2190 (list.mmap local_cxt_to_string '\n",
      " 'local_cxt),\\\\n  let s1 := goal_str ++ \\\\\"\\\\\\\\n\\\\\\\\n\\\\\",\\\\n  let s2 := '\n",
      " '\\\\\"Local Context Vars: \\\\\" ++ (to_string local_cxt_len) ++ '\n",
      " '\\\\\"\\\\\\\\n\\\\\\\\n\\\\\",\\\\n  let s3 := join \\\\\"\\\\\\\\n\\\\\\\\n\\\\\" local_cxt_strs,\\\\n  '\n",
      " 'return $ s1 ++ s2 ++ s3\\\\n\\\\nmeta def state_report : tactic string :=\\\\ndo '\n",
      " '\\\\n gs \\\\u2190 tactic.get_goals,\\\\n -- loop over all goals (has effect of '\n",
      " 'resetting the goal each time)\\\\n let gs_len := list.length gs,\\\\n '\n",
      " 'goal_strings \\\\u2190 gs.mmap goal_to_string,\\\\n tactic.set_goals gs,  -- set '\n",
      " 'goals back\\\\n let s := \\\\\"Goals: \\\\\" ++ (to_string gs_len) ++ '\n",
      " '\\\\\"\\\\\\\\n\\\\\\\\n\\\\\" ++ (join \\\\\"\\\\\\\\n\\\\\\\\n\\\\\" goal_strings),\\\\n return s\\\\n '\n",
      " '\\\\nmeta def trace_goal_state : tactic unit :=\\\\ndo \\\\n s \\\\u2190 '\n",
      " 'state_report,\\\\n tactic.trace s,\\\\n return ()\\\\n\\\\nend '\n",
      " 'inspection_tools\\\\n\\\\n\\\\nnamespace custom\\\\n \\\\nmeta def trace_custom_state '\n",
      " ': tactic unit :=\\\\ndo \\\\n tactic.trace \\\\\"\\\\\",  -- make more interesting\\\\n '\n",
      " 'return ()\\\\n\\\\nend custom\\\\n\\\\nsection example_block\\\\nuniverses u '\n",
      " 'v\\\\nexample (a b: Type u) : a = a '\n",
      " ':=\\\\nbegin\\\\nrefl,\\\\ninspection_tools.trace_goal_state,\\\\ncustom.trace_custom_state,\\\\nend\\\\nend '\n",
      " 'example_block\\\\n\\\\n#eval 1\", \"file_name\": \"fake_lean_file1.lean\", \"seq_num\": '\n",
      " '2, \"command\": \"sync\"}')\n",
      "\n",
      "<=: 10:45:45.747776\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:45.963713\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:46.087615\n",
      "{'message': 'file invalidated', 'response': 'ok', 'seq_num': 2}\n",
      "\n",
      "\n",
      "=>: 10:45:46.087825\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 3, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.090066\n",
      "{'response': 'ok', 'seq_num': 3}\n",
      "\n",
      "\n",
      "=>: 10:45:46.090262\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 4, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.090626\n",
      "{'response': 'ok', 'seq_num': 4}\n",
      "\n",
      "\n",
      "=>: 10:45:46.090753\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 5, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.091122\n",
      "{'response': 'ok', 'seq_num': 5}\n",
      "\n",
      "\n",
      "=>: 10:45:46.091346\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 6, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.091682\n",
      "{'response': 'ok', 'seq_num': 6}\n",
      "\n",
      "\n",
      "=>: 10:45:46.091797\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 7, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.092102\n",
      "{'response': 'ok', 'seq_num': 7}\n",
      "\n",
      "\n",
      "=>: 10:45:46.092212\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 8, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.092514\n",
      "{'response': 'ok', 'seq_num': 8}\n",
      "\n",
      "\n",
      "=>: 10:45:46.092619\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 9, \"command\": '\n",
      " '\"info\"}')\n",
      "\n",
      "<=: 10:45:46.092919\n",
      "{'response': 'ok', 'seq_num': 9}\n",
      "\n",
      "\n",
      "=>: 10:45:46.093021\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 10, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.093321\n",
      "{'response': 'ok', 'seq_num': 10}\n",
      "\n",
      "\n",
      "=>: 10:45:46.093426\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 11, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.093718\n",
      "{'response': 'ok', 'seq_num': 11}\n",
      "\n",
      "\n",
      "=>: 10:45:46.093821\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 12, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.094116\n",
      "{'response': 'ok', 'seq_num': 12}\n",
      "\n",
      "\n",
      "=>: 10:45:46.094218\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 13, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.094515\n",
      "{'response': 'ok', 'seq_num': 13}\n",
      "\n",
      "\n",
      "=>: 10:45:46.094616\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 14, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.094908\n",
      "{'response': 'ok', 'seq_num': 14}\n",
      "\n",
      "\n",
      "=>: 10:45:46.095007\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 15, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.095305\n",
      "{'response': 'ok', 'seq_num': 15}\n",
      "\n",
      "\n",
      "=>: 10:45:46.095405\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 16, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.095695\n",
      "{'response': 'ok', 'seq_num': 16}\n",
      "\n",
      "\n",
      "=>: 10:45:46.095794\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 17, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.096083\n",
      "{'response': 'ok', 'seq_num': 17}\n",
      "\n",
      "\n",
      "=>: 10:45:46.096182\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 18, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.096462\n",
      "{'response': 'ok', 'seq_num': 18}\n",
      "\n",
      "\n",
      "=>: 10:45:46.096560\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 19, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.096852\n",
      "{'response': 'ok', 'seq_num': 19}\n",
      "\n",
      "\n",
      "=>: 10:45:46.096951\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 20, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.097239\n",
      "{'response': 'ok', 'seq_num': 20}\n",
      "\n",
      "\n",
      "=>: 10:45:46.097337\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 21, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.097635\n",
      "{'response': 'ok', 'seq_num': 21}\n",
      "\n",
      "\n",
      "=>: 10:45:46.097736\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 22, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.098032\n",
      "{'response': 'ok', 'seq_num': 22}\n",
      "\n",
      "\n",
      "=>: 10:45:46.098131\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 23, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.098422\n",
      "{'response': 'ok', 'seq_num': 23}\n",
      "\n",
      "\n",
      "=>: 10:45:46.098523\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 24, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.098821\n",
      "{'response': 'ok', 'seq_num': 24}\n",
      "\n",
      "\n",
      "=>: 10:45:46.098923\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 25, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.099215\n",
      "{'response': 'ok', 'seq_num': 25}\n",
      "\n",
      "\n",
      "=>: 10:45:46.099316\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 26, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.099634\n",
      "{'response': 'ok', 'seq_num': 26}\n",
      "\n",
      "\n",
      "=>: 10:45:46.099737\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 27, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.100037\n",
      "{'response': 'ok', 'seq_num': 27}\n",
      "\n",
      "\n",
      "=>: 10:45:46.100137\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 28, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.100429\n",
      "{'response': 'ok', 'seq_num': 28}\n",
      "\n",
      "\n",
      "=>: 10:45:46.100528\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 29, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.100829\n",
      "{'response': 'ok', 'seq_num': 29}\n",
      "\n",
      "\n",
      "=>: 10:45:46.100931\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 30, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.101226\n",
      "{'response': 'ok', 'seq_num': 30}\n",
      "\n",
      "\n",
      "=>: 10:45:46.101327\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 31, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.101624\n",
      "{'response': 'ok', 'seq_num': 31}\n",
      "\n",
      "\n",
      "=>: 10:45:46.101723\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 32, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.102013\n",
      "{'response': 'ok', 'seq_num': 32}\n",
      "\n",
      "\n",
      "=>: 10:45:46.102112\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 33, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.102419\n",
      "{'response': 'ok', 'seq_num': 33}\n",
      "\n",
      "\n",
      "=>: 10:45:46.102520\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 34, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.102812\n",
      "{'response': 'ok', 'seq_num': 34}\n",
      "\n",
      "\n",
      "=>: 10:45:46.102912\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 35, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.103206\n",
      "{'response': 'ok', 'seq_num': 35}\n",
      "\n",
      "\n",
      "=>: 10:45:46.103306\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 36, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.103599\n",
      "{'response': 'ok', 'seq_num': 36}\n",
      "\n",
      "\n",
      "=>: 10:45:46.103699\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 37, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.103986\n",
      "{'response': 'ok', 'seq_num': 37}\n",
      "\n",
      "\n",
      "=>: 10:45:46.104086\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 38, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.104379\n",
      "{'response': 'ok', 'seq_num': 38}\n",
      "\n",
      "\n",
      "=>: 10:45:46.104479\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 39, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.104776\n",
      "{'response': 'ok', 'seq_num': 39}\n",
      "\n",
      "\n",
      "=>: 10:45:46.104877\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 40, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.105175\n",
      "{'response': 'ok', 'seq_num': 40}\n",
      "\n",
      "\n",
      "=>: 10:45:46.105287\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 41, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.105581\n",
      "{'response': 'ok', 'seq_num': 41}\n",
      "\n",
      "\n",
      "=>: 10:45:46.105693\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 42, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.105996\n",
      "{'response': 'ok', 'seq_num': 42}\n",
      "\n",
      "\n",
      "=>: 10:45:46.106109\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 43, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.167035\n",
      "{'is_running': True,\n",
      " 'response': 'current_tasks',\n",
      " 'tasks': [{'desc': 'parsing at line 1',\n",
      "            'end_pos_col': 8,\n",
      "            'end_pos_line': 75,\n",
      "            'file_name': 'fake_lean_file1.lean',\n",
      "            'pos_col': 0,\n",
      "            'pos_line': 1},\n",
      "           {'desc': 'parsing at line 1',\n",
      "            'end_pos_col': 1,\n",
      "            'end_pos_line': 1,\n",
      "            'file_name': 'dummy.lean',\n",
      "            'pos_col': 0,\n",
      "            'pos_line': 1}]}\n",
      "\n",
      "<=: 10:45:46.544449\n",
      "{'response': 'ok', 'seq_num': 43}\n",
      "\n",
      "\n",
      "=>: 10:45:46.544811\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 44, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.545289\n",
      "{'response': 'ok', 'seq_num': 44}\n",
      "\n",
      "\n",
      "=>: 10:45:46.545466\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 45, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.545830\n",
      "{'response': 'ok', 'seq_num': 45}\n",
      "\n",
      "\n",
      "=>: 10:45:46.545996\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 46, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.546355\n",
      "{'response': 'ok', 'seq_num': 46}\n",
      "\n",
      "\n",
      "=>: 10:45:46.546516\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 47, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.546866\n",
      "{'response': 'ok', 'seq_num': 47}\n",
      "\n",
      "\n",
      "=>: 10:45:46.547023\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 48, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.547373\n",
      "{'response': 'ok', 'seq_num': 48}\n",
      "\n",
      "\n",
      "=>: 10:45:46.547528\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 49, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.547875\n",
      "{'response': 'ok', 'seq_num': 49}\n",
      "\n",
      "\n",
      "=>: 10:45:46.548030\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 50, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.548381\n",
      "{'response': 'ok', 'seq_num': 50}\n",
      "\n",
      "\n",
      "=>: 10:45:46.548540\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 51, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.548935\n",
      "{'response': 'ok', 'seq_num': 51}\n",
      "\n",
      "\n",
      "=>: 10:45:46.549098\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 52, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.549464\n",
      "{'response': 'ok', 'seq_num': 52}\n",
      "\n",
      "\n",
      "=>: 10:45:46.549584\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 53, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.549863\n",
      "{'response': 'ok', 'seq_num': 53}\n",
      "\n",
      "\n",
      "=>: 10:45:46.549972\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 54, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.550249\n",
      "{'response': 'ok', 'seq_num': 54}\n",
      "\n",
      "\n",
      "=>: 10:45:46.550358\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 55, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.550630\n",
      "{'response': 'ok', 'seq_num': 55}\n",
      "\n",
      "\n",
      "=>: 10:45:46.550737\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 56, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.551008\n",
      "{'response': 'ok', 'seq_num': 56}\n",
      "\n",
      "\n",
      "=>: 10:45:46.551114\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 57, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.551382\n",
      "{'response': 'ok', 'seq_num': 57}\n",
      "\n",
      "\n",
      "=>: 10:45:46.551486\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 58, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.551755\n",
      "{'response': 'ok', 'seq_num': 58}\n",
      "\n",
      "\n",
      "=>: 10:45:46.551859\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 59, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.552125\n",
      "{'response': 'ok', 'seq_num': 59}\n",
      "\n",
      "\n",
      "=>: 10:45:46.552257\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 60, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.552644\n",
      "{'response': 'ok', 'seq_num': 60}\n",
      "\n",
      "\n",
      "=>: 10:45:46.552827\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 61, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.553142\n",
      "{'response': 'ok', 'seq_num': 61}\n",
      "\n",
      "\n",
      "=>: 10:45:46.553266\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 62, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.553560\n",
      "{'response': 'ok', 'seq_num': 62}\n",
      "\n",
      "\n",
      "=>: 10:45:46.553668\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 63, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.553944\n",
      "{'response': 'ok', 'seq_num': 63}\n",
      "\n",
      "\n",
      "=>: 10:45:46.554049\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 64, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.554321\n",
      "{'response': 'ok', 'seq_num': 64}\n",
      "\n",
      "\n",
      "=>: 10:45:46.554425\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 65, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.554692\n",
      "{'response': 'ok', 'seq_num': 65}\n",
      "\n",
      "\n",
      "=>: 10:45:46.554796\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 66, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.555066\n",
      "{'response': 'ok', 'seq_num': 66}\n",
      "\n",
      "\n",
      "=>: 10:45:46.555170\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 67, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.555440\n",
      "{'response': 'ok', 'seq_num': 67}\n",
      "\n",
      "\n",
      "=>: 10:45:46.555548\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 68, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.555817\n",
      "{'response': 'ok', 'seq_num': 68}\n",
      "\n",
      "\n",
      "=>: 10:45:46.555919\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 69, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.556188\n",
      "{'response': 'ok', 'seq_num': 69}\n",
      "\n",
      "\n",
      "=>: 10:45:46.556292\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 70, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.556566\n",
      "{'response': 'ok', 'seq_num': 70}\n",
      "\n",
      "\n",
      "=>: 10:45:46.556666\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 71, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.556983\n",
      "{'response': 'ok', 'seq_num': 71}\n",
      "\n",
      "\n",
      "=>: 10:45:46.557089\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 72, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.557443\n",
      "{'response': 'ok', 'seq_num': 72}\n",
      "\n",
      "\n",
      "=>: 10:45:46.557561\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 73, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.557876\n",
      "{'response': 'ok', 'seq_num': 73}\n",
      "\n",
      "\n",
      "=>: 10:45:46.558084\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 74, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.558433\n",
      "{'response': 'ok', 'seq_num': 74}\n",
      "\n",
      "\n",
      "=>: 10:45:46.558549\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 75, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.558822\n",
      "{'response': 'ok', 'seq_num': 75}\n",
      "\n",
      "\n",
      "=>: 10:45:46.558929\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 76, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.559197\n",
      "{'response': 'ok', 'seq_num': 76}\n",
      "\n",
      "\n",
      "=>: 10:45:46.559298\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 77, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.559645\n",
      "{'response': 'ok', 'seq_num': 77}\n",
      "\n",
      "\n",
      "=>: 10:45:46.559756\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 78, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.560044\n",
      "{'response': 'ok', 'seq_num': 78}\n",
      "\n",
      "\n",
      "=>: 10:45:46.560157\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 79, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.560579\n",
      "{'response': 'ok', 'seq_num': 79}\n",
      "\n",
      "\n",
      "=>: 10:45:46.560774\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 80, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.561237\n",
      "{'response': 'ok', 'seq_num': 80}\n",
      "\n",
      "\n",
      "=>: 10:45:46.561375\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 81, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.561717\n",
      "{'response': 'ok', 'seq_num': 81}\n",
      "\n",
      "\n",
      "=>: 10:45:46.561836\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 82, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.562138\n",
      "{'response': 'ok', 'seq_num': 82}\n",
      "\n",
      "\n",
      "=>: 10:45:46.562253\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 83, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.562571\n",
      "{'response': 'ok', 'seq_num': 83}\n",
      "\n",
      "\n",
      "=>: 10:45:46.562687\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 84, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.563005\n",
      "{'response': 'ok', 'seq_num': 84}\n",
      "\n",
      "\n",
      "=>: 10:45:46.563117\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 85, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.563410\n",
      "{'response': 'ok', 'seq_num': 85}\n",
      "\n",
      "\n",
      "=>: 10:45:46.563514\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 86, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.563824\n",
      "{'response': 'ok', 'seq_num': 86}\n",
      "\n",
      "\n",
      "=>: 10:45:46.563929\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 87, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.564221\n",
      "{'response': 'ok', 'seq_num': 87}\n",
      "\n",
      "\n",
      "=>: 10:45:46.564325\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 88, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.564637\n",
      "{'response': 'ok', 'seq_num': 88}\n",
      "\n",
      "\n",
      "=>: 10:45:46.564743\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 89, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.565034\n",
      "{'response': 'ok', 'seq_num': 89}\n",
      "\n",
      "\n",
      "=>: 10:45:46.565139\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 90, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.565446\n",
      "{'response': 'ok', 'seq_num': 90}\n",
      "\n",
      "\n",
      "=>: 10:45:46.565551\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 91, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.565843\n",
      "{'response': 'ok', 'seq_num': 91}\n",
      "\n",
      "\n",
      "=>: 10:45:46.565949\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 92, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.566240\n",
      "{'response': 'ok', 'seq_num': 92}\n",
      "\n",
      "\n",
      "=>: 10:45:46.566346\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 93, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.566642\n",
      "{'response': 'ok', 'seq_num': 93}\n",
      "\n",
      "\n",
      "=>: 10:45:46.566745\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 94, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.567035\n",
      "{'response': 'ok', 'seq_num': 94}\n",
      "\n",
      "\n",
      "=>: 10:45:46.567135\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 95, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.567507\n",
      "{'response': 'ok', 'seq_num': 95}\n",
      "\n",
      "\n",
      "=>: 10:45:46.567705\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 96, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.568221\n",
      "{'response': 'ok', 'seq_num': 96}\n",
      "\n",
      "\n",
      "=>: 10:45:46.568536\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 97, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.569892\n",
      "{'response': 'ok', 'seq_num': 97}\n",
      "\n",
      "\n",
      "=>: 10:45:46.570115\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 98, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.570610\n",
      "{'response': 'ok', 'seq_num': 98}\n",
      "\n",
      "\n",
      "=>: 10:45:46.572098\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 99, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.573191\n",
      "{'response': 'ok', 'seq_num': 99}\n",
      "\n",
      "\n",
      "=>: 10:45:46.573481\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 100, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.574554\n",
      "{'response': 'ok', 'seq_num': 100}\n",
      "\n",
      "\n",
      "=>: 10:45:46.574801\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 101, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.575271\n",
      "{'response': 'ok', 'seq_num': 101}\n",
      "\n",
      "\n",
      "=>: 10:45:46.575423\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 102, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.575781\n",
      "{'response': 'ok', 'seq_num': 102}\n",
      "\n",
      "\n",
      "=>: 10:45:46.576064\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 103, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.576569\n",
      "{'response': 'ok', 'seq_num': 103}\n",
      "\n",
      "\n",
      "=>: 10:45:46.576719\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 104, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.577702\n",
      "{'response': 'ok', 'seq_num': 104}\n",
      "\n",
      "\n",
      "=>: 10:45:46.577969\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 105, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.578521\n",
      "{'response': 'ok', 'seq_num': 105}\n",
      "\n",
      "\n",
      "=>: 10:45:46.578676\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 106, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.579001\n",
      "{'response': 'ok', 'seq_num': 106}\n",
      "\n",
      "\n",
      "=>: 10:45:46.579125\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 107, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.579445\n",
      "{'response': 'ok', 'seq_num': 107}\n",
      "\n",
      "\n",
      "=>: 10:45:46.579561\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 108, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.579844\n",
      "{'response': 'ok', 'seq_num': 108}\n",
      "\n",
      "\n",
      "=>: 10:45:46.579953\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 109, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.580230\n",
      "{'response': 'ok', 'seq_num': 109}\n",
      "\n",
      "\n",
      "=>: 10:45:46.580337\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 110, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.580626\n",
      "{'response': 'ok', 'seq_num': 110}\n",
      "\n",
      "\n",
      "=>: 10:45:46.580844\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 111, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.581708\n",
      "{'response': 'ok', 'seq_num': 111}\n",
      "\n",
      "\n",
      "=>: 10:45:46.581865\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 112, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.582231\n",
      "{'response': 'ok', 'seq_num': 112}\n",
      "\n",
      "\n",
      "=>: 10:45:46.582363\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 113, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.582918\n",
      "{'response': 'ok', 'seq_num': 113}\n",
      "\n",
      "\n",
      "=>: 10:45:46.583174\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 114, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.583559\n",
      "{'response': 'ok', 'seq_num': 114}\n",
      "\n",
      "\n",
      "=>: 10:45:46.583686\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 115, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.584054\n",
      "{'response': 'ok', 'seq_num': 115}\n",
      "\n",
      "\n",
      "=>: 10:45:46.584243\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 116, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.584715\n",
      "{'response': 'ok', 'seq_num': 116}\n",
      "\n",
      "\n",
      "=>: 10:45:46.584921\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 117, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.586633\n",
      "{'response': 'ok', 'seq_num': 117}\n",
      "\n",
      "\n",
      "=>: 10:45:46.586918\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 118, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.587497\n",
      "{'response': 'ok', 'seq_num': 118}\n",
      "\n",
      "\n",
      "=>: 10:45:46.587724\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 119, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.588308\n",
      "{'response': 'ok', 'seq_num': 119}\n",
      "\n",
      "\n",
      "=>: 10:45:46.588547\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 120, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.589171\n",
      "{'response': 'ok', 'seq_num': 120}\n",
      "\n",
      "\n",
      "=>: 10:45:46.589403\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 121, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.589976\n",
      "{'response': 'ok', 'seq_num': 121}\n",
      "\n",
      "\n",
      "=>: 10:45:46.590193\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 122, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.590748\n",
      "{'response': 'ok', 'seq_num': 122}\n",
      "\n",
      "\n",
      "=>: 10:45:46.591613\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 123, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.592754\n",
      "{'response': 'ok', 'seq_num': 123}\n",
      "\n",
      "\n",
      "=>: 10:45:46.593041\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 124, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.593627\n",
      "{'response': 'ok', 'seq_num': 124}\n",
      "\n",
      "\n",
      "=>: 10:45:46.593854\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 125, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.594407\n",
      "{'response': 'ok', 'seq_num': 125}\n",
      "\n",
      "\n",
      "=>: 10:45:46.594628\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 126, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.595224\n",
      "{'response': 'ok', 'seq_num': 126}\n",
      "\n",
      "\n",
      "=>: 10:45:46.595465\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 127, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.596078\n",
      "{'response': 'ok', 'seq_num': 127}\n",
      "\n",
      "\n",
      "=>: 10:45:46.596314\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 128, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.596894\n",
      "{'response': 'ok', 'seq_num': 128}\n",
      "\n",
      "\n",
      "=>: 10:45:46.597128\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 129, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.597678\n",
      "{'response': 'ok', 'seq_num': 129}\n",
      "\n",
      "\n",
      "=>: 10:45:46.597910\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 130, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.598395\n",
      "{'response': 'ok', 'seq_num': 130}\n",
      "\n",
      "\n",
      "=>: 10:45:46.598545\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 131, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.598911\n",
      "{'response': 'ok', 'seq_num': 131}\n",
      "\n",
      "\n",
      "=>: 10:45:46.599039\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 132, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.599358\n",
      "{'response': 'ok', 'seq_num': 132}\n",
      "\n",
      "\n",
      "=>: 10:45:46.599470\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 133, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.599778\n",
      "{'response': 'ok', 'seq_num': 133}\n",
      "\n",
      "\n",
      "=>: 10:45:46.599947\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 134, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.600588\n",
      "{'response': 'ok', 'seq_num': 134}\n",
      "\n",
      "\n",
      "=>: 10:45:46.600807\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 135, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.601322\n",
      "{'response': 'ok', 'seq_num': 135}\n",
      "\n",
      "\n",
      "=>: 10:45:46.601516\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 136, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.601971\n",
      "{'response': 'ok', 'seq_num': 136}\n",
      "\n",
      "\n",
      "=>: 10:45:46.602112\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 137, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.602433\n",
      "{'response': 'ok', 'seq_num': 137}\n",
      "\n",
      "\n",
      "=>: 10:45:46.602550\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 138, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.602869\n",
      "{'response': 'ok', 'seq_num': 138}\n",
      "\n",
      "\n",
      "=>: 10:45:46.602983\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 139, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.603289\n",
      "{'response': 'ok', 'seq_num': 139}\n",
      "\n",
      "\n",
      "=>: 10:45:46.603399\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 140, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.604359\n",
      "{'response': 'ok', 'seq_num': 140}\n",
      "\n",
      "\n",
      "=>: 10:45:46.604583\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 141, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.605058\n",
      "{'response': 'ok', 'seq_num': 141}\n",
      "\n",
      "\n",
      "=>: 10:45:46.605249\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 142, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.605688\n",
      "{'response': 'ok', 'seq_num': 142}\n",
      "\n",
      "\n",
      "=>: 10:45:46.606054\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 143, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.606539\n",
      "{'response': 'ok', 'seq_num': 143}\n",
      "\n",
      "\n",
      "=>: 10:45:46.606737\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 144, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.607169\n",
      "{'response': 'ok', 'seq_num': 144}\n",
      "\n",
      "\n",
      "=>: 10:45:46.607373\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 145, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.608401\n",
      "{'response': 'ok', 'seq_num': 145}\n",
      "\n",
      "\n",
      "=>: 10:45:46.608563\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 146, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.608910\n",
      "{'response': 'ok', 'seq_num': 146}\n",
      "\n",
      "\n",
      "=>: 10:45:46.609062\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 147, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.609413\n",
      "{'response': 'ok', 'seq_num': 147}\n",
      "\n",
      "\n",
      "=>: 10:45:46.609600\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 148, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.609922\n",
      "{'response': 'ok', 'seq_num': 148}\n",
      "\n",
      "\n",
      "=>: 10:45:46.610042\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 149, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.610334\n",
      "{'response': 'ok', 'seq_num': 149}\n",
      "\n",
      "\n",
      "=>: 10:45:46.610444\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 150, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.610715\n",
      "{'response': 'ok', 'seq_num': 150}\n",
      "\n",
      "\n",
      "=>: 10:45:46.610820\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 151, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.611103\n",
      "{'response': 'ok', 'seq_num': 151}\n",
      "\n",
      "\n",
      "=>: 10:45:46.611320\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 152, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.611790\n",
      "{'response': 'ok', 'seq_num': 152}\n",
      "\n",
      "\n",
      "=>: 10:45:46.611985\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 153, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.612522\n",
      "{'response': 'ok', 'seq_num': 153}\n",
      "\n",
      "\n",
      "=>: 10:45:46.612723\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 154, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.613231\n",
      "{'response': 'ok', 'seq_num': 154}\n",
      "\n",
      "\n",
      "=>: 10:45:46.613427\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 155, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.613938\n",
      "{'response': 'ok', 'seq_num': 155}\n",
      "\n",
      "\n",
      "=>: 10:45:46.614129\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 156, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.614645\n",
      "{'response': 'ok', 'seq_num': 156}\n",
      "\n",
      "\n",
      "=>: 10:45:46.614847\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 157, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.615428\n",
      "{'response': 'ok', 'seq_num': 157}\n",
      "\n",
      "\n",
      "=>: 10:45:46.615679\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 158, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.616289\n",
      "{'response': 'ok', 'seq_num': 158}\n",
      "\n",
      "\n",
      "=>: 10:45:46.616524\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 159, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.616946\n",
      "{'response': 'ok', 'seq_num': 159}\n",
      "\n",
      "\n",
      "=>: 10:45:46.617085\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 160, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.617393\n",
      "{'response': 'ok', 'seq_num': 160}\n",
      "\n",
      "\n",
      "=>: 10:45:46.617510\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 161, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.618016\n",
      "{'response': 'ok', 'seq_num': 161}\n",
      "\n",
      "\n",
      "=>: 10:45:46.618252\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 162, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.620068\n",
      "{'response': 'ok', 'seq_num': 162}\n",
      "\n",
      "\n",
      "=>: 10:45:46.620365\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 163, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.620996\n",
      "{'response': 'ok', 'seq_num': 163}\n",
      "\n",
      "\n",
      "=>: 10:45:46.621233\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 164, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.622157\n",
      "{'response': 'ok', 'seq_num': 164}\n",
      "\n",
      "\n",
      "=>: 10:45:46.622456\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 165, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.623290\n",
      "{'response': 'ok', 'seq_num': 165}\n",
      "\n",
      "\n",
      "=>: 10:45:46.623569\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 166, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.624290\n",
      "{'response': 'ok', 'seq_num': 166}\n",
      "\n",
      "\n",
      "=>: 10:45:46.624571\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 167, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.625121\n",
      "{'response': 'ok', 'seq_num': 167}\n",
      "\n",
      "\n",
      "=>: 10:45:46.625347\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 168, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.625802\n",
      "{'response': 'ok', 'seq_num': 168}\n",
      "\n",
      "\n",
      "=>: 10:45:46.625945\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 169, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.626259\n",
      "{'response': 'ok', 'seq_num': 169}\n",
      "\n",
      "\n",
      "=>: 10:45:46.626382\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 170, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.626671\n",
      "{'response': 'ok', 'seq_num': 170}\n",
      "\n",
      "\n",
      "=>: 10:45:46.626785\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 171, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.627068\n",
      "{'response': 'ok', 'seq_num': 171}\n",
      "\n",
      "\n",
      "=>: 10:45:46.627178\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 172, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.627571\n",
      "{'response': 'ok', 'seq_num': 172}\n",
      "\n",
      "\n",
      "=>: 10:45:46.627771\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 173, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.628305\n",
      "{'response': 'ok', 'seq_num': 173}\n",
      "\n",
      "\n",
      "=>: 10:45:46.628448\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 174, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.628759\n",
      "{'response': 'ok', 'seq_num': 174}\n",
      "\n",
      "\n",
      "=>: 10:45:46.628879\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 175, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.629171\n",
      "{'response': 'ok', 'seq_num': 175}\n",
      "\n",
      "\n",
      "=>: 10:45:46.629281\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 176, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.629553\n",
      "{'response': 'ok', 'seq_num': 176}\n",
      "\n",
      "\n",
      "=>: 10:45:46.629658\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 177, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.629928\n",
      "{'response': 'ok', 'seq_num': 177}\n",
      "\n",
      "\n",
      "=>: 10:45:46.630034\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 178, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.630304\n",
      "{'response': 'ok', 'seq_num': 178}\n",
      "\n",
      "\n",
      "=>: 10:45:46.630410\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 179, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.630684\n",
      "{'response': 'ok', 'seq_num': 179}\n",
      "\n",
      "\n",
      "=>: 10:45:46.630788\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 180, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.631157\n",
      "{'response': 'ok', 'seq_num': 180}\n",
      "\n",
      "\n",
      "=>: 10:45:46.631349\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 181, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.631786\n",
      "{'response': 'ok', 'seq_num': 181}\n",
      "\n",
      "\n",
      "=>: 10:45:46.631915\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 182, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.632216\n",
      "{'response': 'ok', 'seq_num': 182}\n",
      "\n",
      "\n",
      "=>: 10:45:46.632332\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 183, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.632646\n",
      "{'response': 'ok', 'seq_num': 183}\n",
      "\n",
      "\n",
      "=>: 10:45:46.632756\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 184, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.633040\n",
      "{'response': 'ok', 'seq_num': 184}\n",
      "\n",
      "\n",
      "=>: 10:45:46.633148\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 185, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.633421\n",
      "{'response': 'ok', 'seq_num': 185}\n",
      "\n",
      "\n",
      "=>: 10:45:46.633525\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 186, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.633819\n",
      "{'response': 'ok', 'seq_num': 186}\n",
      "\n",
      "\n",
      "=>: 10:45:46.633922\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 187, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.634188\n",
      "{'response': 'ok', 'seq_num': 187}\n",
      "\n",
      "\n",
      "=>: 10:45:46.634291\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 188, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.634564\n",
      "{'response': 'ok', 'seq_num': 188}\n",
      "\n",
      "\n",
      "=>: 10:45:46.634740\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 189, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.635207\n",
      "{'response': 'ok', 'seq_num': 189}\n",
      "\n",
      "\n",
      "=>: 10:45:46.635445\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 190, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.635933\n",
      "{'response': 'ok', 'seq_num': 190}\n",
      "\n",
      "\n",
      "=>: 10:45:46.636123\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 191, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.636558\n",
      "{'response': 'ok', 'seq_num': 191}\n",
      "\n",
      "\n",
      "=>: 10:45:46.636691\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 192, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.637017\n",
      "{'response': 'ok', 'seq_num': 192}\n",
      "\n",
      "\n",
      "=>: 10:45:46.637140\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 193, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.637448\n",
      "{'response': 'ok', 'seq_num': 193}\n",
      "\n",
      "\n",
      "=>: 10:45:46.637556\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 194, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.637856\n",
      "{'response': 'ok', 'seq_num': 194}\n",
      "\n",
      "\n",
      "=>: 10:45:46.637963\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 195, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.638257\n",
      "{'response': 'ok', 'seq_num': 195}\n",
      "\n",
      "\n",
      "=>: 10:45:46.638360\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 196, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.638650\n",
      "{'response': 'ok', 'seq_num': 196}\n",
      "\n",
      "\n",
      "=>: 10:45:46.638752\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 197, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.639056\n",
      "{'response': 'ok', 'seq_num': 197}\n",
      "\n",
      "\n",
      "=>: 10:45:46.639266\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 198, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.639774\n",
      "{'response': 'ok', 'seq_num': 198}\n",
      "\n",
      "\n",
      "=>: 10:45:46.639965\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 199, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.640492\n",
      "{'response': 'ok', 'seq_num': 199}\n",
      "\n",
      "\n",
      "=>: 10:45:46.640715\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 200, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.641252\n",
      "{'response': 'ok', 'seq_num': 200}\n",
      "\n",
      "\n",
      "=>: 10:45:46.641497\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 201, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.641973\n",
      "{'response': 'ok', 'seq_num': 201}\n",
      "\n",
      "\n",
      "=>: 10:45:46.642101\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 202, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.642393\n",
      "{'response': 'ok', 'seq_num': 202}\n",
      "\n",
      "\n",
      "=>: 10:45:46.642508\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 203, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.642843\n",
      "{'response': 'ok', 'seq_num': 203}\n",
      "\n",
      "\n",
      "=>: 10:45:46.642954\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 204, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.643228\n",
      "{'response': 'ok', 'seq_num': 204}\n",
      "\n",
      "\n",
      "=>: 10:45:46.643334\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 205, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.643603\n",
      "{'response': 'ok', 'seq_num': 205}\n",
      "\n",
      "\n",
      "=>: 10:45:46.643776\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 206, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.644278\n",
      "{'response': 'ok', 'seq_num': 206}\n",
      "\n",
      "\n",
      "=>: 10:45:46.644460\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 207, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.644772\n",
      "{'response': 'ok', 'seq_num': 207}\n",
      "\n",
      "\n",
      "=>: 10:45:46.644890\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 208, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.645171\n",
      "{'response': 'ok', 'seq_num': 208}\n",
      "\n",
      "\n",
      "=>: 10:45:46.645278\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 209, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.645554\n",
      "{'response': 'ok', 'seq_num': 209}\n",
      "\n",
      "\n",
      "=>: 10:45:46.645658\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 210, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.645922\n",
      "{'response': 'ok', 'seq_num': 210}\n",
      "\n",
      "\n",
      "=>: 10:45:46.646025\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 211, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.646283\n",
      "{'response': 'ok', 'seq_num': 211}\n",
      "\n",
      "\n",
      "=>: 10:45:46.646388\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 212, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.646649\n",
      "{'response': 'ok', 'seq_num': 212}\n",
      "\n",
      "\n",
      "=>: 10:45:46.646751\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 213, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.647012\n",
      "{'response': 'ok', 'seq_num': 213}\n",
      "\n",
      "\n",
      "=>: 10:45:46.647114\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 214, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.647377\n",
      "{'response': 'ok', 'seq_num': 214}\n",
      "\n",
      "\n",
      "=>: 10:45:46.647642\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 215, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.648300\n",
      "{'response': 'ok', 'seq_num': 215}\n",
      "\n",
      "\n",
      "=>: 10:45:46.648546\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 216, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.649174\n",
      "{'response': 'ok', 'seq_num': 216}\n",
      "\n",
      "\n",
      "=>: 10:45:46.649406\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 217, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.649946\n",
      "{'response': 'ok', 'seq_num': 217}\n",
      "\n",
      "\n",
      "=>: 10:45:46.650092\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 218, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.650405\n",
      "{'response': 'ok', 'seq_num': 218}\n",
      "\n",
      "\n",
      "=>: 10:45:46.650523\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 219, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.650845\n",
      "{'response': 'ok', 'seq_num': 219}\n",
      "\n",
      "\n",
      "=>: 10:45:46.650963\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 220, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.651243\n",
      "{'response': 'ok', 'seq_num': 220}\n",
      "\n",
      "\n",
      "=>: 10:45:46.651351\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 221, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.651670\n",
      "{'response': 'ok', 'seq_num': 221}\n",
      "\n",
      "\n",
      "=>: 10:45:46.651845\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 222, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.652316\n",
      "{'response': 'ok', 'seq_num': 222}\n",
      "\n",
      "\n",
      "=>: 10:45:46.652451\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 223, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.652783\n",
      "{'response': 'ok', 'seq_num': 223}\n",
      "\n",
      "\n",
      "=>: 10:45:46.652900\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 224, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.653213\n",
      "{'response': 'ok', 'seq_num': 224}\n",
      "\n",
      "\n",
      "=>: 10:45:46.653324\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 225, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.653630\n",
      "{'response': 'ok', 'seq_num': 225}\n",
      "\n",
      "\n",
      "=>: 10:45:46.653740\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 226, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.654049\n",
      "{'response': 'ok', 'seq_num': 226}\n",
      "\n",
      "\n",
      "=>: 10:45:46.654155\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 227, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.654463\n",
      "{'response': 'ok', 'seq_num': 227}\n",
      "\n",
      "\n",
      "=>: 10:45:46.654568\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 228, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.654888\n",
      "{'response': 'ok', 'seq_num': 228}\n",
      "\n",
      "\n",
      "=>: 10:45:46.654994\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 229, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.655295\n",
      "{'response': 'ok', 'seq_num': 229}\n",
      "\n",
      "\n",
      "=>: 10:45:46.655398\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 230, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.655885\n",
      "{'response': 'ok', 'seq_num': 230}\n",
      "\n",
      "\n",
      "=>: 10:45:46.656109\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 231, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.656442\n",
      "{'response': 'ok', 'seq_num': 231}\n",
      "\n",
      "\n",
      "=>: 10:45:46.656566\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 232, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.656860\n",
      "{'response': 'ok', 'seq_num': 232}\n",
      "\n",
      "\n",
      "=>: 10:45:46.656972\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 233, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.657287\n",
      "{'response': 'ok', 'seq_num': 233}\n",
      "\n",
      "\n",
      "=>: 10:45:46.657398\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 234, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.657670\n",
      "{'response': 'ok', 'seq_num': 234}\n",
      "\n",
      "\n",
      "=>: 10:45:46.657776\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 235, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.658065\n",
      "{'response': 'ok', 'seq_num': 235}\n",
      "\n",
      "\n",
      "=>: 10:45:46.658173\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 236, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.658439\n",
      "{'response': 'ok', 'seq_num': 236}\n",
      "\n",
      "\n",
      "=>: 10:45:46.658544\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 237, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.658804\n",
      "{'response': 'ok', 'seq_num': 237}\n",
      "\n",
      "\n",
      "=>: 10:45:46.658906\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 238, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.659171\n",
      "{'response': 'ok', 'seq_num': 238}\n",
      "\n",
      "\n",
      "=>: 10:45:46.659299\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 239, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.659747\n",
      "{'response': 'ok', 'seq_num': 239}\n",
      "\n",
      "\n",
      "=>: 10:45:46.659984\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 240, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.660514\n",
      "{'response': 'ok', 'seq_num': 240}\n",
      "\n",
      "\n",
      "=>: 10:45:46.660713\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 241, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.661772\n",
      "{'response': 'ok', 'seq_num': 241}\n",
      "\n",
      "\n",
      "=>: 10:45:46.661928\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 242, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.662287\n",
      "{'response': 'ok', 'seq_num': 242}\n",
      "\n",
      "\n",
      "=>: 10:45:46.662424\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 243, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.662765\n",
      "{'response': 'ok', 'seq_num': 243}\n",
      "\n",
      "\n",
      "=>: 10:45:46.662883\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 244, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.663204\n",
      "{'response': 'ok', 'seq_num': 244}\n",
      "\n",
      "\n",
      "=>: 10:45:46.663316\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 245, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.663621\n",
      "{'response': 'ok', 'seq_num': 245}\n",
      "\n",
      "\n",
      "=>: 10:45:46.663769\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 246, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.664210\n",
      "{'response': 'ok', 'seq_num': 246}\n",
      "\n",
      "\n",
      "=>: 10:45:46.664404\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 247, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.664946\n",
      "{'response': 'ok', 'seq_num': 247}\n",
      "\n",
      "\n",
      "=>: 10:45:46.665137\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 248, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.665786\n",
      "{'response': 'ok', 'seq_num': 248}\n",
      "\n",
      "\n",
      "=>: 10:45:46.666002\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 249, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.666334\n",
      "{'response': 'ok', 'seq_num': 249}\n",
      "\n",
      "\n",
      "=>: 10:45:46.666463\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 250, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.666760\n",
      "{'response': 'ok', 'seq_num': 250}\n",
      "\n",
      "\n",
      "=>: 10:45:46.666875\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 251, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.667149\n",
      "{'response': 'ok', 'seq_num': 251}\n",
      "\n",
      "\n",
      "=>: 10:45:46.667256\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 252, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.667532\n",
      "{'response': 'ok', 'seq_num': 252}\n",
      "\n",
      "\n",
      "=>: 10:45:46.667638\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 253, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.667900\n",
      "{'response': 'ok', 'seq_num': 253}\n",
      "\n",
      "\n",
      "=>: 10:45:46.668003\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 254, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.668415\n",
      "{'response': 'ok', 'seq_num': 254}\n",
      "\n",
      "\n",
      "=>: 10:45:46.668604\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 255, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.669106\n",
      "{'response': 'ok', 'seq_num': 255}\n",
      "\n",
      "\n",
      "=>: 10:45:46.669296\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 256, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.669783\n",
      "{'response': 'ok', 'seq_num': 256}\n",
      "\n",
      "\n",
      "=>: 10:45:46.669916\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 257, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.670245\n",
      "{'response': 'ok', 'seq_num': 257}\n",
      "\n",
      "\n",
      "=>: 10:45:46.670357\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 258, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.670687\n",
      "{'response': 'ok', 'seq_num': 258}\n",
      "\n",
      "\n",
      "=>: 10:45:46.670800\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 259, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.671126\n",
      "{'response': 'ok', 'seq_num': 259}\n",
      "\n",
      "\n",
      "=>: 10:45:46.671234\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 260, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.671536\n",
      "{'response': 'ok', 'seq_num': 260}\n",
      "\n",
      "\n",
      "=>: 10:45:46.671642\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 261, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.672109\n",
      "{'response': 'ok', 'seq_num': 261}\n",
      "\n",
      "\n",
      "=>: 10:45:46.672352\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 262, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.672953\n",
      "{'response': 'ok', 'seq_num': 262}\n",
      "\n",
      "\n",
      "=>: 10:45:46.673101\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 263, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.673418\n",
      "{'response': 'ok', 'seq_num': 263}\n",
      "\n",
      "\n",
      "=>: 10:45:46.673530\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 264, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.673805\n",
      "{'response': 'ok', 'seq_num': 264}\n",
      "\n",
      "\n",
      "=>: 10:45:46.673914\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 265, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.674187\n",
      "{'response': 'ok', 'seq_num': 265}\n",
      "\n",
      "\n",
      "=>: 10:45:46.674297\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 266, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.674672\n",
      "{'response': 'ok', 'seq_num': 266}\n",
      "\n",
      "\n",
      "=>: 10:45:46.674793\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 267, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.675072\n",
      "{'response': 'ok', 'seq_num': 267}\n",
      "\n",
      "\n",
      "=>: 10:45:46.675180\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 268, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.675449\n",
      "{'response': 'ok', 'seq_num': 268}\n",
      "\n",
      "\n",
      "=>: 10:45:46.675600\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 269, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.676066\n",
      "{'response': 'ok', 'seq_num': 269}\n",
      "\n",
      "\n",
      "=>: 10:45:46.676249\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 270, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.676719\n",
      "{'response': 'ok', 'seq_num': 270}\n",
      "\n",
      "\n",
      "=>: 10:45:46.676855\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 271, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.677188\n",
      "{'response': 'ok', 'seq_num': 271}\n",
      "\n",
      "\n",
      "=>: 10:45:46.677302\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 272, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.677615\n",
      "{'response': 'ok', 'seq_num': 272}\n",
      "\n",
      "\n",
      "=>: 10:45:46.677724\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 273, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.678065\n",
      "{'response': 'ok', 'seq_num': 273}\n",
      "\n",
      "\n",
      "=>: 10:45:46.678196\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 274, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.678492\n",
      "{'response': 'ok', 'seq_num': 274}\n",
      "\n",
      "\n",
      "=>: 10:45:46.678603\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 275, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.678894\n",
      "{'response': 'ok', 'seq_num': 275}\n",
      "\n",
      "\n",
      "=>: 10:45:46.679005\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 276, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.679285\n",
      "{'response': 'ok', 'seq_num': 276}\n",
      "\n",
      "\n",
      "=>: 10:45:46.679506\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 277, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.679962\n",
      "{'response': 'ok', 'seq_num': 277}\n",
      "\n",
      "\n",
      "=>: 10:45:46.680158\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 278, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.680779\n",
      "{'response': 'ok', 'seq_num': 278}\n",
      "\n",
      "\n",
      "=>: 10:45:46.680948\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 279, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.681415\n",
      "{'response': 'ok', 'seq_num': 279}\n",
      "\n",
      "\n",
      "=>: 10:45:46.681646\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 280, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.682144\n",
      "{'response': 'ok', 'seq_num': 280}\n",
      "\n",
      "\n",
      "=>: 10:45:46.682334\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 281, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.682687\n",
      "{'response': 'ok', 'seq_num': 281}\n",
      "\n",
      "\n",
      "=>: 10:45:46.682824\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 282, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.683126\n",
      "{'response': 'ok', 'seq_num': 282}\n",
      "\n",
      "\n",
      "=>: 10:45:46.683241\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 283, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.683521\n",
      "{'response': 'ok', 'seq_num': 283}\n",
      "\n",
      "\n",
      "=>: 10:45:46.683628\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 284, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.683899\n",
      "{'response': 'ok', 'seq_num': 284}\n",
      "\n",
      "\n",
      "=>: 10:45:46.684013\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 285, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.684321\n",
      "{'response': 'ok', 'seq_num': 285}\n",
      "\n",
      "\n",
      "=>: 10:45:46.684568\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 286, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.685059\n",
      "{'response': 'ok', 'seq_num': 286}\n",
      "\n",
      "\n",
      "=>: 10:45:46.685254\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 287, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.685753\n",
      "{'response': 'ok', 'seq_num': 287}\n",
      "\n",
      "\n",
      "=>: 10:45:46.685944\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 288, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.686385\n",
      "{'response': 'ok', 'seq_num': 288}\n",
      "\n",
      "\n",
      "=>: 10:45:46.686517\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 289, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.686875\n",
      "{'response': 'ok', 'seq_num': 289}\n",
      "\n",
      "\n",
      "=>: 10:45:46.686994\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 290, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.687310\n",
      "{'response': 'ok', 'seq_num': 290}\n",
      "\n",
      "\n",
      "=>: 10:45:46.687425\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 291, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.687737\n",
      "{'response': 'ok', 'seq_num': 291}\n",
      "\n",
      "\n",
      "=>: 10:45:46.687848\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 292, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.688260\n",
      "{'response': 'ok', 'seq_num': 292}\n",
      "\n",
      "\n",
      "=>: 10:45:46.688466\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 293, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.689055\n",
      "{'response': 'ok', 'seq_num': 293}\n",
      "\n",
      "\n",
      "=>: 10:45:46.689212\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 294, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.689553\n",
      "{'response': 'ok', 'seq_num': 294}\n",
      "\n",
      "\n",
      "=>: 10:45:46.689689\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 295, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.690016\n",
      "{'response': 'ok', 'seq_num': 295}\n",
      "\n",
      "\n",
      "=>: 10:45:46.690149\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 296, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.690503\n",
      "{'response': 'ok', 'seq_num': 296}\n",
      "\n",
      "\n",
      "=>: 10:45:46.690630\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 297, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.690924\n",
      "{'response': 'ok', 'seq_num': 297}\n",
      "\n",
      "\n",
      "=>: 10:45:46.691041\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 298, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.691328\n",
      "{'response': 'ok', 'seq_num': 298}\n",
      "\n",
      "\n",
      "=>: 10:45:46.691439\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 299, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.692142\n",
      "{'response': 'ok', 'seq_num': 299}\n",
      "\n",
      "\n",
      "=>: 10:45:46.692417\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 300, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.692982\n",
      "{'response': 'ok', 'seq_num': 300}\n",
      "\n",
      "\n",
      "=>: 10:45:46.693205\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 301, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.693666\n",
      "{'response': 'ok', 'seq_num': 301}\n",
      "\n",
      "\n",
      "=>: 10:45:46.693840\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 302, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.694319\n",
      "{'response': 'ok', 'seq_num': 302}\n",
      "\n",
      "\n",
      "=>: 10:45:46.694532\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 303, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.695042\n",
      "{'response': 'ok', 'seq_num': 303}\n",
      "\n",
      "\n",
      "=>: 10:45:46.695289\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 304, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.695890\n",
      "{'response': 'ok', 'seq_num': 304}\n",
      "\n",
      "\n",
      "=>: 10:45:46.696126\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 305, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.696643\n",
      "{'response': 'ok', 'seq_num': 305}\n",
      "\n",
      "\n",
      "=>: 10:45:46.696797\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 306, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.697178\n",
      "{'response': 'ok', 'seq_num': 306}\n",
      "\n",
      "\n",
      "=>: 10:45:46.697335\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 307, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.697646\n",
      "{'response': 'ok', 'seq_num': 307}\n",
      "\n",
      "\n",
      "=>: 10:45:46.697768\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 308, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.698065\n",
      "{'response': 'ok', 'seq_num': 308}\n",
      "\n",
      "\n",
      "=>: 10:45:46.698180\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 309, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.698459\n",
      "{'response': 'ok', 'seq_num': 309}\n",
      "\n",
      "\n",
      "=>: 10:45:46.698573\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 310, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.698875\n",
      "{'response': 'ok', 'seq_num': 310}\n",
      "\n",
      "\n",
      "=>: 10:45:46.699136\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 311, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.699619\n",
      "{'response': 'ok', 'seq_num': 311}\n",
      "\n",
      "\n",
      "=>: 10:45:46.699796\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 312, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.700247\n",
      "{'response': 'ok', 'seq_num': 312}\n",
      "\n",
      "\n",
      "=>: 10:45:46.700409\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 313, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.700872\n",
      "{'response': 'ok', 'seq_num': 313}\n",
      "\n",
      "\n",
      "=>: 10:45:46.701035\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 314, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.701875\n",
      "{'response': 'ok', 'seq_num': 314}\n",
      "\n",
      "\n",
      "=>: 10:45:46.702114\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 315, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.702877\n",
      "{'response': 'ok', 'seq_num': 315}\n",
      "\n",
      "\n",
      "=>: 10:45:46.703124\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 316, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.703695\n",
      "{'response': 'ok', 'seq_num': 316}\n",
      "\n",
      "\n",
      "=>: 10:45:46.703908\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 317, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.704435\n",
      "{'response': 'ok', 'seq_num': 317}\n",
      "\n",
      "\n",
      "=>: 10:45:46.704645\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 318, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.705164\n",
      "{'response': 'ok', 'seq_num': 318}\n",
      "\n",
      "\n",
      "=>: 10:45:46.705348\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 319, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.705889\n",
      "{'response': 'ok', 'seq_num': 319}\n",
      "\n",
      "\n",
      "=>: 10:45:46.706089\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 320, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.706976\n",
      "{'response': 'ok', 'seq_num': 320}\n",
      "\n",
      "\n",
      "=>: 10:45:46.707226\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 321, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.707610\n",
      "{'response': 'ok', 'seq_num': 321}\n",
      "\n",
      "\n",
      "=>: 10:45:46.707738\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 322, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.708117\n",
      "{'response': 'ok', 'seq_num': 322}\n",
      "\n",
      "\n",
      "=>: 10:45:46.708234\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 323, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.708589\n",
      "{'response': 'ok', 'seq_num': 323}\n",
      "\n",
      "\n",
      "=>: 10:45:46.708699\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 324, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.709110\n",
      "{'response': 'ok', 'seq_num': 324}\n",
      "\n",
      "\n",
      "=>: 10:45:46.709277\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 325, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.709699\n",
      "{'response': 'ok', 'seq_num': 325}\n",
      "\n",
      "\n",
      "=>: 10:45:46.709864\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 326, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.710524\n",
      "{'response': 'ok', 'seq_num': 326}\n",
      "\n",
      "\n",
      "=>: 10:45:46.710681\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 327, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.711027\n",
      "{'response': 'ok', 'seq_num': 327}\n",
      "\n",
      "\n",
      "=>: 10:45:46.711142\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 328, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.711494\n",
      "{'response': 'ok', 'seq_num': 328}\n",
      "\n",
      "\n",
      "=>: 10:45:46.711605\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 329, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.711964\n",
      "{'response': 'ok', 'seq_num': 329}\n",
      "\n",
      "\n",
      "=>: 10:45:46.712073\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 330, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.712369\n",
      "{'response': 'ok', 'seq_num': 330}\n",
      "\n",
      "\n",
      "=>: 10:45:46.712497\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 331, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.712807\n",
      "{'response': 'ok', 'seq_num': 331}\n",
      "\n",
      "\n",
      "=>: 10:45:46.712917\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 332, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.713383\n",
      "{'response': 'ok', 'seq_num': 332}\n",
      "\n",
      "\n",
      "=>: 10:45:46.713554\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 333, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.714018\n",
      "{'response': 'ok', 'seq_num': 333}\n",
      "\n",
      "\n",
      "=>: 10:45:46.714217\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 334, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.714619\n",
      "{'response': 'ok', 'seq_num': 334}\n",
      "\n",
      "\n",
      "=>: 10:45:46.714742\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 335, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.715071\n",
      "{'response': 'ok', 'seq_num': 335}\n",
      "\n",
      "\n",
      "=>: 10:45:46.715184\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 336, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.715505\n",
      "{'response': 'ok', 'seq_num': 336}\n",
      "\n",
      "\n",
      "=>: 10:45:46.715617\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 337, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.715922\n",
      "{'response': 'ok', 'seq_num': 337}\n",
      "\n",
      "\n",
      "=>: 10:45:46.716028\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 338, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.716340\n",
      "{'response': 'ok', 'seq_num': 338}\n",
      "\n",
      "\n",
      "=>: 10:45:46.716446\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 339, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.716746\n",
      "{'response': 'ok', 'seq_num': 339}\n",
      "\n",
      "\n",
      "=>: 10:45:46.716851\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 340, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.717170\n",
      "{'response': 'ok', 'seq_num': 340}\n",
      "\n",
      "\n",
      "=>: 10:45:46.717318\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 341, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.717809\n",
      "{'response': 'ok', 'seq_num': 341}\n",
      "\n",
      "\n",
      "=>: 10:45:46.717925\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 342, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.718255\n",
      "{'response': 'ok', 'seq_num': 342}\n",
      "\n",
      "\n",
      "=>: 10:45:46.718366\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 343, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.718673\n",
      "{'response': 'ok', 'seq_num': 343}\n",
      "\n",
      "\n",
      "=>: 10:45:46.718779\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 344, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.719087\n",
      "{'response': 'ok', 'seq_num': 344}\n",
      "\n",
      "\n",
      "=>: 10:45:46.719191\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 345, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.719490\n",
      "{'response': 'ok', 'seq_num': 345}\n",
      "\n",
      "\n",
      "=>: 10:45:46.719594\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 346, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.719897\n",
      "{'response': 'ok', 'seq_num': 346}\n",
      "\n",
      "\n",
      "=>: 10:45:46.720008\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 347, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.720307\n",
      "{'response': 'ok', 'seq_num': 347}\n",
      "\n",
      "\n",
      "=>: 10:45:46.720413\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 348, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.720718\n",
      "{'response': 'ok', 'seq_num': 348}\n",
      "\n",
      "\n",
      "=>: 10:45:46.720897\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 349, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.721489\n",
      "{'response': 'ok', 'seq_num': 349}\n",
      "\n",
      "\n",
      "=>: 10:45:46.721725\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 350, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.722080\n",
      "{'response': 'ok', 'seq_num': 350}\n",
      "\n",
      "\n",
      "=>: 10:45:46.722229\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 351, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.722590\n",
      "{'response': 'ok', 'seq_num': 351}\n",
      "\n",
      "\n",
      "=>: 10:45:46.722711\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 352, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.723078\n",
      "{'response': 'ok', 'seq_num': 352}\n",
      "\n",
      "\n",
      "=>: 10:45:46.723192\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 353, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.723532\n",
      "{'response': 'ok', 'seq_num': 353}\n",
      "\n",
      "\n",
      "=>: 10:45:46.723644\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 354, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.723987\n",
      "{'response': 'ok', 'seq_num': 354}\n",
      "\n",
      "\n",
      "=>: 10:45:46.724096\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 355, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.724436\n",
      "{'response': 'ok', 'seq_num': 355}\n",
      "\n",
      "\n",
      "=>: 10:45:46.724610\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 356, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.724923\n",
      "{'response': 'ok', 'seq_num': 356}\n",
      "\n",
      "\n",
      "=>: 10:45:46.725035\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 357, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.725317\n",
      "{'response': 'ok', 'seq_num': 357}\n",
      "\n",
      "\n",
      "=>: 10:45:46.725424\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 358, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.725709\n",
      "{'response': 'ok', 'seq_num': 358}\n",
      "\n",
      "\n",
      "=>: 10:45:46.725816\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 359, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.726093\n",
      "{'response': 'ok', 'seq_num': 359}\n",
      "\n",
      "\n",
      "=>: 10:45:46.726209\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 360, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.726509\n",
      "{'response': 'ok', 'seq_num': 360}\n",
      "\n",
      "\n",
      "=>: 10:45:46.726621\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 361, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.726949\n",
      "{'response': 'ok', 'seq_num': 361}\n",
      "\n",
      "\n",
      "=>: 10:45:46.727058\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 362, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.727450\n",
      "{'response': 'ok', 'seq_num': 362}\n",
      "\n",
      "\n",
      "=>: 10:45:46.727562\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 363, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.727904\n",
      "{'response': 'ok', 'seq_num': 363}\n",
      "\n",
      "\n",
      "=>: 10:45:46.728012\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 364, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.728319\n",
      "{'response': 'ok', 'seq_num': 364}\n",
      "\n",
      "\n",
      "=>: 10:45:46.728439\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 365, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.728736\n",
      "{'response': 'ok', 'seq_num': 365}\n",
      "\n",
      "\n",
      "=>: 10:45:46.728843\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 366, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.729123\n",
      "{'response': 'ok', 'seq_num': 366}\n",
      "\n",
      "\n",
      "=>: 10:45:46.729250\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 367, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.729546\n",
      "{'response': 'ok', 'seq_num': 367}\n",
      "\n",
      "\n",
      "=>: 10:45:46.729656\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 368, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.729937\n",
      "{'response': 'ok', 'seq_num': 368}\n",
      "\n",
      "\n",
      "=>: 10:45:46.730048\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 369, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.730372\n",
      "{'response': 'ok', 'seq_num': 369}\n",
      "\n",
      "\n",
      "=>: 10:45:46.730497\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 370, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.730865\n",
      "{'response': 'ok', 'seq_num': 370}\n",
      "\n",
      "\n",
      "=>: 10:45:46.731001\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 371, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.731463\n",
      "{'response': 'ok', 'seq_num': 371}\n",
      "\n",
      "\n",
      "=>: 10:45:46.731613\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 372, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.732035\n",
      "{'response': 'ok', 'seq_num': 372}\n",
      "\n",
      "\n",
      "=>: 10:45:46.732256\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 373, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.732638\n",
      "{'response': 'ok', 'seq_num': 373}\n",
      "\n",
      "\n",
      "=>: 10:45:46.732774\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 374, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.733114\n",
      "{'response': 'ok', 'seq_num': 374}\n",
      "\n",
      "\n",
      "=>: 10:45:46.733249\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 375, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.733561\n",
      "{'response': 'ok', 'seq_num': 375}\n",
      "\n",
      "\n",
      "=>: 10:45:46.733686\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 376, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.733987\n",
      "{'response': 'ok', 'seq_num': 376}\n",
      "\n",
      "\n",
      "=>: 10:45:46.734134\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 377, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.734462\n",
      "{'response': 'ok', 'seq_num': 377}\n",
      "\n",
      "\n",
      "=>: 10:45:46.734593\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 378, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.734913\n",
      "{'response': 'ok', 'seq_num': 378}\n",
      "\n",
      "\n",
      "=>: 10:45:46.735042\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 379, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.735360\n",
      "{'response': 'ok', 'seq_num': 379}\n",
      "\n",
      "\n",
      "=>: 10:45:46.735487\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 380, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.735791\n",
      "{'response': 'ok', 'seq_num': 380}\n",
      "\n",
      "\n",
      "=>: 10:45:46.735909\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 381, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.736201\n",
      "{'response': 'ok', 'seq_num': 381}\n",
      "\n",
      "\n",
      "=>: 10:45:46.736314\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 382, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.736603\n",
      "{'response': 'ok', 'seq_num': 382}\n",
      "\n",
      "\n",
      "=>: 10:45:46.736724\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 383, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.737013\n",
      "{'response': 'ok', 'seq_num': 383}\n",
      "\n",
      "\n",
      "=>: 10:45:46.737122\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 384, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.737513\n",
      "{'response': 'ok', 'seq_num': 384}\n",
      "\n",
      "\n",
      "=>: 10:45:46.737641\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 385, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.737995\n",
      "{'response': 'ok', 'seq_num': 385}\n",
      "\n",
      "\n",
      "=>: 10:45:46.738160\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 386, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.738518\n",
      "{'response': 'ok', 'seq_num': 386}\n",
      "\n",
      "\n",
      "=>: 10:45:46.738646\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 387, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.738998\n",
      "{'response': 'ok', 'seq_num': 387}\n",
      "\n",
      "\n",
      "=>: 10:45:46.739151\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 388, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.739703\n",
      "{'response': 'ok', 'seq_num': 388}\n",
      "\n",
      "\n",
      "=>: 10:45:46.739876\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 389, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.740218\n",
      "{'response': 'ok', 'seq_num': 389}\n",
      "\n",
      "\n",
      "=>: 10:45:46.740348\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 390, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.740661\n",
      "{'response': 'ok', 'seq_num': 390}\n",
      "\n",
      "\n",
      "=>: 10:45:46.740783\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 391, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.741089\n",
      "{'response': 'ok', 'seq_num': 391}\n",
      "\n",
      "\n",
      "=>: 10:45:46.741208\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 392, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.741691\n",
      "{'response': 'ok', 'seq_num': 392}\n",
      "\n",
      "\n",
      "=>: 10:45:46.741848\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 393, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.742192\n",
      "{'response': 'ok', 'seq_num': 393}\n",
      "\n",
      "\n",
      "=>: 10:45:46.742331\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 394, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.742789\n",
      "{'response': 'ok', 'seq_num': 394}\n",
      "\n",
      "\n",
      "=>: 10:45:46.742949\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 395, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.743304\n",
      "{'response': 'ok', 'seq_num': 395}\n",
      "\n",
      "\n",
      "=>: 10:45:46.743427\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 396, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.743715\n",
      "{'response': 'ok', 'seq_num': 396}\n",
      "\n",
      "\n",
      "=>: 10:45:46.743847\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 397, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.744143\n",
      "{'response': 'ok', 'seq_num': 397}\n",
      "\n",
      "\n",
      "=>: 10:45:46.744258\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 398, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.744832\n",
      "{'response': 'ok', 'seq_num': 398}\n",
      "\n",
      "\n",
      "=>: 10:45:46.744969\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 399, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.746226\n",
      "{'is_running': False, 'response': 'current_tasks', 'tasks': []}\n",
      "\n",
      "<=: 10:45:46.746389\n",
      "{'response': 'ok', 'seq_num': 399}\n",
      "\n",
      "\n",
      "=>: 10:45:46.746507\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 400, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.747490\n",
      "{'response': 'ok', 'seq_num': 400}\n",
      "\n",
      "\n",
      "=>: 10:45:46.756513\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 401, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.757158\n",
      "{'response': 'ok', 'seq_num': 401}\n",
      "\n",
      "\n",
      "=>: 10:45:46.757397\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 402, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.758074\n",
      "{'response': 'ok', 'seq_num': 402}\n",
      "\n",
      "\n",
      "=>: 10:45:46.758224\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 403, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.760893\n",
      "{'response': 'ok', 'seq_num': 403}\n",
      "\n",
      "\n",
      "=>: 10:45:46.761086\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 404, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.762074\n",
      "{'response': 'ok', 'seq_num': 404}\n",
      "\n",
      "\n",
      "=>: 10:45:46.762226\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 405, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.762698\n",
      "{'response': 'ok', 'seq_num': 405}\n",
      "\n",
      "\n",
      "=>: 10:45:46.762886\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 406, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.763308\n",
      "{'response': 'ok', 'seq_num': 406}\n",
      "\n",
      "\n",
      "=>: 10:45:46.763496\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 407, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.763910\n",
      "{'response': 'ok', 'seq_num': 407}\n",
      "\n",
      "\n",
      "=>: 10:45:46.764100\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 408, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.764505\n",
      "{'response': 'ok', 'seq_num': 408}\n",
      "\n",
      "\n",
      "=>: 10:45:46.764685\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 409, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.765156\n",
      "{'response': 'ok', 'seq_num': 409}\n",
      "\n",
      "\n",
      "=>: 10:45:46.765351\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 410, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.765847\n",
      "{'response': 'ok', 'seq_num': 410}\n",
      "\n",
      "\n",
      "=>: 10:45:46.766069\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 411, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.766517\n",
      "{'response': 'ok', 'seq_num': 411}\n",
      "\n",
      "\n",
      "=>: 10:45:46.766694\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 412, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.767168\n",
      "{'response': 'ok', 'seq_num': 412}\n",
      "\n",
      "\n",
      "=>: 10:45:46.767349\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 413, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.768225\n",
      "{'response': 'ok', 'seq_num': 413}\n",
      "\n",
      "\n",
      "=>: 10:45:46.768451\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 414, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.768935\n",
      "{'response': 'ok', 'seq_num': 414}\n",
      "\n",
      "\n",
      "=>: 10:45:46.769129\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 415, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.769761\n",
      "{'response': 'ok', 'seq_num': 415}\n",
      "\n",
      "\n",
      "=>: 10:45:46.770356\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 416, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.771568\n",
      "{'response': 'ok', 'seq_num': 416}\n",
      "\n",
      "\n",
      "=>: 10:45:46.771799\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 417, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.772510\n",
      "{'response': 'ok', 'seq_num': 417}\n",
      "\n",
      "\n",
      "=>: 10:45:46.772694\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 418, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.773146\n",
      "{'response': 'ok', 'seq_num': 418}\n",
      "\n",
      "\n",
      "=>: 10:45:46.773293\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 419, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.774125\n",
      "{'response': 'ok', 'seq_num': 419}\n",
      "\n",
      "\n",
      "=>: 10:45:46.774331\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 420, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.778524\n",
      "{'response': 'ok', 'seq_num': 420}\n",
      "\n",
      "\n",
      "=>: 10:45:46.778759\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 421, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.779152\n",
      "{'response': 'ok', 'seq_num': 421}\n",
      "\n",
      "\n",
      "=>: 10:45:46.779278\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 422, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.779633\n",
      "{'response': 'ok', 'seq_num': 422}\n",
      "\n",
      "\n",
      "=>: 10:45:46.779761\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 423, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.780939\n",
      "{'response': 'ok', 'seq_num': 423}\n",
      "\n",
      "\n",
      "=>: 10:45:46.781177\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 424, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.781847\n",
      "{'response': 'ok', 'seq_num': 424}\n",
      "\n",
      "\n",
      "=>: 10:45:46.782043\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 425, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.782417\n",
      "{'response': 'ok', 'seq_num': 425}\n",
      "\n",
      "\n",
      "=>: 10:45:46.782557\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 426, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.782870\n",
      "{'response': 'ok', 'seq_num': 426}\n",
      "\n",
      "\n",
      "=>: 10:45:46.782988\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 427, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.790055\n",
      "{'response': 'ok', 'seq_num': 427}\n",
      "\n",
      "\n",
      "=>: 10:45:46.790290\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 428, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.790722\n",
      "{'response': 'ok', 'seq_num': 428}\n",
      "\n",
      "\n",
      "=>: 10:45:46.790843\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 429, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.793254\n",
      "{'response': 'ok', 'seq_num': 429}\n",
      "\n",
      "\n",
      "=>: 10:45:46.793475\n",
      "('{\"line\": 1, \"column\": 0, \"file_name\": \"dummy.lean\", \"seq_num\": 430, '\n",
      " '\"command\": \"info\"}')\n",
      "\n",
      "<=: 10:45:46.793698\n",
      "{'msgs': [{'caption': 'trace output',\n",
      "           'file_name': 'fake_lean_file1.lean',\n",
      "           'pos_col': 0,\n",
      "           'pos_line': 70,\n",
      "           'severity': 'information',\n",
      "           'text': 'Goals: 0\\n\\n\\n'},\n",
      "          {'caption': 'trace output',\n",
      "           'file_name': 'fake_lean_file1.lean',\n",
      "           'pos_col': 0,\n",
      "           'pos_line': 71,\n",
      "           'severity': 'information',\n",
      "           'text': '\\n'},\n",
      "          {'caption': 'eval result',\n",
      "           'end_pos_col': 7,\n",
      "           'end_pos_line': 75,\n",
      "           'file_name': 'fake_lean_file1.lean',\n",
      "           'pos_col': 0,\n",
      "           'pos_line': 75,\n",
      "           'severity': 'information',\n",
      "           'text': '1'}],\n",
      " 'response': 'all_messages'}\n",
      "\n",
      "<=: 10:45:46.794591\n",
      "{'response': 'ok', 'seq_num': 430}\n",
      "\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal(['u', 'v'], ['a b: Type u'],  'a = a')\n",
    "    display(lean_interface.apply_tactic(goal, 'refl', verbose=True))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "collapsed": false,
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('success',\n",
       " [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop'], conclusion='@eq.{1} Prop p p')],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('tactic_failure',\n",
       " ['done tactic failed, there are unsolved goals\\nstate:\\np q : Prop\\n⊢ p = p'],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('tactic_failure',\n",
       " [\"unknown identifier 'abc123'\",\n",
       "  \"don't know how to synthesize placeholder\\ncontext:\\np q : Prop\\n⊢ Type ?\"],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('success',\n",
       " [LeanGoal(universes=[], assumptions=['m : nat'], conclusion='@eq.{1} nat nat.zero nat.zero'),\n",
       "  LeanGoal(universes=[], assumptions=['m : nat', 'n_n : nat', 'n_ih : @eq.{1} nat n_n n_n'], conclusion='@eq.{1} nat (nat.succ n_n) (nat.succ n_n)')],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('theorem_error',\n",
       " [\"unknown identifier 'abc'\",\n",
       "  \"unknown identifier 'xyz'\",\n",
       "  \"don't know how to synthesize placeholder\\ncontext:\\n⊢ Sort ?\"],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "('theorem_error',\n",
       " [\"unknown identifier 'abc'\",\n",
       "  \"unknown identifier 'xyz'\",\n",
       "  \"don't know how to synthesize placeholder\\ncontext:\\n⊢ Sort ?\"],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# lots of examples\n",
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal1 = LeanGoal([], ['p q : Prop'],  'p = p')\n",
    "    display(lean_interface.apply_tactic(goal1, 'refl'))\n",
    "    display(lean_interface.apply_tactic(goal1, 'skip'))\n",
    "    display(lean_interface.apply_tactic(goal1, 'done'))\n",
    "    display(lean_interface.apply_tactic(goal1, 'abc123'))\n",
    "    goal2 = LeanGoal([], ['n m : nat'],  'n = n')\n",
    "    display(lean_interface.apply_tactic(goal2, 'induction n'))\n",
    "    goal3 = LeanGoal([], [], 'abc = xyz')\n",
    "    display(lean_interface.apply_tactic(goal3, 'skip'))\n",
    "    display(lean_interface.apply_tactic(goal3, 'fgh'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[('success', [], ''),\n",
       " ('success',\n",
       "  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop'], conclusion='@eq.{1} Prop p p')],\n",
       "  ''),\n",
       " ('tactic_failure',\n",
       "  ['done tactic failed, there are unsolved goals\\nstate:\\np q : Prop\\n⊢ p = p'],\n",
       "  ''),\n",
       " ('tactic_failure',\n",
       "  [\"unknown identifier 'abc123'\",\n",
       "   \"don't know how to synthesize placeholder\\ncontext:\\np q : Prop\\n⊢ Type ?\"],\n",
       "  ''),\n",
       " ('success',\n",
       "  [LeanGoal(universes=[], assumptions=['m : nat'], conclusion='@eq.{1} nat nat.zero nat.zero'),\n",
       "   LeanGoal(universes=[], assumptions=['m : nat', 'n_n : nat', 'n_ih : @eq.{1} nat n_n n_n'], conclusion='@eq.{1} nat (nat.succ n_n) (nat.succ n_n)')],\n",
       "  ''),\n",
       " ('theorem_error',\n",
       "  [\"unknown identifier 'abc'\",\n",
       "   \"unknown identifier 'xyz'\",\n",
       "   \"don't know how to synthesize placeholder\\ncontext:\\n⊢ Sort ?\"],\n",
       "  ''),\n",
       " ('theorem_error',\n",
       "  [\"unknown identifier 'abc'\",\n",
       "   \"unknown identifier 'xyz'\",\n",
       "   \"don't know how to synthesize placeholder\\ncontext:\\n⊢ Sort ?\"],\n",
       "  '')]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# examples of executing in batch\n",
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal1 = LeanGoal([], ['p q : Prop'],  'p = p')\n",
    "    goal2 = LeanGoal([], ['n m : nat'],  'n = n')\n",
    "    goal3 = LeanGoal([], [], 'abc = xyz')\n",
    "    \n",
    "    goals = [goal1, goal1, goal1, goal1, goal2, goal3, goal3]\n",
    "    tactics = ['refl', 'skip', 'done', 'abc123', 'induction n', 'skip', 'fgh']\n",
    "    \n",
    "    display(lean_interface.apply_tactic_multiple(goals, tactics))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Speed and robustness\n",
    "Unfortunately, this is quit slow."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Each call to the Lean interface takes on average 0.31146204471588135 seconds'"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# time it\n",
    "total_runs = 50\n",
    "total_time = 0\n",
    "goal = LeanGoal([], [],  'true')\n",
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    # give the system a chance to \"warm up\"\n",
    "    lean_interface.apply_tactic(goal, 'refl')\n",
    "    time.sleep(2)\n",
    "    \n",
    "    for i in range(total_runs):\n",
    "        a = time.time()\n",
    "        response = lean_interface.apply_tactic(goal, 'refl')\n",
    "        b = time.time()\n",
    "        total_time += b - a\n",
    "\"Each call to the Lean interface takes on average {} seconds\".format(total_time / total_runs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "But sending multiple calls to Lean speeds things up."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Each call to the Lean interface takes on average 0.4297070026397705 seconds'"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "'Each goal/tactic pair (w/ batch size 32) takes on average 0.013428343832492829 seconds'"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# time running multiple goal-tactics at a time \n",
    "total_runs = 50\n",
    "batch_size = 32\n",
    "total_time = 0\n",
    "goals = [LeanGoal([], [],  'true')] * batch_size\n",
    "tactics = ['refl'] * batch_size\n",
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    # give the system a chance to \"warm up\"\n",
    "    lean_interface.apply_tactic(LeanGoal([], [],  'true'), 'refl')\n",
    "    time.sleep(2)\n",
    "    \n",
    "    for i in range(total_runs):\n",
    "        a = time.time()\n",
    "        response = lean_interface.apply_tactic_multiple(goals, tactics)\n",
    "        b = time.time()\n",
    "        total_time += b - a\n",
    "display(\"Each call to the Lean interface takes on average {} seconds\".format(total_time / total_runs))\n",
    "display(\"Each goal/tactic pair (w/ batch size {}) takes on average {} seconds\".format(batch_size, total_time / total_runs / batch_size))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It is very difficult to make this process robust. If one is not careful, the results returned by `apply_tactic_multiple` could be for a previous call to the method.  There are ways to get around this, but if one is not careful they would significantly increase Lean's memory usage over time.  (For example, using a new file name for every \"sync\" request would be bad, since Lean caches the results of each file.)  This is a test that `apply_tactic_multiple` is robust."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Passed tests'"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# test robustness.  Make sure we are getting correct results back \n",
    "# and not results for a previous request.\n",
    "rounds = 100\n",
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    for r in range(rounds):\n",
    "        count = rounds - r\n",
    "        goals = [LeanGoal([], ['p_{}_{} : Prop'.format(r, i)],  'p_{}_{}'.format(r, i)) for i in range(count)]\n",
    "        \n",
    "        if r % 3 == 0:\n",
    "            tactics = ['skip' for _ in range(count)]\n",
    "            results = lean_interface.apply_tactic_multiple(goals, tactics)\n",
    "            assert len(results) == count\n",
    "            for i, (response, new_goals, _) in enumerate(results):\n",
    "                assert response == 'success'\n",
    "                assert new_goals[0].conclusion == 'p_{}_{}'.format(r, i)\n",
    "        else:\n",
    "            tactics = ['simp' for _ in range(count)]\n",
    "            results = lean_interface.apply_tactic_multiple(goals, tactics)\n",
    "            assert len(results) == count\n",
    "            for i, (response, _, _) in enumerate(results):\n",
    "                assert response == 'tactic_failure', response\n",
    "\"Passed tests\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Stepping through a full proof"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success',\n",
       " [LeanGoal(universes=[], assumptions=['m : nat'], conclusion='@eq.{1} nat (@has_add.add.{0} nat nat.has_add m nat.zero) (@has_add.add.{0} nat nat.has_add nat.zero m)'),\n",
       "  LeanGoal(universes=[], assumptions=['m : nat', 'n_n : nat', 'n_ih : @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n_n) (@has_add.add.{0} nat nat.has_add n_n m)'], conclusion='@eq.{1} nat (@has_add.add.{0} nat nat.has_add m (nat.succ n_n)) (@has_add.add.{0} nat nat.has_add (nat.succ n_n) m)')],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    display(lean_interface.apply_tactic(LeanGoal([], ['m n : nat'], \"m + n = n + m\"), \"induction n\"))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success',\n",
       " [LeanGoal(universes=[], assumptions=['n_n : nat', 'n_ih : @eq.{1} nat (@has_add.add.{0} nat nat.has_add nat.zero n_n) (@has_add.add.{0} nat nat.has_add n_n nat.zero)'], conclusion='@eq.{1} nat (@has_add.add.{0} nat nat.has_add nat.zero (nat.succ n_n)) (@has_add.add.{0} nat nat.has_add (nat.succ n_n) nat.zero)'),\n",
       "  LeanGoal(universes=[], assumptions=['n_n : nat', 'm_n : nat', 'm_ih : @eq.{1} nat (@has_add.add.{0} nat nat.has_add m_n n_n) (@has_add.add.{0} nat nat.has_add n_n m_n) → @eq.{1} nat (@has_add.add.{0} nat nat.has_add m_n (nat.succ n_n)) (@has_add.add.{0} nat nat.has_add (nat.succ n_n) m_n)', 'n_ih : @eq.{1} nat (@has_add.add.{0} nat nat.has_add (nat.succ m_n) n_n) (@has_add.add.{0} nat nat.has_add n_n (nat.succ m_n))'], conclusion='@eq.{1} nat (@has_add.add.{0} nat nat.has_add (nat.succ m_n) (nat.succ n_n)) (@has_add.add.{0} nat nat.has_add (nat.succ n_n) (nat.succ m_n))')],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    display(lean_interface.apply_tactic(\n",
    "        LeanGoal([], ['m n_n : ℕ','n_ih : m + n_n = n_n + m'], 'm + nat.succ n_n = nat.succ n_n + m'), \n",
    "        \"induction m\"))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    display(lean_interface.apply_tactic(\n",
    "        LeanGoal([], ['n_n : ℕ','n_ih : 0 + n_n = n_n + 0'],\n",
    "         '0 + nat.succ n_n = nat.succ n_n + 0'), \n",
    "        \"simp\"))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "('success', [], '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    display(lean_interface.apply_tactic(\n",
    "        LeanGoal([], ['n_n m_n : ℕ',\n",
    "         'm_ih : m_n + n_n = n_n + m_n → m_n + nat.succ n_n = nat.succ n_n + m_n',\n",
    "         'n_ih : nat.succ m_n + n_n = n_n + nat.succ m_n'],\n",
    "         'nat.succ m_n + nat.succ n_n = nat.succ n_n + nat.succ m_n'), \n",
    "        \"simp\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Creating a simple Lean solver (with breath first search) in Python"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here we put all of this together to create (a non-practical) BFS prover.  Some highlights:\n",
    "- Some tactics like `apply` take a parameter.  We search the local context for all possible things to put in this parameter.  Note, we do no type checking before sending it to Lean.  The user inputs the tactic as `apply {}` to signify that something needs to be filled in from the context.\n",
    "- Our setup assumes the tactic is only applied to the first goal.  This isn't true of all tactics, so we force this by \"treeifying\" our proof, that is adding brackets `{ ... }` where necessary.\n",
    "- Sending multiple calls to Lean at the same time makes it much faster.  This is the only difference between the \"fast\" version.\n",
    "- We provide a way to verify a proof in the end (sending the whole proof as if it was a single tactic), and also walking through the proof to get information (which might be useful for machine-learning-like training).\n",
    "- This is just a proof-of-concept and not very useful in itself."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def premises_from_goal(goal):\n",
    "    prems = []\n",
    "    for l in goal.assumptions:\n",
    "        a, _ = l.split(\":\")\n",
    "        for v in a.strip().split(\" \"):\n",
    "            prems.append(v)\n",
    "    return prems\n",
    "\n",
    "def tactic_applications(tactics, prems):\n",
    "    tacs = []\n",
    "    for t in tactics:\n",
    "        if \"{}\" in t:\n",
    "            for p in prems:\n",
    "                tacs.append(t.replace(\"{}\", p))\n",
    "        else:\n",
    "            tacs.append(t)\n",
    "    return tacs\n",
    "\n",
    "def treeify_proof(proof_list):\n",
    "    s = \"\"\n",
    "    goal_cnts = [1]  # open goal counts at each depth\n",
    "    for tactic, new_goal_cnt in proof_list:\n",
    "        while True:\n",
    "            # take goals\n",
    "            goal_cnt = goal_cnts.pop()\n",
    "\n",
    "            # if no goals at this depth, end block and take off stack again\n",
    "            if goal_cnt == 0:\n",
    "                s += \", }\"\n",
    "                continue\n",
    "            \n",
    "            if goal_cnt == 1:\n",
    "                if s: # don't put comma in front\n",
    "                    s += \", \"\n",
    "                \n",
    "            # if more than one goal, take one of them, start block and put rest back on stack\n",
    "            if goal_cnt > 1:\n",
    "                goal_cnts.append(goal_cnt - 1)\n",
    "                s += \", { \"\n",
    "            \n",
    "            break\n",
    "            \n",
    "        # apply tactic\n",
    "        s += tactic\n",
    "        \n",
    "        # put remaining goals on stack\n",
    "        goal_cnts.append(new_goal_cnt)\n",
    "            \n",
    "    return s \n",
    "\n",
    "class BreathFirstProofSearch(LeanTacticTestingInterface):\n",
    "        \n",
    "    def proof_search(self, lean_goal, tactics, verbose=False):\n",
    "        starting_goal = lean_goal\n",
    "        starting_goal_list = (starting_goal,)\n",
    "        empty_tactics = tuple()\n",
    "        goal_list_queue = collections.deque()\n",
    "        goal_list_queue.append((starting_goal_list, empty_tactics))\n",
    "\n",
    "        while goal_list_queue:\n",
    "            goal_list, ts = goal_list_queue.popleft()\n",
    "            goal = goal_list[0]\n",
    "            prems = premises_from_goal(goal)\n",
    "            all_tactics = tactic_applications(tactics, prems)\n",
    "            for t in all_tactics:\n",
    "                response, new_goals, _ = self.apply_tactic(goal, t, verbose=verbose)\n",
    "                if response == 'success':\n",
    "                    new_goal_list = tuple(new_goals) + goal_list[1:]\n",
    "                    new_ts = ts + ((t, len(new_goals)),)\n",
    "                    if not new_goal_list:\n",
    "                        return treeify_proof(new_ts)\n",
    "\n",
    "                    goal_list_queue.append((new_goal_list, new_ts))\n",
    "        return None\n",
    "    \n",
    "    def proof_search_fast(self, lean_goal, tactics, verbose=False):\n",
    "        starting_goal = lean_goal\n",
    "        starting_goal_list = (starting_goal,)\n",
    "        empty_tactics = tuple()\n",
    "        goal_list_queue = collections.deque()\n",
    "        goal_list_queue.append((starting_goal_list, empty_tactics))\n",
    "\n",
    "        while goal_list_queue:\n",
    "            goal_list, ts = goal_list_queue.popleft()\n",
    "            goal = goal_list[0]\n",
    "            prems = premises_from_goal(goal)\n",
    "            all_tactics = tactic_applications(tactics, prems)\n",
    "            \n",
    "            # faster to batch process all apply_tactic calls\n",
    "            results = self.apply_tactic_multiple([goal] * len(all_tactics), all_tactics, verbose=verbose)\n",
    "            for t, (response, new_goals, _) in zip(all_tactics, results):\n",
    "                if response == 'success':\n",
    "                    new_goal_list = tuple(new_goals) + goal_list[1:]\n",
    "                    new_ts = ts + ((t, len(new_goals)),)\n",
    "                    if not new_goal_list:\n",
    "                        return treeify_proof(new_ts)\n",
    "\n",
    "                    goal_list_queue.append((new_goal_list, new_ts))\n",
    "        return None\n",
    "    \n",
    "    def is_valid_proof(self, goal, proof, verbose=False):\n",
    "        t = proof.replace(\"\\n\", \"\")  # treat proof as a single tactic\n",
    "        response, goals, _ = self.apply_tactic(goal, t, verbose=verbose)\n",
    "        if response == 'success' and goals == []:\n",
    "            return True\n",
    "        return goals\n",
    "    \n",
    "    def walk_through_proof(self, lean_goal, proof):\n",
    "        ts = proof.replace(\" {\", \"\").replace(\"}, \", \"\").split(\", \")\n",
    "        goals = [lean_goal]\n",
    "        for t in ts:\n",
    "            goal = goals[0]\n",
    "            print(\" Primary Goal:  \", goal)\n",
    "            print(\" Tactic applied:\", t)\n",
    "            _, new_goals, _ = self.apply_tactic(goal, t)\n",
    "            goals = new_goals + goals[1:]\n",
    "            print(\" New Goals: \", new_goals)\n",
    "            print(\" All Goals: \", goals)\n",
    "            print()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def example(goal, tactics, verbose=False):\n",
    "    with BreathFirstProofSearch() as bfs:\n",
    "        print(\"Goal:\", goal)\n",
    "        print(\"Tactics:\", tactics)\n",
    "        print()\n",
    "        start = time.time()\n",
    "        proof = bfs.proof_search_fast(goal, tactics, verbose=verbose)\n",
    "        end = time.time()\n",
    "        print(\"Time to proof:\", end-start, \"seconds\")\n",
    "        print(\"Proof:\", proof)\n",
    "        print()\n",
    "        print(\"Verified:\", bfs.is_valid_proof(goal, proof, verbose=verbose))\n",
    "        print()\n",
    "        print(\"Walk through proof:\")\n",
    "        bfs.walk_through_proof(goal, proof)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Goal: LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='p ∧ q → q ∧ p')\n",
      "Tactics: ['apply {}', 'cases {}', 'intro', 'split', 'left', 'right']\n",
      "\n",
      "Time to proof: 2.7585809230804443 seconds\n",
      "Proof: intro, cases a, split, { apply a_right, }, apply a_left\n",
      "\n",
      "Verified: True\n",
      "\n",
      "Walk through proof:\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='p ∧ q → q ∧ p')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q'], conclusion='and q p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q'], conclusion='and q p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q'], conclusion='and q p')\n",
      " Tactic applied: cases a\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='and q p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='and q p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='and q p')\n",
      " Tactic applied: split\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='q'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='q'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='q')\n",
      " Tactic applied: apply a_right\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_left : p', 'a_right : q'], conclusion='p')\n",
      " Tactic applied: apply a_left\n",
      " New Goals:  []\n",
      " All Goals:  []\n",
      "\n"
     ]
    }
   ],
   "source": [
    "example(\n",
    "    goal = LeanGoal([], ['p q r : Prop'], 'p ∧ q → q ∧ p'), \n",
    "    tactics=['apply {}', 'cases {}', 'intro', 'split', 'left', 'right'],\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Goal: LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='(p -> (q -> r)) <-> (p /\\\\ q -> r)')\n",
      "Tactics: ['apply {}', 'cases {}', 'intro', 'split', 'left', 'right']\n",
      "\n",
      "Time to proof: 7.318338871002197 seconds\n",
      "Proof: split, { intro, intro, cases a_1, apply a, { apply a_1_left, }, apply a_1_right, }, intro, intro, intro, apply a, split, { apply a_1, }, apply a_2\n",
      "\n",
      "Verified: True\n",
      "\n",
      "Walk through proof:\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='(p -> (q -> r)) <-> (p /\\\\ q -> r)')\n",
      " Tactic applied: split\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(p → q → r) → and p q → r'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(p → q → r) → and p q → r'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(p → q → r) → and p q → r')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r'], conclusion='and p q → r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r'], conclusion='and p q → r'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r'], conclusion='and p q → r')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1 : and p q'], conclusion='r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1 : and p q'], conclusion='r'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1 : and p q'], conclusion='r')\n",
      " Tactic applied: cases a_1\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='r'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='r')\n",
      " Tactic applied: apply a\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='q')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='q'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='p')\n",
      " Tactic applied: apply a_1_left\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='q'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : p → q → r', 'a_1_left : p', 'a_1_right : q'], conclusion='q')\n",
      " Tactic applied: apply a_1_right\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop'], conclusion='(and p q → r) → p → q → r')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r'], conclusion='p → q → r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r'], conclusion='p → q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r'], conclusion='p → q → r')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p'], conclusion='q → r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p'], conclusion='q → r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p'], conclusion='q → r')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='r')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='r')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='r')\n",
      " Tactic applied: apply a\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='and p q')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='and p q')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='and p q')\n",
      " Tactic applied: split\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='q')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='q')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='p')\n",
      " Tactic applied: apply a_1\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='q')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : and p q → r', 'a_1 : p', 'a_2 : q'], conclusion='q')\n",
      " Tactic applied: apply a_2\n",
      " New Goals:  []\n",
      " All Goals:  []\n",
      "\n"
     ]
    }
   ],
   "source": [
    "example(\n",
    "    goal = LeanGoal([], ['p q r : Prop'], '(p -> (q -> r)) <-> (p /\\ q -> r)'), \n",
    "    tactics=['apply {}', 'cases {}', 'intro', 'split', 'left', 'right']\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Goal: LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='¬(p ↔ ¬p)')\n",
      "Tactics: ['apply {}', 'cases {}', 'intro', 'split', 'left', 'right']\n",
      "\n",
      "Time to proof: 45.084619998931885 seconds\n",
      "Proof: intro, cases a, apply a_mp, { apply a_mpr, intro, apply a_mp, { apply a, }, apply a, }, apply a_mpr, intro, apply a_mp, { apply a, }, apply a\n",
      "\n",
      "Verified: True\n",
      "\n",
      "Walk through proof:\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p q r : Prop'], conclusion='¬(p ↔ ¬p)')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : iff p (not p)'], conclusion='false')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : iff p (not p)'], conclusion='false')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a : iff p (not p)'], conclusion='false')\n",
      " Tactic applied: cases a\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='false')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='false')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='false')\n",
      " Tactic applied: apply a_mp\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')\n",
      " Tactic applied: apply a_mpr\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false')\n",
      " Tactic applied: apply a_mp\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')\n",
      " Tactic applied: apply a\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')\n",
      " Tactic applied: apply a\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='p')\n",
      " Tactic applied: apply a_mpr\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p'], conclusion='not p')\n",
      " Tactic applied: intro\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='false')\n",
      " Tactic applied: apply a_mp\n",
      " New Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')]\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p'), LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')\n",
      " Tactic applied: apply a\n",
      " New Goals:  []\n",
      " All Goals:  [LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')]\n",
      "\n",
      " Primary Goal:   LeanGoal(universes=[], assumptions=['p : Prop', 'q : Prop', 'r : Prop', 'a_mp : p → not p', 'a_mpr : not p → p', 'a : p'], conclusion='p')\n",
      " Tactic applied: apply a\n",
      " New Goals:  []\n",
      " All Goals:  []\n",
      "\n"
     ]
    }
   ],
   "source": [
    "example(\n",
    "    goal = LeanGoal([], ['p q r : Prop'], '¬(p ↔ ¬p)'), \n",
    "    tactics=['apply {}', 'cases {}', 'intro', 'split', 'left', 'right']\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Custom printing of Lean expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Our `apply_tactic` will return a list of goals, using Lean's verbose pp.all format.  Hence, `m n : ℕ ⊢ m + n = n + m` is returned as `LeanGoal(['m n : nat'], \"@eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) (@has_add.add.{0} nat nat.has_add n m)\")`.  On one hand, this is not very readable by a human.  On the other hand, it is not as machine parsable as it could be.  It is however possible to have `apply_tactic` output the goals in other formats (or print other relevant information about the goal state).  \n",
    "\n",
    "For example, here we write a simple piece of code which prints the Lean goals just as Lean does."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "simple_custom_code = r\"\"\"\n",
    "namespace custom\n",
    " \n",
    "meta def trace_custom_state : tactic unit :=\n",
    "do \n",
    " tactic.trace_state,  -- default Lean pretty printed goals\n",
    " return ()\n",
    "\n",
    "end custom\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "2 goals\n",
      "case nat.zero\n",
      "m : ℕ\n",
      "⊢ m + 0 = 0 + m\n",
      "\n",
      "case nat.succ\n",
      "m n_n : ℕ,\n",
      "n_ih : m + n_n = n_n + m\n",
      "⊢ m + nat.succ n_n = nat.succ n_n + m\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    lean_interface.custom_code = simple_custom_code\n",
    "    _, _, custom_msg = (lean_interface.apply_tactic(LeanGoal([], ['m n : nat'], \"m + n = n + m\"), \"induction n\"))\n",
    "print(custom_msg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On the other end, we may which to print the goals as expressions.  Here is  code to do that.  (It is basically the same code we are using in the LeanTacticTestingInterface above except with s-expressions instead of pp.all formatting.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "sexp_custom_code = r\"\"\"\n",
    "namespace custom\n",
    "\n",
    "def join (sep : string) : list string → string\n",
    "| [x]     := x\n",
    "| []      := \"\"\n",
    "| (x::xs) := x ++ sep ++ join xs\n",
    "\n",
    "meta def expr_to_string (e : expr bool.tt) : tactic string :=\n",
    "do\n",
    "  return $ to_string e.to_raw_fmt\n",
    "  \n",
    "meta def local_cxt_to_string (v : expr bool.tt) : tactic string := \n",
    "do \n",
    "  tp ← tactic.infer_type v,\n",
    "  v_str ← expr_to_string v,\n",
    "  tp_str ← expr_to_string tp,\n",
    "  return $ v_str ++ \"\\n\\n\" ++ tp_str\n",
    "\n",
    "meta def goal_to_string (g : expr) : tactic string :=\n",
    "do \n",
    "  tactic.set_goals [g],\n",
    "  goal ← tactic.target,\n",
    "  local_cxt ← tactic.local_context,\n",
    "  let local_cxt_len := list.length local_cxt,\n",
    "  goal_str ← expr_to_string goal,\n",
    "  local_cxt_strs ← (list.mmap local_cxt_to_string local_cxt),\n",
    "  let s1 := goal_str ++ \"\\n\\n\",\n",
    "  let s2 := \"Local Context Vars: \" ++ (to_string local_cxt_len) ++ \"\\n\\n\",\n",
    "  let s3 := join \"\\n\\n\" local_cxt_strs,\n",
    "  return $ s1 ++ s2 ++ s3\n",
    "\n",
    "meta def state_report : tactic string :=\n",
    "do \n",
    " gs ← tactic.get_goals,\n",
    " -- loop over all goals (has effect of resetting the goal each time)\n",
    " let gs_len := list.length gs,\n",
    " goal_strings ← gs.mmap goal_to_string,\n",
    " tactic.set_goals gs,  -- set goals back\n",
    " let s := \"Goals: \" ++ (to_string gs_len) ++ \"\\n\\n\" ++ (join \"\\n\\n\" goal_strings),\n",
    " return s\n",
    " \n",
    "meta def trace_custom_state : tactic unit :=\n",
    "do \n",
    " s ← state_report,\n",
    " tactic.trace s,\n",
    " return ()\n",
    "\n",
    "end custom\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Goals: 2\n",
      "\n",
      "(app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (local_const 0._fresh.12.7660 m (const 1 []))) (const nat.zero []))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (const nat.zero [])) (local_const 0._fresh.12.7660 m (const 1 []))))\n",
      "\n",
      "Local Context Vars: 1\n",
      "\n",
      "(local_const 0._fresh.12.7660 m (const 1 []))\n",
      "\n",
      "(const nat [])\n",
      "\n",
      "(app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (local_const 0._fresh.12.7660 m (const 1 []))) (app (const nat.succ []) (local_const 0._fresh.11.2205 n_n (const 1 []))))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (app (const nat.succ []) (local_const 0._fresh.11.2205 n_n (const 1 [])))) (local_const 0._fresh.12.7660 m (const 1 []))))\n",
      "\n",
      "Local Context Vars: 3\n",
      "\n",
      "(local_const 0._fresh.12.7660 m (const 1 []))\n",
      "\n",
      "(const nat [])\n",
      "\n",
      "(local_const 0._fresh.11.2205 n_n (const 1 []))\n",
      "\n",
      "(const nat [])\n",
      "\n",
      "(local_const 0._fresh.11.2206 n_ih (const 1 []))\n",
      "\n",
      "(app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (local_const 0._fresh.12.7660 m (const 1 []))) (local_const 0._fresh.11.2205 n_n (const 1 [])))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (local_const 0._fresh.11.2205 n_n (const 1 []))) (local_const 0._fresh.12.7660 m (const 1 []))))\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    lean_interface.custom_code = sexp_custom_code\n",
    "    _, _, custom_msg = (lean_interface.apply_tactic(LeanGoal([], ['m n : nat'], \"m + n = n + m\"), \"induction n\"))\n",
    "print(custom_msg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here is code which turns each goal into a single s-expression.  The format is `(goal <intro_cnt> <expr>)` where `<expr>` is the expression and `<intro_cnt>` is the number of `intro`s one has to do on the expression to get back to the goal.  For example `m n : ℕ ⊢ m + n = n + m` is stored as `∀ m n : ℕ, m + n = n + m` so `intro_cnt` is 2 since to `intro`s are needed to reproduce `m n : ℕ ⊢ m + n = n + m`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "sexp_custom_code = r\"\"\"\n",
    "namespace custom\n",
    "\n",
    "def join (sep : string) : list string → string\n",
    "| [x]     := x\n",
    "| []      := \"\"\n",
    "| (x::xs) := x ++ sep ++ join xs\n",
    "\n",
    "meta def expr_to_string (e : expr bool.tt) : tactic string :=\n",
    "do\n",
    "  return $ to_string e.to_raw_fmt\n",
    "\n",
    "meta def goal_to_string (g : expr) : tactic string :=\n",
    "do \n",
    "  n ← tactic.revert_all,\n",
    "  goal ← tactic.target,\n",
    "  tactic.iterate_exactly n (do tactic.intro1, return ()),\n",
    "  goal_str ← expr_to_string goal,\n",
    "  let s := \"(goal \" ++ (to_string n) ++ \" \" ++ goal_str ++ \")\",\n",
    "  tactic.rotate_left 1,\n",
    "  return s\n",
    "\n",
    "meta def state_report : tactic string :=\n",
    "do \n",
    " gs ← tactic.get_goals,\n",
    " let gs_len := list.length gs,\n",
    " goal_strings ← gs.mmap goal_to_string,\n",
    " let s := join \"\\n\\n\" goal_strings,\n",
    " return s\n",
    " \n",
    "meta def trace_custom_state : tactic unit :=\n",
    "do \n",
    " s ← state_report,\n",
    " tactic.trace s,\n",
    " return ()\n",
    "\n",
    "end custom\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(goal 1 (pi m default (const nat []) (app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (var 0)) (const nat.zero []))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (const nat.zero [])) (var 0)))))\n",
      "\n",
      "(goal 3 (pi m default (const nat []) (pi n_n default (const nat []) (pi n_ih default (app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (var 1)) (var 0))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (var 0)) (var 1))) (app (app (app (const eq [1]) (const nat [])) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (var 2)) (app (const nat.succ []) (var 1)))) (app (app (app (app (const has_add.add [0]) (const nat [])) (const nat.has_add [])) (app (const nat.succ []) (var 1))) (var 2)))))))\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    lean_interface.custom_code = sexp_custom_code\n",
    "    _, _, custom_msg = (lean_interface.apply_tactic(LeanGoal([], ['m n : nat'], \"m + n = n + m\"), \"induction n\"))\n",
    "print(custom_msg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "See Lewis and Wu [interface between Mathematica and Lean](https://robertylewis.com/leanmm/) for an example of parsing Lean expressions into Mathematica code.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Current issues"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The current system relies on Leans pretty printer (with `pp.all` set to true) to output the goals which can then be fed back into Lean.  However, the pretty print (even with `pp.all` set to true) may not always output valid Lean code.  Here are some known issues:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Privately defined terms"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This mostly comes up in proof recording, but some true theorems of Lean can't be entered into our system since they refer to privately defined terms.  However, in most cases those theorems are also marked as private (or they are automatically created theorems internal to Lean)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Term blowup"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Because of subexpression sharing, sometimes the terms can blow up in size (usually because of type classes).  If they get too big, the pretty printer will replace parts with `…`,  making them unusable to Lean.  (Also, for some reason an expression with two `…`s will cause the lean server to stop, so we replace `…` with `_redacted_code_too_long_`.) As we can see, even the statement `12345678901234567890 - 12345678901234567890 = 0`, when expanded out, is too large for the pretty printer. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "New goal:\n",
      " LeanGoal(universes=[], assumptions=[], conclusion='@eq.{1} nat (@has_sub.sub.{0} nat nat.has_sub (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (… nat.has_one nat.has_add (… nat.has_add (… …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (… nat.has_add (… …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (@has_zero.zero.{0} nat nat.has_zero)')\n",
      "\n",
      "Put that new goal back in...\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "('theorem_error',\n",
       " [\"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\",\n",
       "  \"unknown identifier '_redacted_code_too_long_'\"],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal([], [], '12345678901234567890 - 12345678901234567890 = 0')\n",
    "    result = (lean_interface.apply_tactic(goal, \"skip\"))\n",
    "    goal2 = result[1][0]\n",
    "    print(\"New goal:\\n\", goal2)\n",
    "    print()\n",
    "    print(\"Put that new goal back in...\")\n",
    "    result2 = (lean_interface.apply_tactic(goal2, \"skip\"))\n",
    "    display(result2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Missing @ symbols"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`@` symbols are needed for some functions with implicit parameters.  With `pp.all` set to true, the pretty printer usually adds the `@` symbols as needed but can occasionally miss some cases.  Here is one such case."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "New goal:\n",
      " LeanGoal(universes=['u'], assumptions=[], conclusion='@eq.{(imax (u+1) u)} (Π {α : Sort u}, α → α) id.{u} id.{u}')\n",
      "\n",
      "Put that new goal back in...\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "('theorem_error',\n",
       " ['type mismatch at application\\n  eq id\\nterm\\n  id\\nhas type\\n  ?m_1 → ?m_1 : Sort u\\nbut is expected to have type\\n  Π {α : Sort u}, α → α : Sort (imax (u+1) u)'],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "What the new goal should be:\n",
      " LeanGoal(universes=['u'], assumptions=[], conclusion='@eq.{(imax (u+1) u)} (Π {α : Sort u}, α → α) @id.{u} @id.{u}')\n",
      "\n",
      "Put that new goal back in...\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "('success',\n",
       " [LeanGoal(universes=['u'], assumptions=[], conclusion='@eq.{(imax (u+1) u)} (Π {α : Sort u}, α → α) id.{u} id.{u}')],\n",
       " '')"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal(['u'], [], '@id.{u} = @id.{u}')\n",
    "    result = (lean_interface.apply_tactic(goal, \"skip\"))\n",
    "    goal2 = result[1][0]\n",
    "    print(\"New goal:\\n\", goal2)\n",
    "    print()\n",
    "    print(\"Put that new goal back in...\")\n",
    "    result2 = (lean_interface.apply_tactic(goal2, \"skip\"))\n",
    "    display(result2)\n",
    "    goal3 = LeanGoal(['u'], [], '@eq.{(imax (u+1) u)} (Π {α : Sort u}, α → α) @id.{u} @id.{u}')\n",
    "    print(\"What the new goal should be:\\n\", goal3)\n",
    "    print()\n",
    "    print(\"Put that new goal back in...\")\n",
    "    result3 = (lean_interface.apply_tactic(goal3, \"skip\"))\n",
    "    display(result3)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Extra `@` sysmbols (or maybe a missing case in the Lean parser)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Currently `@(λ {α : Type} (x : α), x)` is not valid Lean code even though `@id` is.  However, the pretty printer tries to add an @ in this case (and even without the `@` it would still be incorrect, so it is likely a bug in the Lean parser).  Consider this example:\n",
    "```lean\n",
    "theorem id_defn : @id = (λ {α : Type} (x: α), x) := by refl\n",
    "#check congr_fun id_defn bool -- @eq.{1} ((λ (x : Type), x → x) bool) (@id.{1} bool) (@(λ {α : Type} (x : α), x) bool)\n",
    "```\n",
    "If we try plugging that theorem into Lean as follows, we will get an error:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "('theorem_error', [\"invalid '@', identifier expected\"], '')\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal([], [], '@eq.{1} ((λ (x : Type), x → x) bool) (@id.{1} bool) (@(λ {α : Type} (x : α), x) bool)')\n",
    "    result = (lean_interface.apply_tactic(goal, \"skip\"))\n",
    "    print(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Implicit and type class assumptions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One can't directly enter typeclass and implicit assumptions into our framework.  We could easily add this functionality if it matters, but it shouldn't matter from the stand points of proofs."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "LeanGoal(universes=['u'], assumptions=['α : Type u', '_inst_1 : inhabited.{u+1} α'], conclusion='@Exists.{u+1} α (λ (x : α), @eq.{u+1} α x x)')\n",
      "('success', [], '')\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    goal = LeanGoal(['u'], [], '∀ {α : Type u} [inhabited α], (∃ x : α, x = x)')\n",
    "    result = (lean_interface.apply_tactic(goal, \"intro, intro\"))\n",
    "    \n",
    "    # the new goal should be \n",
    "    #  {α : Type u} [_inst_1 : inhabited.{u+1} α] ⊢ @Exists.{u+1} α (λ (x : α), @eq.{u+1} α x x)\n",
    "    # but we record it as the slightly different\n",
    "    #  (α : Type u) (_inst_1 : inhabited.{u+1} α) ⊢ @Exists.{u+1} α (λ (x : α), @eq.{u+1} α x x)\n",
    "    goal2 = result[1][0]\n",
    "    print(goal2)\n",
    "    \n",
    "    # however, the proof is the same\n",
    "    result = (lean_interface.apply_tactic(goal2, \"existsi _inst_1.default, refl\"))\n",
    "    print(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Let expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `intro` tactic can move `let` binders to the local context.  However, I don't know a way to either\n",
    "1. figure out that the assumption in the local context is associated with a let binder and know what it is assigned to, nor\n",
    "2. enter this back into Lean.\n",
    "\n",
    "Consider the following example."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "('success', [], '')\n",
      "('success', [LeanGoal(universes=[], assumptions=['x : nat'], conclusion='@eq.{1} nat x (@has_zero.zero.{0} nat nat.has_zero)')], '')\n",
      "('tactic_failure', ['invalid apply tactic, failed to unify\\n  x = 0\\nwith\\n  ?m_2 = ?m_2\\nstate:\\nx : ℕ\\n⊢ x = 0'], '')\n",
      "('success', [LeanGoal(universes=[], assumptions=['x : opt_param.{1} nat (@has_zero.zero.{0} nat nat.has_zero)'], conclusion='@eq.{1} (opt_param.{1} nat (@has_zero.zero.{0} nat nat.has_zero)) x (@has_zero.zero.{0} (opt_param.{1} nat (@has_zero.zero.{0} nat nat.has_zero)) nat.has_zero)')], '')\n"
     ]
    }
   ],
   "source": [
    "with LeanTacticTestingInterface() as lean_interface:\n",
    "    # This is solvable with this proof:\n",
    "    goal = LeanGoal([], [], 'let x : ℕ := 0 in x = 0')\n",
    "    proof = \"intro, refl\"\n",
    "    result = (lean_interface.apply_tactic(goal, proof))\n",
    "    print(result)\n",
    "    \n",
    "    # but if we do it in two steps, the assumption gets recorded incorrectly:\n",
    "    goal = LeanGoal([], [], 'let x : ℕ := 0 in x = 0')\n",
    "    result = (lean_interface.apply_tactic(goal, 'intro'))\n",
    "    print(result)\n",
    "    \n",
    "    goal2 = result[1][0]\n",
    "    result = (lean_interface.apply_tactic(goal2, 'refl'))\n",
    "    print(result)\n",
    "    \n",
    "    # moveover, even if we enter this as `x : nat := 0` in the assumptions it gets \n",
    "    # a different interpretation than we intend.  It interprets this as `x : opt_param nat 0`.\n",
    "    goal3 = LeanGoal([], ['x : nat := 0'], 'x = 0')\n",
    "    result = (lean_interface.apply_tactic(goal3, 'skip'))\n",
    "    print(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Other"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are other small issues that sometimes come up, and I'm sure more issues will arise as this is tested on all the theorems in Lean.  However, right now about in the core library, about 95% of theorems correctly load into Lean.  (I imagine that in `mathlib`, with the increased use of type classes, that this number will go down.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## TODOs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "- Code:\n",
    "    - Is there a way to make this faster?\n",
    "    - Is there a way to make this more robust?  (It works for now, but still feels rickety.)\n",
    "    - Make this production level code.  It is just a proof of concept and still quite hacky.\n",
    "- Functionality\n",
    "    - How should one enter definitions and notation?\n",
    "    - Can we even enter all Lean theorems this way (assuming there definitions and notation are stored in mathlib)?\n",
    "      - A next step would be to get a list of all theorems and see if we can apply the `skip` tactic to them.\n",
    "    - How should one enter premises?  The easiest way is to add them as assumptions to the goal.\n",
    "    - ~~What about imports, etc?~~\n",
    "    - We only apply tactics to a single goal and not a goal stack"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## What I want from Lean 4"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "- Either a REPL like interface which is fast,\n",
    "- or a way to quickly in a few milliseconds call Lean for the text of a small file and get a direct (and unambiguous) response to my request.\n",
    "- Better documentation of the communication interface\n",
    "- Better documentation of the tactic commands"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.5.2"
  },
  "toc": {
   "nav_menu": {},
   "number_sections": true,
   "sideBar": true,
   "skip_h1_title": false,
   "title_cell": "Table of Contents",
   "title_sidebar": "Contents",
   "toc_cell": true,
   "toc_position": {},
   "toc_section_display": true,
   "toc_window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}