search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Stackoverflow #8

Closed thery closed 3 years ago

thery commented 3 years ago

Hi, i am trying to generate the doc on a library and alectryon seems to have problem on large proofs. Here are two examples of errors I get.

Exiting early due to an error:
Unexpected response: b'sertop: internal error, uncaught exception:\n'
Full output: b'        Stack overflow\n        \n(Answer query130389(CoqExn((loc())(stm_ids())(backtrace(Backtrace()))(exn Not_found)(pp(Pp_glue((Pp_box(Pp_hovbox 0)(Pp_glue((Pp_string Anomaly)(Pp_print_break 1 0)(Pp_box(Pp_hbox 0)(Pp_glue((Pp_glue((Pp_string'

and

Unexpected response: b'sertop: internal error, uncaught exception:\n'
Full output: b'        Stack overflow\n        \n(Of_sexp_error"sertop/sertop_ser.ml.cmd_of_sexp: unexpected sum tag"(invalid_sexp(query130332(Print((sid 1639)(pp((pp_format PpStr)(pp_depth 30)(pp_margin 50))))(CoqExpr((v(CNotation(InConstrEntrySomeLevel"_ <= _")((((v(CApp(()((v(CRef((v(Ser_Qualid(DirPath())(Id Rabs)))(loc()))()))(loc())))((((v(CRef((v(Ser_Qualid(DirPath())(Id e2)))(loc()))()))(loc()))()))))(loc()))((v(CNotation(InConstrEntrySomeLevel"_ * _")((((v(CNotation(InConstrEntrySomeLevel"/ _")((((v(CPrim(Numeral SPlus((int 2)(frac"")(exp"")))))(loc())))()()())))(loc()))((v(CApp(()((v(CRef((v(Ser_Qualid(DirPath())(Id ulp)))(loc()))()))(loc())))((((v(CNotation(InConstrEntrySomeLevel"_ + _")((((v(CNotation(InConstrEntrySomeLevel"_ * _")(((('

Is there something I can do?

cpitclaudel commented 3 years ago

Hi Laurent,

Looks like a SerAPI bug: it seems to be stack-overflowing on something. Do you have the input file? Alternatively we can record the commands that Alectryon sends to SerAPI to create a repro. Here's an example:

$ echo "Print nat." > test.v
$ alectryon --debug test.v | grep '>>' | sed 's/^>> //' > sertop.in
$ sertop < sertop.in # This should reproduce the error
…
(Answer EOF Ack)
(Answer EOF Completed)

If you can upload the generated sertop.in somewhere we could get @ejgallego's opinion.

ejgallego commented 3 years ago

Indeed, it could even be a Coq bug; send me the concrete file and I will have a look.

thery commented 3 years ago

double.zip I am using coq 8.10 + ssreflect + coq-flocq. The file that is problematic is alectryon.py --frontend coq DWPlus.v fails with

Full output: b'        Stack overflow\n        \n(Of_sexp_error"sertop/sertop_ser.ml.cmd_of_sexp: unexpected sum tag"(invalid_sexp(query130369(Print((sid 1639)(pp((pp_format PpStr)(pp_depth 30)(pp_margin 51))))(CoqExpr((v(CRecord(('
ejgallego commented 3 years ago

Thanks @thery , Coq 8.10 is a bit behind of my current dev setup so i'll take time to reproduce, that could be well a Coq bug; something that would help is to pass --debug to serapi to see the backtrace .

thery commented 3 years ago

I've been using 8.10 because it was written in the doc. But I've just tried with 8.12 and it seems to work : I've managed to compile all the library without any stackoverflow.

Here is the command that fails in 8.10 with the traceback option 

!! Coq raised an exception:
       Stack overflow.
   Results past this point may be unreliable.
