Skip to content

Commit

Permalink
improve regex parsing
Browse files Browse the repository at this point in the history
  • Loading branch information
Boris Shminke committed Sep 15, 2022
1 parent 263d327 commit 257c599
Showing 1 changed file with 46 additions and 58 deletions.
104 changes: 46 additions & 58 deletions examples/cicm2022_example.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"server \"isabelle\" = 127.0.0.1:38145 (password \"2b731e67-df0a-4493-a9c4-09d82ad14fc6\")\n",
"server \"isabelle\" = 127.0.0.1:37955 (password \"2fd5b83c-75e6-458b-a22c-24084e82c413\")\n",
"\n"
]
}
Expand Down Expand Up @@ -126,7 +126,7 @@
{
"data": {
"text/plain": [
"<Process 1235>"
"<Process 323>"
]
},
"execution_count": 5,
Expand All @@ -152,7 +152,7 @@
{
"data": {
"text/plain": [
"1235"
"323"
]
},
"execution_count": 6,
Expand All @@ -178,7 +178,7 @@
{
"data": {
"text/plain": [
"<isabelle_client.isabelle__client.IsabelleClient at 0x7f90344e4a00>"
"<isabelle_client.isabelle__client.IsabelleClient at 0x7f0c5c65b1c0>"
]
},
"execution_count": 7,
Expand Down Expand Up @@ -329,14 +329,14 @@
"name": "stdout",
"output_type": "stream",
"text": [
"CPU times: user 10.6 ms, sys: 0 ns, total: 10.6 ms\n",
"Wall time: 17.7 s\n"
"CPU times: user 5.04 ms, sys: 0 ns, total: 5.04 ms\n",
"Wall time: 18.7 s\n"
]
},
{
"data": {
"text/plain": [
"'3a351829-9b53-4e33-8359-1ae92907af8c'"
"'7d0f609a-6327-4d4b-a5bd-a4e4c9dd3787'"
]
},
"execution_count": 12,
Expand Down Expand Up @@ -392,19 +392,20 @@
"name": "stdout",
"output_type": "stream",
"text": [
"CPU times: user 9.65 ms, sys: 211 µs, total: 9.86 ms\n",
"Wall time: 15.6 s\n"
"CPU times: user 4.22 ms, sys: 875 µs, total: 5.1 ms\n",
"Wall time: 15.7 s\n"
]
},
{
"data": {
"text/plain": [
"[IsabelleResponse(response_type='OK', response_body='{\"isabelle_id\":\"c2a2be496f35\",\"isabelle_name\":\"Isabelle2021-1\"}', response_length=None),\n",
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"2142ac80-245f-4cfe-86c8-b4cbc713312f\"}', response_length=None),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":18,\"task\":\"2142ac80-245f-4cfe-86c8-b4cbc713312f\",\"message\":\"theory Draft.Problem 18%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=161),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":99,\"task\":\"2142ac80-245f-4cfe-86c8-b4cbc713312f\",\"message\":\"theory Draft.Problem 99%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=161),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":100,\"task\":\"2142ac80-245f-4cfe-86c8-b4cbc713312f\",\"message\":\"theory Draft.Problem 100%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=163),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"errors\":[],\"nodes\":[{\"messages\":[{\"kind\":\"writeln\",\"message\":\"Sledgehammering...\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"Proof found...\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"cvc4\\\\\": Try this: by simp (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"verit\\\\\": Try this: by presburger (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"z3\\\\\": Try this: by simp (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"vampire\\\\\": Try this: by simp (3 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"e\\\\\": Try this: by force (5 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"spass\\\\\": Try this: by blast (2 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}}],\"exports\":[],\"status\":{\"percentage\":100,\"unprocessed\":0,\"running\":0,\"finished\":11,\"failed\":0,\"total\":11,\"consolidated\":true,\"canceled\":false,\"ok\":true,\"warned\":0},\"theory_name\":\"Draft.Problem\",\"node_name\":\"Problem.thy\"}],\"task\":\"2142ac80-245f-4cfe-86c8-b4cbc713312f\"}', response_length=1351)]"
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\"}', response_length=None),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":18,\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\",\"message\":\"theory Draft.Problem 18%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=161),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":36,\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\",\"message\":\"theory Draft.Problem 36%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=161),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":99,\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\",\"message\":\"theory Draft.Problem 99%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=161),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":100,\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\",\"message\":\"theory Draft.Problem 100%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Problem\"}', response_length=163),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"errors\":[],\"nodes\":[{\"messages\":[{\"kind\":\"writeln\",\"message\":\"Sledgehammering...\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"Proof found...\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"verit\\\\\": Try this: by auto (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"cvc4\\\\\": Try this: by presburger (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"vampire\\\\\": Try this: by force (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}},{\"kind\":\"writeln\",\"message\":\"\\\\\"e\\\\\": Try this: by presburger (1 ms)\",\"pos\":{\"line\":5,\"offset\":60,\"end_offset\":72,\"file\":\"Problem.thy\"}}],\"exports\":[],\"status\":{\"percentage\":100,\"unprocessed\":0,\"running\":0,\"finished\":11,\"failed\":0,\"total\":11,\"consolidated\":true,\"canceled\":false,\"ok\":true,\"warned\":0},\"theory_name\":\"Draft.Problem\",\"node_name\":\"Problem.thy\"}],\"task\":\"ac3dbba0-c955-4983-9c9d-0cbe8cca0b65\"}', response_length=1093)]"
]
},
"execution_count": 14,
Expand Down Expand Up @@ -453,37 +454,25 @@
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"cvc4\": Try this: by simp (1 ms)',\n",
" 'message': '\"verit\": Try this: by auto (1 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"verit\": Try this: by presburger (1 ms)',\n",
" 'message': '\"cvc4\": Try this: by presburger (1 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"z3\": Try this: by simp (1 ms)',\n",
" 'message': '\"vampire\": Try this: by force (1 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"vampire\": Try this: by simp (3 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"e\": Try this: by force (5 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
" 'file': 'Problem.thy'}},\n",
" {'kind': 'writeln',\n",
" 'message': '\"spass\": Try this: by blast (2 ms)',\n",
" 'message': '\"e\": Try this: by presburger (1 ms)',\n",
" 'pos': {'line': 5,\n",
" 'offset': 60,\n",
" 'end_offset': 72,\n",
Expand All @@ -501,7 +490,7 @@
" 'warned': 0},\n",
" 'theory_name': 'Draft.Problem',\n",
" 'node_name': 'Problem.thy'}],\n",
" 'task': '2142ac80-245f-4cfe-86c8-b4cbc713312f'}"
" 'task': 'ac3dbba0-c955-4983-9c9d-0cbe8cca0b65'}"
]
},
"execution_count": 15,
Expand Down Expand Up @@ -531,12 +520,10 @@
"text/plain": [
"['Sledgehammering...',\n",
" 'Proof found...',\n",
" '\"cvc4\": Try this: by simp (1 ms)',\n",
" '\"verit\": Try this: by presburger (1 ms)',\n",
" '\"z3\": Try this: by simp (1 ms)',\n",
" '\"vampire\": Try this: by simp (3 ms)',\n",
" '\"e\": Try this: by force (5 ms)',\n",
" '\"spass\": Try this: by blast (2 ms)']"
" '\"verit\": Try this: by auto (1 ms)',\n",
" '\"cvc4\": Try this: by presburger (1 ms)',\n",
" '\"vampire\": Try this: by force (1 ms)',\n",
" '\"e\": Try this: by presburger (1 ms)']"
]
},
"execution_count": 16,
Expand Down Expand Up @@ -564,14 +551,7 @@
{
"data": {
"text/plain": [
"[[],\n",
" [],\n",
" ['by simp'],\n",
" ['by presburger'],\n",
" ['by simp'],\n",
" ['by simp'],\n",
" ['by force'],\n",
" ['by blast']]"
"[[], [], ['by auto'], ['by presburger'], ['by force'], ['by presburger']]"
]
},
"execution_count": 17,
Expand All @@ -584,7 +564,7 @@
"import re\n",
"\n",
"proposed_solutions = [\n",
" re.findall('\".*\": Try this: (.*) \\(\\d+ ms\\)', message)\n",
" re.findall('\".*\": Try this: (.*) \\(\\d+\\.?\\d* m?s\\)', message)\n",
" for message in messages\n",
"]\n",
"proposed_solutions"
Expand All @@ -604,7 +584,7 @@
{
"data": {
"text/plain": [
"'by simp'"
"'by auto'"
]
},
"execution_count": 18,
Expand Down Expand Up @@ -643,7 +623,7 @@
"theory Solution imports Main\n",
"begin\n",
"lemma \"\\<forall> x. \\<exists> y. x = y\"\n",
"by simp\n",
"by auto\n",
"end\n",
" \n"
]
Expand Down Expand Up @@ -676,19 +656,19 @@
"name": "stdout",
"output_type": "stream",
"text": [
"CPU times: user 10.4 ms, sys: 957 µs, total: 11.3 ms\n",
"Wall time: 14.9 s\n"
"CPU times: user 2.95 ms, sys: 3.07 ms, total: 6.03 ms\n",
"Wall time: 15 s\n"
]
},
{
"data": {
"text/plain": [
"[IsabelleResponse(response_type='OK', response_body='{\"isabelle_id\":\"c2a2be496f35\",\"isabelle_name\":\"Isabelle2021-1\"}', response_length=None),\n",
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"cc332841-911f-4293-acc5-6e9ee76ff335\"}', response_length=None),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":22,\"task\":\"cc332841-911f-4293-acc5-6e9ee76ff335\",\"message\":\"theory Draft.Solution 22%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=163),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":99,\"task\":\"cc332841-911f-4293-acc5-6e9ee76ff335\",\"message\":\"theory Draft.Solution 99%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=163),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":100,\"task\":\"cc332841-911f-4293-acc5-6e9ee76ff335\",\"message\":\"theory Draft.Solution 100%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=165),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"errors\":[],\"nodes\":[{\"messages\":[],\"exports\":[],\"status\":{\"percentage\":100,\"unprocessed\":0,\"running\":0,\"finished\":9,\"failed\":0,\"total\":9,\"consolidated\":true,\"canceled\":false,\"ok\":true,\"warned\":0},\"theory_name\":\"Draft.Solution\",\"node_name\":\"Solution.thy\"}],\"task\":\"cc332841-911f-4293-acc5-6e9ee76ff335\"}', response_length=324)]"
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"f71777e8-9b4f-411b-8c09-7e1ca29de918\"}', response_length=None),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":22,\"task\":\"f71777e8-9b4f-411b-8c09-7e1ca29de918\",\"message\":\"theory Draft.Solution 22%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=163),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":99,\"task\":\"f71777e8-9b4f-411b-8c09-7e1ca29de918\",\"message\":\"theory Draft.Solution 99%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=163),\n",
" IsabelleResponse(response_type='NOTE', response_body='{\"percentage\":100,\"task\":\"f71777e8-9b4f-411b-8c09-7e1ca29de918\",\"message\":\"theory Draft.Solution 100%\",\"kind\":\"writeln\",\"session\":\"\",\"theory\":\"Draft.Solution\"}', response_length=165),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"errors\":[],\"nodes\":[{\"messages\":[],\"exports\":[],\"status\":{\"percentage\":100,\"unprocessed\":0,\"running\":0,\"finished\":9,\"failed\":0,\"total\":9,\"consolidated\":true,\"canceled\":false,\"ok\":true,\"warned\":0},\"theory_name\":\"Draft.Solution\",\"node_name\":\"Solution.thy\"}],\"task\":\"f71777e8-9b4f-411b-8c09-7e1ca29de918\"}', response_length=324)]"
]
},
"execution_count": 20,
Expand Down Expand Up @@ -738,7 +718,7 @@
" 'warned': 0},\n",
" 'theory_name': 'Draft.Solution',\n",
" 'node_name': 'Solution.thy'}],\n",
" 'task': 'cc332841-911f-4293-acc5-6e9ee76ff335'}"
" 'task': 'f71777e8-9b4f-411b-8c09-7e1ca29de918'}"
]
},
"execution_count": 21,
Expand Down Expand Up @@ -766,8 +746,8 @@
"data": {
"text/plain": [
"[IsabelleResponse(response_type='OK', response_body='{\"isabelle_id\":\"c2a2be496f35\",\"isabelle_name\":\"Isabelle2021-1\"}', response_length=None),\n",
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"29c104d2-0035-4c56-9076-a532d00b5479\"}', response_length=None),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"return_code\":0,\"task\":\"29c104d2-0035-4c56-9076-a532d00b5479\"}', response_length=None)]"
" IsabelleResponse(response_type='OK', response_body='{\"task\":\"3ddb9298-d640-49cf-af4f-e78d733611a7\"}', response_length=None),\n",
" IsabelleResponse(response_type='FINISHED', response_body='{\"ok\":true,\"return_code\":0,\"task\":\"3ddb9298-d640-49cf-af4f-e78d733611a7\"}', response_length=None)]"
]
},
"execution_count": 22,
Expand Down Expand Up @@ -807,6 +787,14 @@
"# and shut the server down\n",
"isabelle.shutdown()"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "2996e460-06c4-43db-ad6c-e76858a2baf9",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
Expand Down

0 comments on commit 257c599

Please sign in to comment.