Run Agda setup with als (WebAssembly build, with 2.7.0.1)

.benchmark.txt

-- ./Agda/Builtin/Bool.agda
Total           160ms       
Miscellaneous     0ms       
Typing           48ms (75ms)
Typing.TypeSig   24ms       
Serialization    23ms (32ms)
Scoping          23ms (25ms)
Deserialization  21ms (23ms)
Parsing           7ms (14ms)
Highlighting     11ms       

-- ./Agda/Builtin/Char/Properties.agda
Total           173ms       
Miscellaneous    16ms       
Typing           38ms (65ms)
Typing.CheckLHS  17ms (17ms)
Serialization    22ms (28ms)
Parsing          18ms (27ms)
Scoping          12ms (15ms)
Coverage         15ms (15ms)
Deserialization  13ms (15ms)
Highlighting     12ms       
Termination       6ms (11ms)

-- ./Agda/Builtin/Char.agda
Total         10ms 
Miscellaneous 10ms 

-- ./Agda/Builtin/Coinduction.agda
Total         7ms 
Miscellaneous 7ms 

-- ./Agda/Builtin/Cubical/Equiv.agda
Total                      838ms        
Miscellaneous               23ms        
Typing                     191ms (458ms)
Typing.CheckRHS            117ms        
Typing.TypeSig              74ms        
Typing.CheckLHS             61ms  (61ms)
Typing.OccursCheck          13ms        
Parsing                     30ms (107ms)
Parsing.OperatorsExpr       63ms        
Parsing.OperatorsPattern    12ms        
Serialization               65ms  (82ms)
Serialization.BinaryEncode  10ms        
Scoping                     44ms  (55ms)
Scoping.InverseScopeLookup  11ms        
Positivity                  33ms        
Deserialization             21ms  (26ms)
Highlighting                19ms        
DeadCode                     0ms  (17ms)
DeadCode.DeadCodeReachable  16ms        
InterfaceInstantiateFull    13ms        
Coverage                    11ms  (11ms)

-- ./Agda/Builtin/Cubical/Glue.agda
Total           53ms       
Miscellaneous    8ms       
Typing          24ms (25ms)
Deserialization 13ms (13ms)
Parsing          7ms (11ms)

-- ./Agda/Builtin/Cubical/HCompU.agda
Total         25ms 
Miscellaneous  7ms 
Parsing       18ms 

-- ./Agda/Builtin/Cubical/Id.agda
Total           78ms       
Miscellaneous    8ms       
Typing          34ms (65ms)
Typing.TypeSig  15ms       
Typing.CheckLHS  4ms (12ms)
Parsing         10ms (16ms)
Coverage         5ms (11ms)

-- ./Agda/Builtin/Cubical/Path.agda
Total         18ms 
Miscellaneous  6ms 
Parsing       11ms 

-- ./Agda/Builtin/Cubical/Sub.agda
Total         8ms 
Miscellaneous 8ms 

-- ./Agda/Builtin/Equality/Erase.agda
Total         9ms 
Miscellaneous 9ms 

-- ./Agda/Builtin/Equality/Rewrite.agda
Total         8ms 
Miscellaneous 8ms 

-- ./Agda/Builtin/Equality.agda
Total         6ms 
Miscellaneous 6ms 

-- ./Agda/Builtin/Float/Properties.agda
Total           216ms       
Miscellaneous    30ms       
Typing           51ms (57ms)
Serialization    30ms (43ms)
Deserialization  35ms (39ms)
Parsing          23ms (27ms)
Scoping          17ms (20ms)
Import           13ms       
Highlighting     12ms       

-- ./Agda/Builtin/Float.agda
Total           38ms 
Miscellaneous    7ms 
Deserialization 19ms 
Parsing         11ms 

-- ./Agda/Builtin/FromNat.agda
Total           28ms       
Miscellaneous    8ms       
Deserialization 13ms (13ms)
Parsing          7ms (10ms)

-- ./Agda/Builtin/FromNeg.agda
Total         15ms       
Miscellaneous  7ms       
Parsing        8ms (10ms)

