Edit on GitHub

pytact.scripts.ssreflect_dependees

Find all lemmas that depend on ssreflect (approximation)

View Source

 1"""Find all lemmas that depend on ssreflect (approximation)"""
 2
 3from pathlib import Path
 4import sys
 5from pytact.data_reader import data_reader, Original
 6from pytact.graph_visualize_browse import transitive_closure
 7
 8ssr_classification = {
 9    "coq-bits.1.1.0": True,
10    "coq-qcert.2.2.0": False,
11    "coq-ceres.0.4.0": False,
12    "coq-corn.8.16.0": False,
13    "coq-bytestring.0.9.0": False,
14    "coq-hammer.1.3.2+8.11": False,
15    "coq-gaia-stern.1.15": True,
16    "coq-mathcomp-apery.1.0.1": True,
17    "coq-tlc.20200328": False,
18    "coq-iris-heap-lang.3.4.0": True,
19    "coq-printf.2.0.0": False,
20    "coq-smtcoq.2.0+8.11": False,
21    "coq-topology.10.0.1": False,
22    "coq-haskell.1.0.0": False,
23    "coq-bbv.1.3": False,
24    "coq-poltac.0.8.11": False,
25    "coq-mathcomp-odd-order.1.14.0": True,
26    "coq-hott.8.11": False,
27}
28
29def main():
30    ssr_lemmas = set()
31    normal_lemmas = set()
32    dataset_path = Path(sys.argv[1]).resolve()
33    with data_reader(dataset_path) as data:
34        trans_deps = transitive_closure({d.filename: list(d.dependencies)
35                                            for d in data.values()})
36        ssr = Path('coq-tactician-stdlib.8.11.dev/plugins/ssr/ssreflect.bin')
37        ssr_dependees = [ d for d in data.keys() if ssr in trans_deps[d]]
38        for f in data.keys():
39            if f.parts[0] in ssr_classification:
40                if (f in ssr_dependees) != ssr_classification[f.parts[0]]:
41                    print(f)
42            # for d in data[f].definitions():
43            #     if not isinstance(d.status, Original):
44            #         continue
45            #     if proof := d.proof:
46            #         if f in ssr_dependees:
47            #             ssr_lemmas.add(d.name)
48            #         else:
49            #             normal_lemmas.add(d.name)
50
51    # for l in ssr_lemmas:
52    #     print(l)
53    for l in normal_lemmas:
54        print(l)
55
56if __name__ == "__main__":
57    exit(main())

ssr_classification = {'coq-bits.1.1.0': True, 'coq-qcert.2.2.0': False, 'coq-ceres.0.4.0': False, 'coq-corn.8.16.0': False, 'coq-bytestring.0.9.0': False, 'coq-hammer.1.3.2+8.11': False, 'coq-gaia-stern.1.15': True, 'coq-mathcomp-apery.1.0.1': True, 'coq-tlc.20200328': False, 'coq-iris-heap-lang.3.4.0': True, 'coq-printf.2.0.0': False, 'coq-smtcoq.2.0+8.11': False, 'coq-topology.10.0.1': False, 'coq-haskell.1.0.0': False, 'coq-bbv.1.3': False, 'coq-poltac.0.8.11': False, 'coq-mathcomp-odd-order.1.14.0': True, 'coq-hott.8.11': False}

def main(): View Source

30def main():
31    ssr_lemmas = set()
32    normal_lemmas = set()
33    dataset_path = Path(sys.argv[1]).resolve()
34    with data_reader(dataset_path) as data:
35        trans_deps = transitive_closure({d.filename: list(d.dependencies)
36                                            for d in data.values()})
37        ssr = Path('coq-tactician-stdlib.8.11.dev/plugins/ssr/ssreflect.bin')
38        ssr_dependees = [ d for d in data.keys() if ssr in trans_deps[d]]
39        for f in data.keys():
40            if f.parts[0] in ssr_classification:
41                if (f in ssr_dependees) != ssr_classification[f.parts[0]]:
42                    print(f)
43            # for d in data[f].definitions():
44            #     if not isinstance(d.status, Original):
45            #         continue
46            #     if proof := d.proof:
47            #         if f in ssr_dependees:
48            #             ssr_lemmas.add(d.name)
49            #         else:
50            #             normal_lemmas.add(d.name)
51
52    # for l in ssr_lemmas:
53    #     print(l)
54    for l in normal_lemmas:
55        print(l)