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-417: Repair mining error: '<' not supported between instances of 'VernacSentence' and 'VernacSentence' #52

Closed a-gardner1 closed 1 year ago

a-gardner1 commented 1 year ago 
2023-05-03 11:24:39,405 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='htt', initial_state=ProjectCommitDataState(project_state=ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is ...
      repaired_state = ProjectCommitData(project='htt', commit_sha='fb0c1af87736513411bdc82fca80a636deabe6e0', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      change_selection = ChangeSelection(added_commands=[], affected_commands=[], changed_commands=[('Core/pred.v', 0), ('Core/pred.v', 2), ('Core/pred.v', 3), ('Core/pred.v', 4), ('Core/pred.v', 5), ('Core/pred.v', 6), ('Core/pred.v', 7), ('Core/pred.v', 8), ('Core/pred.v', 9), ('Core/pred.v', 10), ('Core/pred.v', 11), ('Core/pred.v', 12), ('Core/pred.v', 13), ('Core/pred.v', 14), ('Core/pred.v', 15), ('Core/pred.v', 16), ('Core/pred.v', 17), ('Core/pred.v', 18), ('Core/pred.v', 19), ('Core/pred.v', 20), ('Core/pred.v', 21), ('Core/pred.v', 22), ('Core/pred.v', 23), ('Core/pred.v', 24), ('Core/pred.v', 25), ('Core/pred.v', 26), ('Core/pred.v', 27), ('Core/pred.v', 28), ('Core/pred.v', 29), ('Core/pred.v', 30), ('Core/pred.v', 31), ('Core/pred.v', 32), ('Core/pred.v', 33), ('Core/pred.v', 34), ('Core/pred.v', 35), ('Core/pred.v', 36), ('Core/pred.v', 37), ('Core/pred.v', 38), ('Core/pred.v', 39), ('Core/pred.v', 40), ('Core/pred.v', 41), ('Core/pred.v', 42), ('Core/pred.v', 43), ('Core/pred.v', 44), ('Core/pre...
      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 0x7fb87b90c700>
      result = None
      db_instance = <prism.data.repair.mining.RepairInstanceDB object at 0x7fb883114070>
      initial_metadata = ProjectMetadata(project_name='htt', build_cmd=['make -j64 -j64'], install_cmd=['make'], clean_cmd=['make clean'], ocaml_version='4.09.1', coq_version='8.11.2', serapi_version='8.11.0+0.11.1', serapi_options=SerAPIOptions(noinit=False, iqr=IQR(I=set(), Q={('.', 'HTT')}, R=set(), pwd=''), warnings=[CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='notation-overridden'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='local-declaration'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='redundant-canonical-projection'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='projection-no-head-constant')], 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=set(), opam_dependencies=['"ocaml"', '"coq" { (>= "8.9.0" & < "8.12~") | (= "dev") }', '"coq-mathcomp-ssreflect" { (>= "1.10.0" & < "1.11~") | (= "dev") }', '"coq-fcsl-pcm" { (>...
      repaired_metadata = ProjectMetadata(project_name='htt', build_cmd=['make -j64 -j64'], install_cmd=['make'], clean_cmd=['make clean'], ocaml_version='4.09.1', coq_version='8.11.2', serapi_version='8.11.0+0.11.1', serapi_options=SerAPIOptions(noinit=False, iqr=IQR(I=set(), Q={('.', 'HTT')}, R=set(), pwd=''), warnings=[CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='notation-overridden'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='local-declaration'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='redundant-canonical-projection'), CoqWarning(state=<CoqWarningState.DISABLED: 1>, name='projection-no-head-constant')], 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=set(), opam_dependencies=['"ocaml"', '"coq" { (>= "8.9.0" & < "8.12~") | (= "dev") }', '"coq-mathcomp-ssreflect" { (>= "1.10.0" & < "1.11~") | (= "dev") }', '"coq-fcsl-pcm" { (>...
      e = TypeError("'<' not supported between instances of 'VernacSentence' and 'VernacSentence'")
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 2093, in make_repair_instance
    repaired_state_diff = ProjectCommitDataDiff.from_commit_data(
      cls = <class 'prism.data.repair.instance.ProjectCommitDataRepairInstance'>
      error_instance = ProjectCommitDataErrorInstance(project_name='htt', initial_state=ProjectCommitDataState(project_state=ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is ...
      repaired_state = ProjectCommitData(project='htt', commit_sha='fb0c1af87736513411bdc82fca80a636deabe6e0', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      align = <function default_align at 0x7fb70c610af0>
      get_repair_tags = <bound method ProjectCommitDataRepairInstance.default_get_repair_tags of <class 'prism.data.repair.instance.ProjectCommitDataRepairInstance'>>
      broken_state = ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/instance.py", line 572, in from_commit_data
    diff = compute_git_diff(a, b)
      cls = <class 'prism.data.repair.instance.ProjectCommitDataDiff'>
      a = ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      b = ProjectCommitData(project='htt', commit_sha='fb0c1af87736513411bdc82fca80a636deabe6e0', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      align = <function default_align at 0x7fb70c610af0>
      diff = None
      compute_diff = True
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/repair/diff.py", line 181, in compute_git_diff
    a.write_coq_project(a_dir)
      a = ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      b = ProjectCommitData(project='htt', commit_sha='fb0c1af87736513411bdc82fca80a636deabe6e0', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      tmpdir = '/tmp/tmps9egiyk2'
      a_dir = PosixPath('/tmp/tmps9egiyk2/a')
      b_dir = PosixPath('/tmp/tmps9egiyk2/b')
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/build_cache.py", line 1072, in write_coq_project
    commands.write_coq_file(dirpath / filename)
      self = ProjectCommitData(project='htt', commit_sha='653adcfb6997c1a68475ee4389485731158afeff', coq_version='8.11.2', build_result=ProjectBuildResult(exit_code=0, stdout="coq_makefile -f _CoqProject -o Makefile.coq\nmake -f Makefile.coq\nmake[1]: Entering directory '/home/atouchet/projects/PEARLS/repos_full/htt'\nCOQDEP VFILES\nCOQC Core/pred.v\nCOQC Core/prelude.v\nCOQC Core/idynamic.v\nCOQC Core/pperm.v\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_trans is deprecated; use perm_trans instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: perm_eq_mem is deprecated; use perm_mem instead\nWarning: p...
      dirpath = PosixPath('/tmp/tmps9egiyk2/a')
      filename = 'Core/pred.v'
      commands = VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import ssreflect ssrbool ssrfun., location=SexpInfo.Loc(filename='Core/pred.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=39)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import eqtype seq., location=SexpInfo.Loc(filename='Core/pred.v', lineno=2, bol_pos=74, lineno_last=2, bol_pos_last=74, beg_charno=74, e...
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/build_cache.py", line 764, in write_coq_file
    for sentence in self.sorted_sentences():
      self = VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import ssreflect ssrbool ssrfun., location=SexpInfo.Loc(filename='Core/pred.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=39)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import eqtype seq., location=SexpInfo.Loc(filename='Core/pred.v', lineno=2, bol_pos=74, lineno_last=2, bol_pos_last=74, beg_charno=74, e...
      filepath = PosixPath('/tmp/tmps9egiyk2/a/Core/pred.v')
      lines = ['']
      linenos = [0]
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/build_cache.py", line 742, in sorted_sentences
    sorted_sentences = VernacSentence.sort_sentences(sorted_sentences)
      self = VernacCommandDataList(commands=[VernacCommandData(identifier=[], command=VernacSentence(text=Require Import ssreflect ssrbool ssrfun., location=SexpInfo.Loc(filename='Core/pred.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=39)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), command_error=None), VernacCommandData(identifier=[], command=VernacSentence(text=From mathcomp Require Import eqtype seq., location=SexpInfo.Loc(filename='Core/pred.v', lineno=2, bol_pos=74, lineno_last=2, bol_pos_last=74, beg_charno=74, e...
      sorted_sentences = [VernacSentence(text=Require Import ssreflect ssrbool ssrfun., location=SexpInfo.Loc(filename='Core/pred.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=39)), VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), VernacSentence(text=From mathcomp Require Import eqtype seq., location=SexpInfo.Loc(filename='Core/pred.v', lineno=2, bol_pos=74, lineno_last=2, bol_pos_last=74, beg_charno=74, end_charno=113)), VernacSentence(text=Set Implicit Arguments., location=SexpInfo.Loc(filename='Core/pred.v', lineno=3, bol_pos=115, lineno_last=3, bol_pos_last=115, beg_charno=115, end_charno=137)), VernacSentence(text=Unset Strict Implicit., location=SexpInf...
      idx = 195
      c = VernacCommandData(identifier=['ImageIm'], command=VernacSentence(text=Lemma ImageIm A B C (f1 : B -> C) (f2 : A -> B) (X : Pred A) : Image f1 (Image f2 X) =p Image (f1 \o f2) X., location=SexpInfo.Loc(filename='Core/pred.v', lineno=575, bol_pos=22446, lineno_last=576, bol_pos_last=22510, beg_charno=22446, end_charno=22561)), command_error=None)
  File "/home/atouchet/projects/prism/development/repos/prism/pearls/prism/data/build_cache.py", line 362, in sort_sentences
    return [s for _, s in sorted([(s.location, s) for s in sentences])]
      sentences = [VernacSentence(text=Require Import ssreflect ssrbool ssrfun., location=SexpInfo.Loc(filename='Core/pred.v', lineno=0, bol_pos=0, lineno_last=0, bol_pos_last=0, beg_charno=0, end_charno=39)), VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), VernacSentence(text=Require Import Setoid Morphisms., location=SexpInfo.Loc(filename='Core/pred.v', lineno=1, bol_pos=41, lineno_last=1, bol_pos_last=41, beg_charno=41, end_charno=72)), VernacSentence(text=From mathcomp Require Import eqtype seq., location=SexpInfo.Loc(filename='Core/pred.v', lineno=2, bol_pos=74, lineno_last=2, bol_pos_last=74, beg_charno=74, end_charno=113)), VernacSentence(text=Set Implicit Arguments., location=SexpInfo.Loc(filename='Core/pred.v', lineno=3, bol_pos=115, lineno_last=3, bol_pos_last=115, beg_charno=115, end_charno=137)), VernacSentence(text=Unset Strict Implicit., location=SexpInf...
builtins.TypeError: '<' not supported between instances of 'VernacSentence' and 'VernacSentence'
tom-p-reichel commented 1 year ago 
@@ -359,7 +359,7 @@ class VernacSentence:
         from different documents can still be sorted together (although
         the significance of the results may be suspect).
         """
-        return [s for _, s in sorted([(s.location, s) for s in sentences])]
+        return sorted(sentences,key=lambda s:s.location)

The problem seems to occur when a list of sentences that come from different documents are sorted together (or if the same sentence or one that overlaps occur in the list) If two sentences have the exact same position, sorted will try to tiebreak by the second item in the tuple, the sentence itself. However, dataclasses aren't ordered by default.

A simple fix would be to sort using only the location by use of a sort key. Though, I'm not sure why sentences from multiple files would be sorted together.

I'll stick this commit in a to-be-made PR.