-- ./Agda/Builtin/FromString.agda
Total           22ms       
Miscellaneous    8ms       
Deserialization 13ms (13ms)

-- ./Agda/Builtin/Int.agda
Total           19ms 
Miscellaneous    6ms 
Deserialization 13ms 

-- ./Agda/Builtin/IO.agda
Total         6ms 
Miscellaneous 6ms 

-- ./Agda/Builtin/List.agda
Total         6ms 
Miscellaneous 6ms 

-- ./Agda/Builtin/Maybe.agda
Total         8ms 
Miscellaneous 8ms 

-- ./Agda/Builtin/Nat.agda
Total         18ms 
Miscellaneous  8ms 
Parsing       10ms 

-- ./Agda/Builtin/Reflection/External.agda
Total                      715ms        
Miscellaneous               19ms        
Typing                     140ms (247ms)
Typing.TypeSig              61ms        
Typing.CheckLHS             18ms  (18ms)
Typing.CheckRHS             12ms        
Parsing                     41ms (196ms)
Parsing.OperatorsExpr      135ms        
Parsing.OperatorsPattern    20ms        
Serialization              105ms (126ms)
Serialization.BinaryEncode  12ms        
Scoping                     47ms  (56ms)
Deserialization             41ms  (48ms)
Highlighting                33ms        
InterfaceInstantiateFull    13ms        
DeadCode                     0ms  (11ms)
DeadCode.DeadCodeReachable  10ms        

-- ./Agda/Builtin/Reflection/Properties.agda
Total           35ms       
Miscellaneous    8ms       
Deserialization 26ms (27ms)

-- ./Agda/Builtin/Reflection.agda
Total           60ms 
Miscellaneous    7ms 
Parsing         31ms 
Deserialization 21ms 

-- ./Agda/Builtin/Sigma.agda
Total         7ms 
Miscellaneous 7ms 

-- ./Agda/Builtin/Size.agda
Total         6ms 
Miscellaneous 6ms 

-- ./Agda/Builtin/Strict.agda
Total         8ms 
Miscellaneous 8ms 

-- ./Agda/Builtin/String/Properties.agda
Total           24ms       
Miscellaneous    9ms       
Deserialization 15ms (15ms)

-- ./Agda/Builtin/String.agda
Total           29ms 
Miscellaneous    6ms 
Deserialization 23ms 

-- ./Agda/Builtin/TrustMe.agda
Total         9ms 
Miscellaneous 9ms 

-- ./Agda/Builtin/Unit.agda
Total         7ms 
Miscellaneous 7ms 

-- ./Agda/Builtin/Word/Properties.agda
Total         10ms 
Miscellaneous 10ms 

-- ./Agda/Builtin/Word.agda
Total         6ms 
Miscellaneous 6ms 

-- ./Agda/Primitive/Cubical.agda
Total         5ms 
Miscellaneous 5ms 

-- ./Agda/Primitive.agda
Total         7ms 
Miscellaneous 7ms 

run_agda_setup_with_als.py

#!/usr/bin/env python

from typing import IO, Dict
import json
import os
from pathlib import Path
import re
import subprocess
import time


def rpcenc(content):
    content['jsonrpc'] = '2.0'
    payload = json.dumps(content)
    sz = len(payload)
    return f'Content-Length: {sz}\r\n\r\n{payload}'

def reqdict(idx, method, params):
    return {
        'id': idx,
        'method': method,
        'params': params,
    }

def notidict(method, params):
    return {
        'method': method,
        'params': params,
    }

def respdict(idx, params = None):
    return {
        'id': idx,
        'result': params,
    }

def iotcmreqs(iotcms, n):
    def _makereq(pair):
        idx, (label, cmd) = pair
        return (label, reqdict(n + idx, 'agda', { "tag": "CmdReq", "contents": cmd }))
    return map(_makereq, enumerate(iotcms))

def send(f: IO[bytes], msg: Dict):
    f.write(rpcenc(msg).encode())
    f.flush()

#############################################################################

dirname = Path(__file__).resolve().parent
agdadatadir = str((dirname / '..' / '..').resolve())

