Edit on GitHub

pytact.scripts.lemmas_new_tactic

Calculate all lemmas in the testing set whose proofs contain tactics that were never seen during training.

View Source

 1"""Calculate all lemmas in the testing set whose proofs contain tactics that
 2were never seen during training."""
 3
 4from pathlib import Path
 5import sys
 6from pytact.data_reader import data_reader, Original
 7
 8test_packages = set([
 9    "coq-bits.1.1.0",
10    "coq-qcert.2.2.0",
11    "coq-ceres.0.4.0",
12    "coq-corn.8.16.0",
13    "coq-bytestring.0.9.0",
14    "coq-hammer.1.3.2+8.11",
15    "coq-gaia-stern.1.15",
16    "coq-mathcomp-apery.1.0.1",
17    "coq-tlc.20200328",
18    "coq-iris-heap-lang.3.4.0",
19    "coq-printf.2.0.0",
20    "coq-smtcoq.2.0+8.11",
21    "coq-topology.10.0.1"
22    "coq-haskell.1.0.0",
23    "coq-bbv.1.3",
24    "coq-poltac.0.8.11",
25    "coq-mathcomp-odd-order.1.14.0",
26    "coq-hott.8.11"
27])
28
29def main():
30    train_tactics = set()
31
32    dataset_path = Path(sys.argv[1]).resolve()
33    with data_reader(dataset_path) as data:
34        for f in data.values():
35            if f.filename.parts[0] in test_packages:
36                continue
37            for d in f.definitions():
38                if not isinstance(d.status, Original):
39                    continue
40                if proof := d.proof:
41                    for step in proof:
42                        if (t := step.tactic) is not None:
43                            train_tactics.add(t.ident)
44
45        for f in data.values():
46            if f.filename.parts[0] not in test_packages:
47                continue
48            for d in f.definitions():
49                if not isinstance(d.status, Original):
50                    continue
51                if proof := d.proof:
52                    fail = False
53                    for step in proof:
54                        if step.tactic is not None and step.tactic.ident not in train_tactics:
55                            fail = True
56                    if not fail:
57                        print(d.name)
58
59if __name__ == "__main__":
60    exit(main())

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

def main(): View Source

30def main():
31    train_tactics = set()
32
33    dataset_path = Path(sys.argv[1]).resolve()
34    with data_reader(dataset_path) as data:
35        for f in data.values():
36            if f.filename.parts[0] in test_packages:
37                continue
38            for d in f.definitions():
39                if not isinstance(d.status, Original):
40                    continue
41                if proof := d.proof:
42                    for step in proof:
43                        if (t := step.tactic) is not None:
44                            train_tactics.add(t.ident)
45
46        for f in data.values():
47            if f.filename.parts[0] not in test_packages:
48                continue
49            for d in f.definitions():
50                if not isinstance(d.status, Original):
51                    continue
52                if proof := d.proof:
53                    fail = False
54                    for step in proof:
55                        if step.tactic is not None and step.tactic.ident not in train_tactics:
56                            fail = True
57                    if not fail:
58                        print(d.name)