Parser error on large QuickChick properties

[anton-trunov]

Here is an example that demonstrates the issue.

From Coq Require Import Arith.
From QuickChick Require Import QuickChick.
Set Warnings "-extraction-opaque-accessed,-extraction".

QuickChick (fun n : nat =>
  n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n =?
  n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n
).

Running

$ alectryon.py --expect-unexpected --frontend coq+rst --backend webpage foo.v -o foo.html

produces IndexError: pop from empty list.

I noticed that QuickChick pretty-prints the property above as follows:

$ coqc foo.v
QuickChecking (fun n : nat =>
 n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n +
 n + n + n + n + n + n + n + n + n + n + n + n + n =?
 n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n +
 n + n + n + n + n + n + n + n + n + n + n + n + n)
Finished, 5 targets (0 cached) in 00:00:01.
+++ Passed 10000 tests (0 discards)

Here is the traceback:

$ alectryon --traceback  --expect-unexpected --frontend coq+rst --backend webpage foo.v -o foo.html
Traceback (most recent call last):
  File "/usr/local/bin/alectryon", line 8, in <module>
    sys.exit(main())
  File "/usr/local/lib/python3.9/site-packages/alectryon/cli.py", line 643, in main
    process_pipelines(args)
  File "/usr/local/lib/python3.9/site-packages/alectryon/cli.py", line 632, in process_pipelines
    state = call_pipeline_step(step, state, ctx)
  File "/usr/local/lib/python3.9/site-packages/alectryon/cli.py", line 597, in call_pipeline_step
    return step(state, **{p: ctx[p] for p in params})
  File "/usr/local/lib/python3.9/site-packages/alectryon/cli.py", line 111, in gen_rstcoq_html
    return _gen_docutils_html(coq, fpath, webpage_style,
  File "/usr/local/lib/python3.9/site-packages/alectryon/cli.py", line 97, in _gen_docutils_html
    return publish_string(
  File "/usr/local/lib/python3.9/site-packages/docutils/core.py", line 407, in publish_string
    output, pub = publish_programmatically(
  File "/usr/local/lib/python3.9/site-packages/docutils/core.py", line 665, in publish_programmatically
    output = pub.publish(enable_exit_status=enable_exit_status)
  File "/usr/local/lib/python3.9/site-packages/docutils/core.py", line 219, in publish
    self.apply_transforms()
  File "/usr/local/lib/python3.9/site-packages/docutils/core.py", line 200, in apply_transforms
    self.document.transformer.apply_transforms()
  File "/usr/local/lib/python3.9/site-packages/docutils/transforms/__init__.py", line 171, in apply_transforms
    transform.apply(**kwargs)
  File "/usr/local/lib/python3.9/site-packages/alectryon/docutils.py", line 251, in apply
    self.apply_coq()
  File "/usr/local/lib/python3.9/site-packages/alectryon/docutils.py", line 212, in apply_coq
    generator, annotated = self.annotate(pending_nodes, config)
  File "/usr/local/lib/python3.9/site-packages/alectryon/docutils.py", line 194, in annotate
    return self.annotate_cached(chunks, sertop_args)
  File "/usr/local/lib/python3.9/site-packages/alectryon/docutils.py", line 187, in annotate_cached
    annotated = annotate(chunks, sertop_args)
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 356, in annotate
    return [api.run(chunk) for chunk in chunks]
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 356, in <listcomp>
    return [api.run(chunk) for chunk in chunks]
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 327, in run
    messages.extend(self._exec(span_id, chunk))
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 271, in _exec
    messages = list(self._collect_messages(ApiMessage, chunk, sid))
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 238, in _collect_messages
    for response in self._deserialize_response(self.next_sexp()):
  File "/usr/local/lib/python3.9/site-packages/alectryon/core.py", line 129, in next_sexp
    sexp = sx.load(response)
  File "/usr/local/lib/python3.9/site-packages/alectryon/sexp.py", line 77, in load
    return parse(tokenize(bs))
  File "/usr/local/lib/python3.9/site-packages/alectryon/sexp.py", line 71, in parse
    top = stack.pop()
IndexError: pop from empty list

[cpitclaudel]

Looks like more output confusion due to mixing plain text from QuickChick with control messages from SerAPI:

  File "alectryon/core.py", line 139, in next_sexp
    sexp = sx.load(response)
    response = b' n + n + n + n + n + n + n + n + n + n + n + n + n)\n'
    self = <alectryon.core.SerAPI object at 0x7f9354c2da90>

  File "alectryon/sexp.py", line 77, in load
    return parse(tokenize(bs))
    bs = b' n + n + n + n + n + n + n + n + n + n + n + n + n)\n'

  File "alectryon/sexp.py", line 71, in parse
    top = stack.pop()
    stack = []
    tok = 41
    tokens = <generator object tokenize at 0x7f9354bb6510>
    top = [b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n', b'+', b'n']

IndexError: pop from empty list

IOW, the problem is that Alectryon attempts to part that last line as a SEXP and fails due to the mismatched parenthesis. I've pushed a patch to ignore all lines that fail to parse in --expect-unexpected.

[anton-trunov]

Is it possible to make a new release with the bug fix for this issue?

[cpitclaudel]

Done, 1.2 should be live soon.

[anton-trunov]

Awesome! Thanks.