search

Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

PEARLS-414: Repair mining error: Need at least one array to concatenate #49

Closed a-gardner1 closed 1 year ago

a-gardner1 commented 1 year ago 
2023-05-03 15:17:49,553 Traceback: Traceback with variables (most recent call last):
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/mining.py", line 804, in build_error_instances_from_label_pair
    commit_diff = ProjectCommitDataDiff.from_commit_data(
      label_a = CacheObjectStatus(project='InteractionTrees', commit_hash='6a23fbc86f5f62c802f7eb5766e12ae8dc6c0eca', coq_version='8.9.1', status=1)
      label_b = CacheObjectStatus(project='InteractionTrees', commit_hash='a5148f755495c66d4e4c283ec1cc42acb0bfb761', coq_version='8.9.1', status=1)
      cache_root = PosixPath('/workspace/pearls/caching/caching_03-28-23')
      cache_fmt_extension = 'json'
      changeset_miner = <bound method ProjectCommitDataErrorInstance.default_changeset_miner of <class 'prism.data.repair.instance.ProjectCommitDataErrorInstance'>>
      repair_mining_logger = <AutoProxy[Client] object, typeid 'Client' at 0x7fdf19fb7eb0>
      cache = <prism.data.build_cache.CoqProjectBuildCache object at 0x7fdf19fb7c10>
      initial_state = ProjectCommitData(project='InteractionTrees', commit_sha='6a23fbc86f5f62c802f7eb5766e12ae8dc6c0eca', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Core/ITreeMonad.v\nCOQC theories/...
      repaired_state = ProjectCommitData(project='InteractionTrees', commit_sha='a5148f755495c66d4e4c283ec1cc42acb0bfb761', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Eq/SimUpToTaus.v\nCOQC theories/C...
      e = ValueError('need at least one array to concatenate')
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 656, in from_commit_data
    alignment = align_commits(a, b, diff, align)
      cls = <class 'prism.data.repair.instance.ProjectCommitDataDiff'>
      a = ProjectCommitData(project='InteractionTrees', commit_sha='6a23fbc86f5f62c802f7eb5766e12ae8dc6c0eca', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Core/ITreeMonad.v\nCOQC theories/...
      b = ProjectCommitData(project='InteractionTrees', commit_sha='a5148f755495c66d4e4c283ec1cc42acb0bfb761', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Eq/SimUpToTaus.v\nCOQC theories/C...
      align = <function default_align at 0x7fdf1a7167a0>
      diff = GitDiff(text='diff --git a/theories/Basics/CategoryFacts.v b/theories/Basics/CategoryFacts.v\nindex 5fcc5e1..8d04bc9 100644\n--- a/theories/Basics/CategoryFacts.v\n+++ b/theories/Basics/CategoryFacts.v\n@@ -50 +50 @@ Context {CatIdL_C : CatIdL C}.\n-Global Instance SemiIso_Id {a} : SemiIso C (id_ a) (id_ a) := {}.\n+Global Instance SemiIso_Id {a} : SemiIso C (id_ a) (id_ a).\n@@ -62,4 +62,4 @@ C b c -> _) (eq2 ==> eq2 ==> eq2) cat}.\n-Global Instance SemiIso_Cat {a b c} (f : C a b) {f\' :\n-C b a} {SemiIso_f : SemiIso C f f\'} (g : C\n-b c) {g\' : C c b} {SemiIso_g : SemiIso C g\n-g\'} : SemiIso C (f >>> g) (g\' >>> f\') := {}.\n+Global Instance SemiIso_Cat {a b c} (f : C a b) {f\'\n+: C b a} {SemiIso_f : SemiIso C f f\'} (g :\n+C b c) {g\' : C c b} {SemiIso_g : SemiIso C\n+g g\'} : SemiIso C (f >>> g) (g\' >>> f\').\n@@ -67,2 +67,2 @@ Proof.\n-rewrite cat_assoc, <- (cat_assoc g), (semi_iso\n-g _), cat_id_l, (semi_iso f _).\n+red.\n+rewrite cat_assoc, <- (cat_assoc g), (semi_iso g _), ...
      compute_diff = True
      return_aligned_commands = False
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/align.py", line 593, in align_commits
    changed_a_indices = np.concatenate(
      diff = GitDiff(text='diff --git a/theories/Basics/CategoryFacts.v b/theories/Basics/CategoryFacts.v\nindex 5fcc5e1..8d04bc9 100644\n--- a/theories/Basics/CategoryFacts.v\n+++ b/theories/Basics/CategoryFacts.v\n@@ -50 +50 @@ Context {CatIdL_C : CatIdL C}.\n-Global Instance SemiIso_Id {a} : SemiIso C (id_ a) (id_ a) := {}.\n+Global Instance SemiIso_Id {a} : SemiIso C (id_ a) (id_ a).\n@@ -62,4 +62,4 @@ C b c -> _) (eq2 ==> eq2 ==> eq2) cat}.\n-Global Instance SemiIso_Cat {a b c} (f : C a b) {f\' :\n-C b a} {SemiIso_f : SemiIso C f f\'} (g : C\n-b c) {g\' : C c b} {SemiIso_g : SemiIso C g\n-g\'} : SemiIso C (f >>> g) (g\' >>> f\') := {}.\n+Global Instance SemiIso_Cat {a b c} (f : C a b) {f\'\n+: C b a} {SemiIso_f : SemiIso C f f\'} (g :\n+C b c) {g\' : C c b} {SemiIso_g : SemiIso C\n+g g\'} : SemiIso C (f >>> g) (g\' >>> f\').\n@@ -67,2 +67,2 @@ Proof.\n-rewrite cat_assoc, <- (cat_assoc g), (semi_iso\n-g _), cat_id_l, (semi_iso f _).\n+red.\n+rewrite cat_assoc, <- (cat_assoc g), (semi_iso g _), ...
      align = <function default_align at 0x7fdf1a7167a0>
      a_files = []
      b_files = []
      diff_alignment = array([], shape=(0, 2), dtype=int64)
      a = ProjectCommitData(project='InteractionTrees', commit_sha='6a23fbc86f5f62c802f7eb5766e12ae8dc6c0eca', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Core/ITreeMonad.v\nCOQC theories/...
      a_file_offsets = {}
      a_file_sizes = {'theories/Basics/Basics.v': 43, 'theories/Basics/Category.v': 1, 'theories/Basics/CategoryFacts.v': 140, 'theories/Basics/CategoryFunctor.v': 16, 'theories/Basics/CategoryKleisli.v': 23, 'theories/Basics/CategoryKleisliFacts.v': 54, 'theories/Basics/CategoryOps.v': 88, 'theories/Basics/CategorySub.v': 52, 'theories/Basics/CategoryTheory.v': 136, 'theories/Basics/Function.v': 12, 'theories/Basics/FunctionFacts.v': 14, 'theories/Basics/Monad.v': 20, 'theories/Basics/MonadState.v': 36, 'theories/Core/ITreeDefinition.v': 62, 'theories/Core/ITreeMonad.v': 4, 'theories/Core/KTree.v': 17, 'theories/Core/KTreeFacts.v': 24, 'theories/Core/Subevent.v': 28, 'theories/Eq.v': 1, 'theories/Eq/Eq.v': 176, 'theories/Eq/EqAxiom.v': 3, 'theories/Eq/Shallow.v': 31, 'theories/Eq/SimUpToTaus.v': 35, 'theories/Eq/UpToTaus.v': 109, 'theories/Events.v': 1, 'theories/Events/Concurrency.v': 10, 'theories/Events/Dependent.v': 6, 'theories/Events/Exception.v': 5, 'theories/Events/Map.v': 26, 'theories/Events/Map...
      a_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [12, 17, 25], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [4], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadState.v': [], 'theories/Core/ITreeDefinition.v': [43, 44, 45, 46], 'theories/Core/ITreeMonad.v': [], 'theories/Core/KTree.v': [], 'theories/Core/KTreeFacts.v': [], 'theories/Core/Subevent.v': [], 'theories/Eq.v': [], 'theories/Eq/Eq.v': [], 'theories/Eq/EqAxiom.v': [], 'theories/Eq/Shallow.v': [4], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [], 'theories/Events/Concurrency.v': [7], 'theories/Events/Dependent.v': [], 'theories/Events/Exception.v': [], 'theories/Events/Ma...
      a_indices_not_in_diff = {'theories/Basics/Basics.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42], 'theories/Basics/Category.v': [0], 'theories/Basics/CategoryFacts.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 14, 15, 16, 18, 19, 20, 21, 22, 23, 24, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139], 'theories/Basics/CategoryFunctor.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15], 'theories/Basics/CategoryKleisli.v': [0, 1, 2, 3, 4, 5, 6, 7, 8,...
      b = ProjectCommitData(project='InteractionTrees', commit_sha='a5148f755495c66d4e4c283ec1cc42acb0bfb761', coq_version='8.9.1', build_result=ProjectBuildResult(exit_code=0, stdout="# Generating _CoqProject\n# including: _CoqConfig\ncoq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/InteractionTrees'\nCOQDEP VFILES\nCOQC theories/Basics/Basics.v\nCOQC theories/Basics/CategoryOps.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Eq/UpToTaus.v\nCOQC theories/Eq/EqAxiom.v\nCOQC theories/Core/KTree.v\nCOQC theories/Eq/SimUpToTaus.v\nCOQC theories/C...
      b_file_offsets = {}
      b_file_sizes = {'theories/Basics/Basics.v': 43, 'theories/Basics/Category.v': 1, 'theories/Basics/CategoryFacts.v': 140, 'theories/Basics/CategoryFunctor.v': 16, 'theories/Basics/CategoryKleisli.v': 23, 'theories/Basics/CategoryKleisliFacts.v': 54, 'theories/Basics/CategoryOps.v': 88, 'theories/Basics/CategorySub.v': 52, 'theories/Basics/CategoryTheory.v': 136, 'theories/Basics/Function.v': 12, 'theories/Basics/FunctionFacts.v': 14, 'theories/Basics/Monad.v': 20, 'theories/Basics/MonadState.v': 36, 'theories/Core/ITreeDefinition.v': 62, 'theories/Core/ITreeMonad.v': 4, 'theories/Core/KTree.v': 17, 'theories/Core/KTreeFacts.v': 24, 'theories/Core/Subevent.v': 28, 'theories/Eq.v': 1, 'theories/Eq/Eq.v': 176, 'theories/Eq/EqAxiom.v': 3, 'theories/Eq/Shallow.v': 31, 'theories/Eq/SimUpToTaus.v': 35, 'theories/Eq/UpToTaus.v': 109, 'theories/Events.v': 1, 'theories/Events/Concurrency.v': 10, 'theories/Events/Dependent.v': 6, 'theories/Events/Exception.v': 5, 'theories/Events/Map.v': 26, 'theories/Events/Map...
      b_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [12, 17, 25], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [4], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadState.v': [], 'theories/Core/ITreeDefinition.v': [43, 44, 45, 46], 'theories/Core/ITreeMonad.v': [], 'theories/Core/KTree.v': [], 'theories/Core/KTreeFacts.v': [], 'theories/Core/Subevent.v': [], 'theories/Eq.v': [], 'theories/Eq/Eq.v': [], 'theories/Eq/EqAxiom.v': [], 'theories/Eq/Shallow.v': [4], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [], 'theories/Events/Concurrency.v': [7], 'theories/Events/Dependent.v': [], 'theories/Events/Exception.v': [], 'theories/Events/Ma...
      b_indices_not_in_diff = {'theories/Basics/Basics.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42], 'theories/Basics/Category.v': [0], 'theories/Basics/CategoryFacts.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 14, 15, 16, 18, 19, 20, 21, 22, 23, 24, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139], 'theories/Basics/CategoryFunctor.v': [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15], 'theories/Basics/CategoryKleisli.v': [0, 1, 2, 3, 4, 5, 6, 7, 8,...
  File "<__array_function__ internals>", line 180, in concatenate
      args = ([],)
      kwargs = {'axis': 0}
      relevant_args = []
      dispatcher = <function concatenate at 0x7fe05bb3dd80>
      implementation = <built-in function concatenate>
      public_api = <function concatenate at 0x7fe05bb3df30>
builtins.ValueError: need at least one array to concatenate
2023-05-03 15:17:49,571 need at least one array to concatenate
NoneType: None
a-gardner1 commented 1 year ago

This is actually a side-effect of a bug in cache extraction. Somehow the commands were extracted (which means that the SerAPI options were captured), but file dependencies were not, and the resulting metadata just shows an empty string for the SerAPI options.

While it is easy to band-aid the solution by treating the symptom (ensuring that we explicitly add nodes to the graph in ProjectCommitData.files instead of adding them only as side-effects of edge additions), we need to get to the bottom of what went wrong during cache extraction on these particular commits and Coq version (8.9.1).

a-gardner1 commented 1 year ago

I cannot reproduce the error in cache extraction, but I did identify some other bugs that may or may not have played a role. They will be bundled with the fixes for the rest of the repair mining errors, which are now waiting on a pipeline to complete.