print(f'{dirname = }')
print(f'{agdadatadir = }')

iotcms = []
with open('file-list', 'r') as f:
    for ent in f:
        ent = ent.strip()
        if not ent or ent[0] == '#': continue

        entrepr = json.dumps(str((dirname / ent).resolve()))
        cmdpre = f'IOTCM {entrepr} None Indirect'
        iotcms.append((ent,  f'{cmdpre} (Cmd_load {entrepr} [])'))
        iotcms.append((None, f'{cmdpre} (Cmd_no_metas)'))

tosend = [
    (None, reqdict(0, 'initialize', {
        'processId': None,
        'rootUri': '',
        'capabilities': {},
        'trace': 'verbose',
    })),
    (None, notidict('initialized', {})),
    *iotcmreqs(iotcms, 1),
    (None, reqdict(len(iotcms) + 1, 'agda', { 'tag': 'CmdReqSYN' })),
]

print('Launching Agda language server...')

proc = subprocess.Popen(
    [
        'node', 
        '/home/qbane/agda-project/wasm-run/wasm-run.mjs', 
        '/home/qbane/Downloads/als-local-opt.wasm',
        '+AGDA', '--profile=internal', '-AGDA',
        '+RTS', '-V1', '-RTS',
    ],
    stdin=subprocess.PIPE,
    stdout=subprocess.PIPE,
    env={
        'Agda_datadir': agdadatadir,
        'PATH': os.environ.get('PATH', ''),
    })

starttime = time.time()

stdin: IO[bytes] | None = proc.stdin
assert stdin is not None
stdout: IO[bytes] | None = proc.stdout
assert stdout is not None

runninginfo = {}
# the running info msg is send at the NEXT command
label = None

for idx, (_nextlabel, outmsg) in enumerate(tosend):
    print(f'---------------------- Sending msg {idx + 1}/{len(tosend)} ---------------------- ')
    print('<-- params.contents', outmsg.get('params', {}).get('contents'))
    send(stdin, outmsg)

    if 'id' not in outmsg:
        continue

    ack = False

    buf = []
    while True:
        data = stdout.readline()
        nbytes = -1
        if mat := re.match(br'Content-Length:\s+(\d+)', data, re.IGNORECASE):
            nbytes = int(mat.group(1))
        assert nbytes >= 0, 'ERROR consuming headers'
        nl = stdout.read(2)
        assert nl == b'\r\n', 'ERROR consuming message boundary'
        raw = stdout.read(nbytes)
        inmsg = json.loads(raw)

        if 'result' in inmsg:
            print('--> RESP', inmsg['id'], inmsg)
            if inmsg['id'] == outmsg['id']:
                ack = True
            if inmsg['result'].get('tag') == 'CmdRes' and inmsg['result'].get('contents'):
                print(inmsg['result'].get('contents'))
                raise Exception('Encounter ERROR sending IOTCM command')

            if inmsg['result'].get('tag') == 'CmdResACK':
                # ACK response
                break

            if inmsg['id'] == 0:
                # init result
                break
        elif 'id' not in inmsg:
            print('--> NOTI', inmsg['method'], inmsg['params'])
        else:
            print('--> REQ', inmsg['id'], inmsg['params'])
            send(stdin, respdict(inmsg['id']))

            msgtag = inmsg['params'].get('tag') 
            if msgtag == 'ResponseRunningInfo':
                if label is not None:
                    if label not in runninginfo:
                        runninginfo[label] = []
                    runninginfo[label].append(inmsg['params']['contents'][1])
            elif msgtag == 'ResponseEnd':
                break

    assert ack, 'Did not receive ACK'

    print('--- DONE ---\n')
    label = _nextlabel

print('Shutting down language server (The "Got EOF" error is fine)...')
stdin.close()
exitcode = proc.wait()

endtime = time.time()

assert exitcode == 0
print(f'All done! Elapsed time: {endtime - starttime:.03f}s')

with open('benchmark.txt', 'w') as f:
    for label, msgs in runninginfo.items():
        f.write(f'-- {label}\n')
        for msg in msgs:
            f.write(msg)
        f.write('\n')