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-415: Repair mining error: AssertionError #50

Closed a-gardner1 closed 1 year ago

a-gardner1 commented 1 year ago 
2023-05-03 15:18:04,432 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='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.1', status=1)
      label_b = CacheObjectStatus(project='InteractionTrees', commit_hash='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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 0x7fe0ec538040>
      cache = <prism.data.build_cache.CoqProjectBuildCache object at 0x7fe0ec538070>
      initial_state = ProjectCommitData(project='InteractionTrees', commit_sha='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      repaired_state = ProjectCommitData(project='InteractionTrees', commit_sha='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      e = AssertionError()
  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='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      b = ProjectCommitData(project='InteractionTrees', commit_sha='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      align = <function default_align at 0x7fdf1a7167a0>
      diff = GitDiff(text='diff --git a/theories/Interp/TranslateFacts.v b/theories/Interp/TranslateFacts.v\nindex e67161a..2a43e10 100644\n--- a/theories/Interp/TranslateFacts.v\n+++ b/theories/Interp/TranslateFacts.v\n@@ -204,0 +205,19 @@ Qed.\n+Lemma eutt_translate_gen : forall {E F X Y} (f : E\n+~> F) (RR : X -> Y -> Prop) (t :\n+itree E X) (s : itree E Y), eutt RR t\n+s -> eutt RR (translate f t) (translate f s).\n+Proof.\n+intros *.\n+revert t s.\n+einit.\n+ecofix CIH.\n+intros * EUTT.\n+rewrite !unfold_translate.punfold EUTT.red in EUTT.\n+induction EUTT; intros; subst; simpl; pclearbot.\n+-estep.\n+-estep.\n+-estep; intros ?; ebase.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+Qed.\n+\n')
      compute_diff = True
      return_aligned_commands = False
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/align.py", line 577, in align_commits
    diff_alignment = _compute_diff_alignment(
      diff = GitDiff(text='diff --git a/theories/Interp/TranslateFacts.v b/theories/Interp/TranslateFacts.v\nindex e67161a..2a43e10 100644\n--- a/theories/Interp/TranslateFacts.v\n+++ b/theories/Interp/TranslateFacts.v\n@@ -204,0 +205,19 @@ Qed.\n+Lemma eutt_translate_gen : forall {E F X Y} (f : E\n+~> F) (RR : X -> Y -> Prop) (t :\n+itree E X) (s : itree E Y), eutt RR t\n+s -> eutt RR (translate f t) (translate f s).\n+Proof.\n+intros *.\n+revert t s.\n+einit.\n+ecofix CIH.\n+intros * EUTT.\n+rewrite !unfold_translate.punfold EUTT.red in EUTT.\n+induction EUTT; intros; subst; simpl; pclearbot.\n+-estep.\n+-estep.\n+-estep; intros ?; ebase.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+Qed.\n+\n')
      align = <function default_align at 0x7fdf1a7167a0>
      a_files = ['theories/Basics/CategoryOps.v', 'theories/Basics/Basics.v', 'theories/Basics/CategoryFunctor.v', 'theories/Core/ITreeDefinition.v', 'theories/Basics/Tacs.v', 'theories/Basics/CategoryTheory.v', 'theories/Eq/Shallow.v', 'theories/Basics/HeterogeneousRelations.v', 'theories/Basics/Function.v', 'theories/Basics/CategoryFacts.v', 'theories/Eq/Eq.v', 'theories/Basics/Monad.v', 'theories/Indexed/Sum.v', 'theories/Indexed/Relation.v', 'theories/Basics/Category.v', 'theories/Eq/UpToTaus.v', 'theories/Basics/CategoryKleisli.v', 'theories/Indexed/Function.v', 'theories/Core/KTree.v', 'theories/Core/ITreeMonad.v', 'theories/Basics/CategoryKleisliFacts.v', 'theories/Interp/Interp.v', 'theories/Core/Subevent.v', 'theories/Core/KTreeFacts.v', 'theories/Interp/Recursion.v', 'theories/Interp/TranslateFacts.v', 'theories/Interp/Handler.v', 'theories/Interp/InterpFacts.v', 'theories/Interp/RecursionFacts.v', 'theories/Eq/SimUpToTaus.v', 'theories/Interp/HandlerFacts.v', 'theories/Indexed/FunctionFacts...
      b_files = ['theories/Basics/CategoryOps.v', 'theories/Basics/Basics.v', 'theories/Basics/CategoryFunctor.v', 'theories/Core/ITreeDefinition.v', 'theories/Basics/Tacs.v', 'theories/Basics/CategoryTheory.v', 'theories/Eq/Shallow.v', 'theories/Basics/HeterogeneousRelations.v', 'theories/Basics/Function.v', 'theories/Basics/CategoryFacts.v', 'theories/Eq/Eq.v', 'theories/Basics/Monad.v', 'theories/Indexed/Sum.v', 'theories/Indexed/Relation.v', 'theories/Basics/Category.v', 'theories/Eq/UpToTaus.v', 'theories/Basics/CategoryKleisli.v', 'theories/Indexed/Function.v', 'theories/Core/KTree.v', 'theories/Core/ITreeMonad.v', 'theories/Basics/CategoryKleisliFacts.v', 'theories/Interp/Interp.v', 'theories/Core/Subevent.v', 'theories/Core/KTreeFacts.v', 'theories/Interp/Recursion.v', 'theories/Interp/TranslateFacts.v', 'theories/Interp/Handler.v', 'theories/Interp/InterpFacts.v', 'theories/Interp/RecursionFacts.v', 'theories/Eq/SimUpToTaus.v', 'theories/Interp/HandlerFacts.v', 'theories/Indexed/FunctionFacts...
      a = ProjectCommitData(project='InteractionTrees', commit_sha='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      a_file_sizes = {'theories/Basics/Basics.v': 27, 'theories/Basics/Category.v': 1, 'theories/Basics/CategoryFacts.v': 140, 'theories/Basics/CategoryFunctor.v': 16, 'theories/Basics/CategoryKleisli.v': 23, 'theories/Basics/CategoryKleisliFacts.v': 56, 'theories/Basics/CategoryOps.v': 117, 'theories/Basics/CategoryRelations.v': 89, 'theories/Basics/CategorySub.v': 52, 'theories/Basics/CategoryTheory.v': 167, 'theories/Basics/Function.v': 12, 'theories/Basics/FunctionFacts.v': 14, 'theories/Basics/HeterogeneousRelations.v': 127, 'theories/Basics/Monad.v': 19, 'theories/Basics/MonadProp.v': 19, 'theories/Basics/MonadState.v': 36, 'theories/Basics/Tacs.v': 11, 'theories/Core/ITreeDefinition.v': 63, 'theories/Core/ITreeMonad.v': 4, 'theories/Core/KTree.v': 15, 'theories/Core/KTreeFacts.v': 25, 'theories/Core/Subevent.v': 28, 'theories/Eq.v': 1, 'theories/Eq/Eq.v': 213, 'theories/Eq/EqAxiom.v': 3, 'theories/Eq/Shallow.v': 31, 'theories/Eq/SimUpToTaus.v': 35, 'theories/Eq/UpToTaus.v': 117, 'theories/Events.v':...
      a_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategoryRelations.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [], 'theories/Basics/HeterogeneousRelations.v': [], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadProp.v': [], 'theories/Basics/MonadState.v': [], 'theories/Basics/Tacs.v': [], 'theories/Core/ITreeDefinition.v': [], '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': [], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [...
      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], 'theories/Basics/Category.v': [0], 'theories/Basics/CategoryFacts.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, 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, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, ...
      b = ProjectCommitData(project='InteractionTrees', commit_sha='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      b_file_sizes = {'theories/Basics/Basics.v': 27, 'theories/Basics/Category.v': 1, 'theories/Basics/CategoryFacts.v': 140, 'theories/Basics/CategoryFunctor.v': 16, 'theories/Basics/CategoryKleisli.v': 23, 'theories/Basics/CategoryKleisliFacts.v': 56, 'theories/Basics/CategoryOps.v': 117, 'theories/Basics/CategoryRelations.v': 89, 'theories/Basics/CategorySub.v': 52, 'theories/Basics/CategoryTheory.v': 167, 'theories/Basics/Function.v': 12, 'theories/Basics/FunctionFacts.v': 14, 'theories/Basics/HeterogeneousRelations.v': 127, 'theories/Basics/Monad.v': 19, 'theories/Basics/MonadProp.v': 19, 'theories/Basics/MonadState.v': 36, 'theories/Basics/Tacs.v': 11, 'theories/Core/ITreeDefinition.v': 63, 'theories/Core/ITreeMonad.v': 4, 'theories/Core/KTree.v': 15, 'theories/Core/KTreeFacts.v': 25, 'theories/Core/Subevent.v': 28, 'theories/Eq.v': 1, 'theories/Eq/Eq.v': 213, 'theories/Eq/EqAxiom.v': 3, 'theories/Eq/Shallow.v': 31, 'theories/Eq/SimUpToTaus.v': 35, 'theories/Eq/UpToTaus.v': 117, 'theories/Events.v':...
      b_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategoryRelations.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [], 'theories/Basics/HeterogeneousRelations.v': [], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadProp.v': [], 'theories/Basics/MonadState.v': [], 'theories/Basics/Tacs.v': [], 'theories/Core/ITreeDefinition.v': [], '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': [], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [...
      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], 'theories/Basics/Category.v': [0], 'theories/Basics/CategoryFacts.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, 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, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, ...
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/align.py", line 492, in _compute_diff_alignment
    assert b_in_diff.files == [rename_map[f] for f in b.files]
      a = ProjectCommitData(project='InteractionTrees', commit_sha='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      diff = GitDiff(text='diff --git a/theories/Interp/TranslateFacts.v b/theories/Interp/TranslateFacts.v\nindex e67161a..2a43e10 100644\n--- a/theories/Interp/TranslateFacts.v\n+++ b/theories/Interp/TranslateFacts.v\n@@ -204,0 +205,19 @@ Qed.\n+Lemma eutt_translate_gen : forall {E F X Y} (f : E\n+~> F) (RR : X -> Y -> Prop) (t :\n+itree E X) (s : itree E Y), eutt RR t\n+s -> eutt RR (translate f t) (translate f s).\n+Proof.\n+intros *.\n+revert t s.\n+einit.\n+ecofix CIH.\n+intros * EUTT.\n+rewrite !unfold_translate.punfold EUTT.red in EUTT.\n+induction EUTT; intros; subst; simpl; pclearbot.\n+-estep.\n+-estep.\n+-estep; intros ?; ebase.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+-rewrite tau_euttge, unfold_translate.eauto.\n+Qed.\n+\n')
      align = <function default_align at 0x7fdf1a7167a0>
      a_in_diff = ProjectCommitData(project='InteractionTrees', commit_sha='5e6974a18f5635d52886444be3ebdc56cdcb06a8', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      b_in_diff = ProjectCommitData(project='InteractionTrees', commit_sha='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      change = Change(before_filename=PosixPath('theories/Interp/TranslateFacts.v'), after_filename=PosixPath('theories/Interp/TranslateFacts.v'), before_range=range(204, 204), after_range=range(205, 224), removed_lines=[], added_lines=['Lemma eutt_translate_gen : forall {E F X Y} (f : E', '~> F) (RR : X -> Y -> Prop) (t :', 'itree E X) (s : itree E Y), eutt RR t', 's -> eutt RR (translate f t) (translate f s).', 'Proof.', 'intros *.', 'revert t s.', 'einit.', 'ecofix CIH.', 'intros * EUTT.', 'rewrite !unfold_translate.punfold EUTT.red in EUTT.', 'induction EUTT; intros; subst; simpl; pclearbot.', '-estep.', '-estep.', '-estep; intros ?; ebase.', '-rewrite tau_euttge, unfold_translate.eauto.', '-rewrite tau_euttge, unfold_translate.eauto.', 'Qed.', ''])
      a_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategoryRelations.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [], 'theories/Basics/HeterogeneousRelations.v': [], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadProp.v': [], 'theories/Basics/MonadState.v': [], 'theories/Basics/Tacs.v': [], 'theories/Core/ITreeDefinition.v': [], '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': [], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [...
      b = ProjectCommitData(project='InteractionTrees', commit_sha='edd9296c7756add051bdcae0360af4c0ebfc36d2', coq_version='8.14.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/Tacs.v\nCOQC theories/Basics/HeterogeneousRelations.v\nCOQC theories/Core/ITreeDefinition.v\nCOQC theories/Indexed/Sum.v\nCOQC theories/Indexed/Relation.v\nCOQC theories/Basics/CategoryFunctor.v\nCOQC theories/Basics/Function.v\nCOQC theories/Eq/Shallow.v\nCOQC theories/Basics/Monad.v\nCOQC theories/Interp/Interp.v\nCOQC theories/Basics/CategoryTheory.v\nCOQC theories/Basics/CategoryKleisli.v\nCOQC theories/Basics/CategoryFacts.v\nCOQC theories/Eq/Eq.v\nCOQC theories/Basics/CategoryRelations.v\nCOQC theories...
      b_indices_in_diff = {'theories/Basics/Basics.v': [], 'theories/Basics/Category.v': [], 'theories/Basics/CategoryFacts.v': [], 'theories/Basics/CategoryFunctor.v': [], 'theories/Basics/CategoryKleisli.v': [], 'theories/Basics/CategoryKleisliFacts.v': [], 'theories/Basics/CategoryOps.v': [], 'theories/Basics/CategoryRelations.v': [], 'theories/Basics/CategorySub.v': [], 'theories/Basics/CategoryTheory.v': [], 'theories/Basics/Function.v': [], 'theories/Basics/FunctionFacts.v': [], 'theories/Basics/HeterogeneousRelations.v': [], 'theories/Basics/Monad.v': [], 'theories/Basics/MonadProp.v': [], 'theories/Basics/MonadState.v': [], 'theories/Basics/Tacs.v': [], 'theories/Core/ITreeDefinition.v': [], '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': [], 'theories/Eq/SimUpToTaus.v': [], 'theories/Eq/UpToTaus.v': [], 'theories/Events.v': [...
      rename_map = {'theories/Basics/Basics.v': 'theories/Basics/Basics.v', 'theories/Basics/Category.v': 'theories/Basics/Category.v', 'theories/Basics/CategoryFacts.v': 'theories/Basics/CategoryFacts.v', 'theories/Basics/CategoryFunctor.v': 'theories/Basics/CategoryFunctor.v', 'theories/Basics/CategoryKleisli.v': 'theories/Basics/CategoryKleisli.v', 'theories/Basics/CategoryKleisliFacts.v': 'theories/Basics/CategoryKleisliFacts.v', 'theories/Basics/CategoryOps.v': 'theories/Basics/CategoryOps.v', 'theories/Basics/CategoryRelations.v': 'theories/Basics/CategoryRelations.v', 'theories/Basics/CategorySub.v': 'theories/Basics/CategorySub.v', 'theories/Basics/CategoryTheory.v': 'theories/Basics/CategoryTheory.v', 'theories/Basics/Function.v': 'theories/Basics/Function.v', 'theories/Basics/FunctionFacts.v': 'theories/Basics/FunctionFacts.v', 'theories/Basics/HeterogeneousRelations.v': 'theories/Basics/HeterogeneousRelations.v', 'theories/Basics/Monad.v': 'theories/Basics/Monad.v', 'theories/Basics/MonadProp....
builtins.AssertionError:
tom-p-reichel commented 1 year ago

I printed out the full values of rename_map, b.files and b_in_diff.files. While it is true that b_in_diff.files != [rename_map[f] for f in b.files], it is also true that set(b_in_diff.files) == set([rename_map[f] for f in b.files]), in the instance I checked.

Did you mean to do set comparison here? If not, you'd be expecting rename_map to be an identity transformation.