PEARLS-416: Repair mining error: Unnested command cannot spill into another command

2023-05-03 17:10:17,445 Traceback: Traceback with variables (most recent call last):
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/mining.py", line 707, in build_repair_instance
    result = miner(error_instance, repaired_state)
      error_instance = ProjectCommitDataErrorInstance(project_name='graph-theory', initial_state=ProjectCommitDataState(project_state=ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theor...
      repaired_state = ProjectCommitData(project='graph-theory', commit_sha='317c64c647616cc8e6061d98aa98bc7ac0c13952', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/finite_quotient.v\nCOQC theories/digraph.v\nCOQC theories/equiv.v\nCOQC theories/ptt.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theories/dom.v\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_minP is deprecated; use arg_minnP instead\nWarning: arg_...
      change_selection = ChangeSelection(added_commands=[('theories/structures.v', 0), ('theories/structures.v', 1), ('theories/structures.v', 2), ('theories/mgraph2.v', 0), ('theories/mgraph2.v', 1), ('theories/extraction_iso.v', 0), ('theories/extraction_iso.v', 1), ('theories/extraction_iso.v', 2), ('theories/extraction_iso.v', 3)], affected_commands=[('theories/finite_quotient.v', 141), ('theories/digraph.v', 247), ('theories/structures.v', 47), ('theories/structures.v', 48), ('theories/structures.v', 44), ('theories/structures.v', 45), ('theories/sgraph.v', 43), ('theories/sgraph.v', 108), ('theories/sgraph.v', 123), ('theories/sgraph.v', 129), ('theories/sgraph.v', 141), ('theories/sgraph.v', 225), ('theories/connectivity.v', 39), ('theories/treewidth.v', 64), ('theories/mgraph2.v', 125), ('theories/mgraph2.v', 149), ('theories/mgraph2.v', 150), ('theories/mgraph2.v', 151), ('theories/mgraph2.v', 152), ('theories/mgraph2.v', 153), ('theories/mgraph2.v', 154), ('theories/mgraph2.v', 155), ('theories/mgrap...
      repair_instance_db_directory = PosixPath('/workspace/pearls/repairs/from_caching_03-28-23')
      miner = <bound method ProjectCommitDataRepairInstance.make_repair_instance of <class 'prism.data.repair.instance.ProjectCommitDataRepairInstance'>>
      repair_mining_logger = <AutoProxy[Client] object, typeid 'Client' at 0x7fddffb74d60>
      result = None
      db_instance = <prism.data.repair.mining.RepairInstanceDB object at 0x7fdf1926e560>
      initial_metadata = ProjectMetadata(project_name='graph-theory', build_cmd=['opam install --deps-only --yes .', 'make -j64'], install_cmd=['make install'], clean_cmd=['make clean'], ocaml_version='4.09.1', coq_version='8.12.2', serapi_version='8.12.0+0.12.1', serapi_options=SerAPIOptions(noinit=False, iqr=IQR(I=set(), Q=set(), R={('theories', 'GraphTheory')}, pwd=''), warnings=[], settings=[], allow_sprop=False, disallow_sprop=False, type_in_type=False, impredicative_set=False, indices_matter=False, loaded_files=[]), ignore_path_regex=set(), coq_dependencies=set(), opam_repos={'coq-released https://coq.inria.fr/opam/released'}, opam_dependencies=['"coq" { (>= "8.10" & < "8.13~") | (= "dev") }', '"coq-mathcomp-ssreflect" { (>= "1.10" & < "1.12~") | (= "dev") }', '"coq-mathcomp-finmap"', '"coq-hierarchy-builder"'], project_url='https://github.com/coq-community/graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51')
      repaired_metadata = ProjectMetadata(project_name='graph-theory', build_cmd=['opam install --deps-only --yes .', 'make -j64'], install_cmd=['make install'], clean_cmd=['make clean'], ocaml_version='4.09.1', coq_version='8.12.2', serapi_version='8.12.0+0.12.1', serapi_options=SerAPIOptions(noinit=False, iqr=IQR(I=set(), Q=set(), R={('theories', 'GraphTheory')}, pwd=''), warnings=[], settings=[], allow_sprop=False, disallow_sprop=False, type_in_type=False, impredicative_set=False, indices_matter=False, loaded_files=[]), ignore_path_regex=set(), coq_dependencies=set(), opam_repos={'coq-released https://coq.inria.fr/opam/released'}, opam_dependencies=['"coq" { (>= "8.10" & < "8.13~") | (= "dev") }', '"coq-mathcomp-ssreflect" { (>= "1.10" & < "1.12~") | (= "dev") }', '"coq-mathcomp-finmap"', '"coq-hierarchy-builder"'], project_url='https://github.com/coq-community/graph-theory', commit_sha='317c64c647616cc8e6061d98aa98bc7ac0c13952')
      e = AssertionError('Unnested command cannot spill into another command')
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 2225, in make_repair_instance
    broken_state = error_instance.error_state
      cls = <class 'prism.data.repair.instance.ProjectCommitDataRepairInstance'>
      error_instance = ProjectCommitDataErrorInstance(project_name='graph-theory', initial_state=ProjectCommitDataState(project_state=ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theor...
      repaired_state = ProjectCommitData(project='graph-theory', commit_sha='317c64c647616cc8e6061d98aa98bc7ac0c13952', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/finite_quotient.v\nCOQC theories/digraph.v\nCOQC theories/equiv.v\nCOQC theories/ptt.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theories/dom.v\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_minP is deprecated; use arg_minnP instead\nWarning: arg_...
      align = <function default_align at 0x7fdf1a7167a0>
      get_repair_tags = <bound method ProjectCommitDataRepairInstance.default_get_repair_tags of <class 'prism.data.repair.instance.ProjectCommitDataRepairInstance'>>
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 1286, in error_state
    error_state = self.change.diff.patch(initial_state.offset_state)
      self = ProjectCommitDataErrorInstance(project_name='graph-theory', initial_state=ProjectCommitDataState(project_state=ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theor...
      initial_state = ProjectCommitDataState(project_state=ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theories/dom.v\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning...
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 475, in patch
    self._patch_locations(result_command_data)
      self = ProjectCommitDataDiff(command_changes={'theories/edone.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/preliminaries.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/bij.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/setoid_bigop.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/finite_quotient.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={141: SerializableDataDiff(diff='@@ -505842,32 +505842,5943 @@\n      type: CRef%0A\n+        - string: y%0A       ...
      data = ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theories/dom.v\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_maxP is deprecated; use arg_max...
      result = ProjectCommitData(project='graph-theory', commit_sha='43424a856535c1133b399cde95ba19851931cf51', coq_version='8.12.2', build_result=ProjectBuildResult(exit_code=0, stdout="Nothing to do.\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/graph-theory'\nCOQDEP VFILES\nCOQC theories/edone.v\nCOQC theories/bounded.v\nCOQC theories/setoid_bigop.v\nCOQC theories/preliminaries.v\nCOQC theories/bij.v\nCOQC theories/set_tac.v\nCOQC theories/structures.v\ntt ≡ tt\n     : Prop\nfun x : unit => (x ⊗ x)%CM\n     : unit -> unit_comMonoid\nCOQC theories/pttdom.v\nCOQC theories/finmap_plus.v\nCOQC theories/digraph.v\nCOQC theories/finite_quotient.v\nCOQC theories/ptt.v\nCOQC theories/equiv.v\nCOQC theories/sgraph.v\nCOQC theories/mgraph.v\nCOQC theories/mgraph2.v\nCOQC theories/helly.v\nCOQC theories/connectivity.v\nCOQC theories/dom.v\nWarning: arg_maxP is deprecated; use arg_maxnP instead\nWarning: arg_maxP is deprecated; use arg_max...
      result_command_data = {'theories/bij.v': VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid CMorphisms., location=SexpInfo.Loc(filename='theories/bij.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=32)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Relation_Definitions., location=SexpInfo.Loc(filename='theories/bij.v', lineno=1, bol_pos=34, lineno_last=1, bol_pos_last=34, beg_charno=34, end_charno=62)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import all_ssreflect., location=SexpInfo.Loc(filename='theories/bij.v', lineno=2, bol_pos=64, lineno_last=2, bol_pos_last=64, beg_charno=64, end_charno=106)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import edone preliminaries., location=SexpInfo.Loc(filename='theories/bij.v', lineno=3, bol_pos=108, lineno_last=3, bol_...
      dropped_commands = {'theories/edone.v': set(), 'theories/preliminaries.v': set(), 'theories/bij.v': set(), 'theories/setoid_bigop.v': set(), 'theories/finite_quotient.v': {141}, 'theories/set_tac.v': set(), 'theories/digraph.v': {247}, 'theories/structures.v': {44, 45, 46, 47, 48, 49}, 'theories/equiv.v': set(), 'theories/sgraph.v': {129, 225, 43, 108, 141, 123}, 'theories/mgraph.v': set(), 'theories/connectivity.v': {39}, 'theories/pttdom.v': set(), 'theories/treewidth.v': {64}, 'theories/ptt.v': set(), 'theories/minor.v': set(), 'theories/mgraph2.v': {149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 125}, 'theories/checkpoint.v': set(), 'theories/excluded.v': {27}, 'theories/skeleton.v': set(), 'theories/cp_minor.v': set(), 'theories/bounded.v': set(), 'theories/rewriting.v': {9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19}, 'theories/finmap_plus.v': set(), '...
      added_commands = {'theories/edone.v': VernacCommandDataList(commands=[]), 'theories/preliminaries.v': VernacCommandDataList(commands=[]), 'theories/bij.v': VernacCommandDataList(commands=[]), 'theories/setoid_bigop.v': VernacCommandDataList(commands=[]), 'theories/finite_quotient.v': VernacCommandDataList(commands=[VernacCommandData(identifier=['quot_union_KE'], command=VernacSentence(text=Lemma quot_union_KE (x: S+K): quot_union_K (\pi x) = \pi (sum_left k x)., location=SexpInfo.Loc(filename='theories/finite_quotient.v', lineno=301, bol_pos=11943, lineno_last=301, bol_pos_last=11943, beg_charno=11945, end_charno=12016)), command_error=None)]), 'theories/set_tac.v': VernacCommandDataList(commands=[]), 'theories/digraph.v': VernacCommandDataList(commands=[VernacCommandData(identifier=['diso_comp'], command=VernacSentence(text=Definition diso_comp {A B C}: diso A B -> diso B C -> diso A C., location=SexpInfo.Loc(filename='theories/digraph.v', lineno=1008, bol_pos=38667, lineno_last=1008, bol_pos_last=386...
      filename = 'theories/dom.v'
      change = VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={11: SerializableDataDiff(diff='@@ -1076,13 +1076,13 @@\n no: 43\n-7\n+5\n %0A    b\n@@ -1093,13 +1093,13 @@\n os: 43\n-7\n+5\n %0A    b\n@@ -1119,5 +1119,5 @@\n 43\n-7\n+5\n %0A \n@@ -1139,4 +1139,4 @@\n 4\n-71\n+69\n %0A\n'), 12: SerializableDataDiff(diff='@@ -1498,13 +1498,13 @@\n no: 47\n-5\n+1\n %0A    b\n@@ -1515,13 +1515,13 @@\n os: 47\n-5\n+1\n %0A    b\n@@ -1541,5 +1541,5 @@\n 47\n-5\n+1\n %0A \n@@ -1561,4 +1561,4 @@\n 5\n-2\n 1\n+7\n %0A\n'), 18: SerializableDataDiff(diff='@@ -1365,10 +1365,10 @@\n no: \n+6\n 7\n-9\n 7%0A  \n@@ -1382,10 +1382,10 @@\n os: \n+6\n 7\n-9\n 7%0A  \n@@ -1407,4 +1407,4 @@\n  \n+6\n 7\n-9\n 7\n@@ -1427,4 +1427,4 @@\n  \n-83\n+71\n 5\n@@ -1478,11 +1478,11 @@\n no: 2\n-2\n+0\n %0A    \n@@ -1501,5 +1501,5 @@\n  2\n-2\n+0\n %0A \n'), 19: SerializableDataDiff(diff='@@ -1367,10 +1367,10 @@\n no: \n-83\n+71\n 7%0A  \n@@ -1384,10 +1384,10 @@\n os: \n-83\n+71\n 7%0A...
      added = VernacCommandDataList(commands=[])
      original_command_index = 32
      command_diff = SerializableDataDiff(diff='@@ -3496,14 +3496,14 @@\n no: 77\n-8\n 1\n+3\n %0A    b\n@@ -3514,14 +3514,14 @@\n os: 77\n-8\n 1\n+3\n %0A    b\n@@ -3542,4 +3542,4 @@\n 7\n-8\n 1\n+3\n %0A\n@@ -3562,5 +3562,5 @@\n 7\n-825\n+757\n %0A\n@@ -3614,11 +3614,11 @@\n o: 18\n-4\n+2\n %0A    \n@@ -3638,5 +3638,5 @@\n 18\n-4\n+2\n %0A \n')
      original_command = VernacCommandData(identifier=[], command=VernacSentence(text=Print Assumptions soundness_and_completeness., location=SexpInfo.Loc(filename='theories/completeness.v', lineno=184, bol_pos=7781, lineno_last=184, bol_pos_last=7781, beg_charno=7781, end_charno=7825)), command_error=None)
      command = VernacCommandData(identifier=[], command=VernacSentence(text=Print Assumptions soundness_and_completeness., location=SexpInfo.Loc(filename='theories/completeness.v', lineno=182, bol_pos=7713, lineno_last=182, bol_pos_last=7713, beg_charno=7713, end_charno=7757)), command_error=None)
      command_data = VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import all_ssreflect., location=SexpInfo.Loc(filename='theories/dom.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=42)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import preliminaries digraph sgraph., location=SexpInfo.Loc(filename='theories/dom.v', lineno=1, bol_pos=44, lineno_last=1, bol_pos_last=44, beg_charno=44, end_charno=87)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Set Implicit Arguments., location=SexpInfo.Loc(filename='theories/dom.v', lineno=3, bol_pos=90, lineno_last=3, bol_pos_last=90, beg_charno=90, end_charno=112)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Unset Strict Implicit., location=SexpInfo.Loc(filename='theories/dom.v', lineno=4, bol_pos=114, lineno_last=4, bol_pos_last=114, beg_charno=11...
      dropped = {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32}
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 381, in _patch_locations
    assert cmd_loc.end_charno < charno, \
      self = ProjectCommitDataDiff(command_changes={'theories/edone.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/preliminaries.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/bij.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/setoid_bigop.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={}, changed_commands={}, dropped_commands=set(), offsets=[]), 'theories/finite_quotient.v': VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={141: SerializableDataDiff(diff='@@ -505842,32 +505842,5943 @@\n      type: CRef%0A\n+        - string: y%0A       ...
      patched_command_data = {'theories/bij.v': VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid CMorphisms., location=SexpInfo.Loc(filename='theories/bij.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=32)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Relation_Definitions., location=SexpInfo.Loc(filename='theories/bij.v', lineno=1, bol_pos=34, lineno_last=1, bol_pos_last=34, beg_charno=34, end_charno=62)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import all_ssreflect., location=SexpInfo.Loc(filename='theories/bij.v', lineno=2, bol_pos=64, lineno_last=2, bol_pos_last=64, beg_charno=64, end_charno=106)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import edone preliminaries., location=SexpInfo.Loc(filename='theories/bij.v', lineno=3, bol_pos=108, lineno_last=3, bol_...
      filename = 'theories/extraction_def.v'
      change = VernacCommandDataListDiff(added_commands=VernacCommandDataList(commands=[]), affected_commands={14: SerializableDataDiff(diff='@@ -696,12 +696,12 @@\n no: 6\n-69\n+33\n %0A    \n@@ -713,12 +713,12 @@\n os: 6\n-69\n+33\n %0A    \n@@ -739,4 +739,4 @@\n 6\n-69\n+33\n %0A\n@@ -758,5 +758,5 @@\n  \n-715\n+679\n %0A\n'), 15: SerializableDataDiff(diff='@@ -3297,12 +3297,12 @@\n no: 8\n-58\n+22\n %0A    \n@@ -3318,4 +3318,4 @@\n 8\n-58\n+22\n %0A\n@@ -3339,5 +3339,5 @@\n  \n-907\n+871\n %0A\n@@ -3360,4 +3360,4 @@\n 9\n-57\n+21\n %0A\n'), 16: SerializableDataDiff(diff='@@ -3293,12 +3293,11 @@\n no: \n-1025\n+989\n %0A   \n@@ -3313,6 +3313,5 @@\n  \n-1025\n+989\n %0A\n@@ -3336,6 +3336,6 @@\n 10\n-68\n+32\n %0A \n@@ -3357,5 +3357,5 @@\n 1\n-106\n+070\n %0A\n'), 17: SerializableDataDiff(diff='@@ -1111,13 +1111,13 @@\n no: 1\n-109\n+073\n %0A    \n@@ -1129,13 +1129,13 @@\n os: 1\n-109\n+073\n %0A    \n@@ -1156,5 +1156,5 @@\n 1\n-109\n+073\n %0A\n@@ -1178,4 +1178,4 @@\n 1\n-56\n+20\n %0A\n'), 18: Se...
      offsets = [((547, 588, 18), (19, 19, 0))]
      commands = VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import RelationClasses Morphisms Setoid Omega., location=SexpInfo.Loc(filename='theories/extraction_def.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=53)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import all_ssreflect., location=SexpInfo.Loc(filename='theories/extraction_def.v', lineno=2, bol_pos=56, lineno_last=2, bol_pos_last=56, beg_charno=56, end_charno=98)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import edone finite_quotient preliminaries., location=SexpInfo.Loc(filename='theories/extraction_def.v', lineno=4, bol_pos=101, lineno_last=4, bol_pos_last=101, beg_charno=101, end_charno=151)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import digraph sgraph minor checkpoint cp_minor., location=S...
      idx = 14
      command = VernacCommandData(identifier=[], command=VernacSentence(text=Notation graph := (graph unit (flat sym))., location=SexpInfo.Loc(filename='theories/extraction_def.v', lineno=17, bol_pos=508, lineno_last=17, bol_pos_last=508, beg_charno=508, end_charno=549)), command_error=None)
      cmd_loc = SexpInfo.Loc(filename='theories/extraction_def.v', lineno=17, bol_pos=508, lineno_last=17, bol_pos_last=508, beg_charno=508, end_charno=549)
      charno = 547
      charno_last = 588
      char_shift = 18
      lineno = 19
      _lineno_last = 19
      line_shift = 0
      nested_line_shift = 1
      nested_char_shift = 43
      j = 92
builtins.AssertionError: Unnested command cannot spill into another command
Radiance-Technologies / prism

PEARLS-416: Repair mining error: Unnested command cannot spill into another command #51
