#!/usr/bin/env python3

import sys
import subprocess

def doit(todo):
  print('')

  input = ''
  expectedtowork = False
  for line in todo:
    expectedtowork = ' # ok' in line
    # note: only the last line matters
    print('< '+line)
    input += line.split(' #')[0].strip()+'\n'
  if todo == ['HOLTrace 1']: expectedtowork = True

  for cmd in './holtrace-verify','./holtrace-verify-simple':
    print(cmd)
    result = subprocess.run([cmd],input=input,text=True,capture_output=True)
    for label,what in ('stdout:',result.stdout),('>',result.stderr):
      what = what.splitlines()
      if len(what) == 0: continue
      if len(what) > 1: print(f'{label} ...')
      print(f'{label} {what[-1]}')
    if result.returncode == 0:
      print('success')
    else:
      print('failure',result.returncode)
    if expectedtowork != (result.returncode == 0):
      print('ALERT')

def main():
  doit([])
  doit([''])
  doit(['b0bool'])
  doit(['HOLTrace'])
  doit(['HOLTrace 1'])

  todo = ['HOLTrace 1']
  for line in sys.stdin:
    line = line.strip()
    if len(line) == 0:
      if todo != ['HOLTrace 1']: doit(todo)
      todo = ['HOLTrace 1']
      continue
    if line[0] == '#': continue
    todo += [line]
  if todo != ['HOLTrace 1']: doit(todo)
  todo = []

if __name__ == '__main__':
  main()