Traceback (most recent call last):
  File "/user/thery/home/git/alectryon/alectryon.py", line 26, in <module>
    main()
  File "/home/thery/git/alectryon/alectryon/cli.py", line 612, in main
    process_pipelines(args)
  File "/home/thery/git/alectryon/alectryon/cli.py", line 604, in process_pipelines
    raise e
  File "/home/thery/git/alectryon/alectryon/cli.py", line 601, in process_pipelines
    state = call_pipeline_step(step, state, ctx)
  File "/home/thery/git/alectryon/alectryon/cli.py", line 570, in call_pipeline_step
    return step(state, **{p: ctx[p] for p in params})
  File "/home/thery/git/alectryon/alectryon/cli.py", line 108, in gen_rstcoq_html
    RSTCoqParser, RSTCoqStandaloneReader)
  File "/home/thery/git/alectryon/alectryon/cli.py", line 103, in _gen_docutils_html
    enable_exit_status=True).decode("utf-8")
  File "/user/thery/home/.local/lib/python3.7/site-packages/docutils/core.py", line 417, in publish_string
    enable_exit_status=enable_exit_status)
  File "/user/thery/home/.local/lib/python3.7/site-packages/docutils/core.py", line 665, in publish_programmatically
    output = pub.publish(enable_exit_status=enable_exit_status)
  File "/user/thery/home/.local/lib/python3.7/site-packages/docutils/core.py", line 219, in publish
    self.apply_transforms()
  File "/user/thery/home/.local/lib/python3.7/site-packages/docutils/core.py", line 200, in apply_transforms
    self.document.transformer.apply_transforms()
  File "/user/thery/home/.local/lib/python3.7/site-packages/docutils/transforms/__init__.py", line 171, in apply_transforms
    transform.apply(**kwargs)
  File "/home/thery/git/alectryon/alectryon/docutils.py", line 233, in apply
    self.apply_coq()
  File "/home/thery/git/alectryon/alectryon/docutils.py", line 196, in apply_coq
    annotated = self.annotate(pending_nodes, config)
  File "/home/thery/git/alectryon/alectryon/docutils.py", line 178, in annotate
    return self.annotate_cached(chunks, sertop_args) # if chunks else []
  File "/home/thery/git/alectryon/alectryon/docutils.py", line 171, in annotate_cached
    annotated = annotate(chunks, sertop_args)
  File "/home/thery/git/alectryon/alectryon/core.py", line 349, in annotate
    return [api.run(chunk) for chunk in chunks]
  File "/home/thery/git/alectryon/alectryon/core.py", line 349, in <listcomp>
    return [api.run(chunk) for chunk in chunks]
  File "/home/thery/git/alectryon/alectryon/core.py", line 321, in run
    goals = list(self._goals(span_id, chunk))
  File "/home/thery/git/alectryon/alectryon/core.py", line 301, in _goals
    yield from (self._pprint_goal(g, sid) for g in goals)
  File "/home/thery/git/alectryon/alectryon/core.py", line 301, in <genexpr>
    yield from (self._pprint_goal(g, sid) for g in goals)
  File "/home/thery/git/alectryon/alectryon/core.py", line 293, in _pprint_goal
    hyps = [self._pprint_hyp(h, sid) for h in goal.hypotheses]
  File "/home/thery/git/alectryon/alectryon/core.py", line 293, in <listcomp>
    hyps = [self._pprint_hyp(h, sid) for h in goal.hypotheses]
  File "/home/thery/git/alectryon/alectryon/core.py", line 288, in _pprint_hyp
    htype = self._pprint(hyp.type, sid, b'CoqExpr', d, w - 3).pp
  File "/home/thery/git/alectryon/alectryon/core.py", line 257, in _pprint
    raise ValueError("No string found in Print answer")
ValueError: No string found in Print answer
ejgallego commented 3 years ago

That's very valuable information, thanks @thery , indeed Coq + SerAPI 8.12 fixed literally dozens of bugs, so it is hard to know which one could be responsible.

Regarding the backtrace, I was trying to see Coq's backtrace, not Python, but indeed I have a good guess as what the problem with print is, and IMHO the easiest fix is to move to 8.12 .

cpitclaudel commented 3 years ago

I've been using 8.10 because it was written in the doc. But I've just tried with 8.12 and it seems to work : I've managed to compile all the library without any stackoverflow.

Brilliant, thanks for testing! I agree with @ejgallego here, I think the fix is for me to update the README :)

cpitclaudel commented 3 years ago

I've changed the readme to say Coq ≥ 8.10 and works best with 8.12; @thery OK with you to close this issue?

thery commented 3 years ago

@cpitclaudel fine with me

ejgallego commented 3 years ago

serapi / coq 8.10 / 8.11 have quite a few bugs that could indeed impact alectryon, so IMO it makes sense to recommend 8.12 [and support lower versions at their own risk]

I'm sorry I didn't track all the changes properly, in many cases bugs in Coq are only exposed if using SerAPI due to the extended API as compared to XML / coqtop.