pytact.scripts.print_tactic_hash

 1"""Print information about all executions of a tactic with a given hash in the dataset."""
 2
 3from pathlib import Path
 4import sys
 5from pytact.data_reader import data_reader
 6
 7from collections import defaultdict
 8
 9def main():
10    identities = defaultdict(list)
11
12    dataset_path = Path(sys.argv[1]).resolve()
13    hid = int(sys.argv[2])
14    with data_reader(dataset_path) as data:
15        for datafile in data.values():
16            for d in datafile.definitions():
17                if proof := d.proof:
18                    for step in proof:
19                        for outcome in step.outcomes:
20                            if tac := outcome.tactic:
21                                if tac.ident == hid:
22                                    print(f"{tac.ident}\n  {datafile.filename}\n  {d.name}\n  "
23                                        f"{tac.text}\n  {tac.base_text}\n  {len(outcome.tactic_arguments)} arguments")
24
25if __name__ == "__main__":
26    exit(main())