logic.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "0d09af4d",
   "metadata": {},
   "source": [
    "# Running Jupyter on a Buildbot worker\n",
    "Why do we want to do this? We can develop pieces of Buildbot code or do experiments with Buildbot code in order to create new features or fix bugs, and as we go we can document the process."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "f3b178df",
   "metadata": {},
   "outputs": [],
   "source": [
    "def solutions(props, varnames, **kw):\n",
    "    import re\n",
    "    props = [x.strip() for x in props.split('\\n') if x.strip()]\n",
    "    lookups = {}\n",
    "    for p in props[:]:\n",
    "        m = re.match(\"^([a-zA-Z]): (.*)\", p)\n",
    "        if m:\n",
    "            lookups[m.group(1)] = m.group(2)\n",
    "            props.remove(p)\n",
    "    print((props, varnames, kw, lookups))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9d889b50",
   "metadata": {},
   "source": [
    "In a Jupyter notebook we may need to put things in a meaningful order for the interpreter, which may not be the logical presentation for a human reader, alas not exactly literate programming as Knuth intended. So the function above needs to be tweaked to make things happy below, and I wish I could do it the reverse way."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "ae58ab72",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(['M iff N', 'p & q', 'forall x: x | ~x', 'q implies H'], 'p,q', {}, {'M': '~p | q', 'N': 'p implies q   # same meaning', 'H': 'forall epsilon: exists delta: ...limit...'})\n",
      "None\n",
      "(['M iff N', 'p & q', 'forall x: x | ~x', 'q implies H'], 'q', {'p': False}, {'M': '~p | q', 'N': 'p implies q   # same meaning', 'H': 'forall epsilon: exists delta: ...limit...'})\n",
      "None\n",
      "(['M iff N', 'p & q', 'forall x: x | ~x', 'q implies H'], 'q', {'p': True}, {'M': '~p | q', 'N': 'p implies q   # same meaning', 'H': 'forall epsilon: exists delta: ...limit...'})\n",
      "None\n"
     ]
    }
   ],
   "source": [
    "# A collection of propositions\n",
    "props = \"\"\"\n",
    "    M: ~p | q\n",
    "    N: p implies q   # same meaning\n",
    "    M iff N\n",
    "    p & q\n",
    "    forall x: x | ~x\n",
    "    H: forall epsilon: exists delta: ...limit...\n",
    "    q implies H\n",
    "\"\"\"\n",
    "\n",
    "print(solutions(props, \"p,q\"))\n",
    "print(solutions(props, \"q\", p=False))\n",
    "print(solutions(props, \"q\", p=True))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}

tryit.ipynb