import json
import glob
path_dir = [

]

# fs = [json.load(open(x)) for x in glob.glob('')]
# fs = [json.load(open(x)) for x in glob.glob()]
fs = []
for p_d in path_dir: 
    fs_temp = [json.load(open(x)) for x in glob.glob(p_d)]
    fs += fs_temp


# fs = [json.load(open(x)) for x in glob.glob()]

# fs = [json.load(open(x)) for x in glob.glob()]

calculated_theorem = []
n = 0
ns = 0

identical_f = {}
for f in fs:
    for result in f['results']:
        full_name = result['example']['full_name']
        # else:
        if result['success']:
            identical_f[full_name] = result
        elif full_name not in identical_f:
            identical_f[full_name] = result
all_success = []
# for f in fs:
    # print(f)
for result in identical_f.values():
    if result['example']['full_name'] in calculated_theorem:
        print(result['example']['full_name'])
        continue
    calculated_theorem.append(result['example']['full_name'])
    # Skip Lean Dojo init failures (only occurred on LeanDojo Mathlib)
    n += 1
    if result['attempt_results'][0]['failure_reason'].startswith("DojoInitError"):
        continue
    
    if result['success']:
        all_success.append(result['example']['full_name'])
        ns += 1
        
print(all_success)

print(ns/n, ns, n)
