cpitclaudel / alectryon Goto Github PK

Congrats on the release! I was upgrading our code to Coq 8.12, and was wondering whether that's supported — the README doesn't say.

• The README instructs to install opam install coq-serapi=8.10.0+0.7.0 (and yes, it depends on "coq" {>= "8.10.0" & < "8.11"} as you'd expect).
• On 8.11 we've used coq-serapi.8.11.0+0.11.0 for a while, there's also coq-serapi.8.11.0+0.11.1
• On 8.12 the only available release is coq-serapi=8.12.0+0.12.0.

Hi @cpitclaudel, I don't know if this was already in your roadmap :)

It appears the webpage output already contains some anchors <div id="key-words" class="section">, hence the suggestion:

it would be awesome if these anchors could be directly "exposed" to the user, e.g. similarly to how GitHub renders Markdown files:

Hi, I noticed that when presenting material in a class I tend to select some piece of text/code with my mouse, and when doing so the cursor tends to cross a lot of lines and the popup window blinks a lot which might distract the audience.

Having a checkbox that lets us opt out of the default "pop up on mouse hover" behavior seems to be an easy solution. Would that be a good idea?

This comment seems outdated, since the .css is not inlined even if you use the command line interface.

def highlight_html(coqstr):
    """Highlight a Coq string `coqstr`.

    Return a raw HTML string.  This function is just a convenience wrapper
    around Pygments' machinery, using a custom Coq lexer and a custom style.

    The generated code needs to be paired with a Pygments stylesheet, which can
    be generated by running the ``regen_tango_subtle_css.py`` script in the
    ``etc/`` folder of the Alectryon distribution.

    If you use Alectryon's command line interface directly, you won't have to
    jump through that last hoop: it renders and writes out the HTML for you,
    with the appropriate CSS inlined.  It might be instructive to consult the
    implementation of ``alectryon.cli.dump_html_standalone`` to see how the CLI
    does it."""

If it was inlined, I could add a command line option to select another style.

I'd like to pick another style, one close to the default vscode one.

One way would be to keep the css external, maybe rename it to remove "tango", and change the regen_tango_subtle_css.py to take an argument (the style), and the let me generate another style at deploy time.

Another option would be to make this comment true, and add a command line option to pick the style.

What is best?

When I'm using the Alectryon minor mode and in the Coq-view, parsing fails if I have emphasized text at the beginning or the end of a parenthetical, like the following:

(*|

This (**doesn't** work) properly

Neither (does **this**)

(But **this** does)

|*)

Sometimes I want to assert a message talk about the variable X34 without quoting the entire message, eg. "coq complains variable x is illtyped"

Hi, it would be useful to add a -dev for alectryon --version when updating from the git repo

In other words

➜  docs git:(main) ✗ alectryon --version
Alectryon v1.3.1

should report v1.3.2-dev instread, until you release it

I had both a pip3 install and a manual install for #66 and had to debug a couple of things to ensure I had the right files installed

The README mentions --sertop-args, but the help string only talks about --sertop-arg

In our CI pipeline we set our COQPATH up so that it points to artifacts which we pull. Unfortunately, the only way that I've been able to get sertop to find these libraries is by adding something like the following into sphinx/conf.py:

serapi_args = []
coqpaths = os.environ.get("COQPATH", "").split(':')
for coqpath in coqpaths:
    if coqpath.endswith("foo/bar") or coqpath.endswith("baz/qux"):
        serapi_args.extend(["-R", coqpath + ","])

from alectryon.docutils import AlectryonTransform
AlectryonTransform.SERAPI_ARGS = serapi_args

It would be much better in terms of usability if COQPATH could be fed directly into sertop so that users don't need to manually parse their dependencies out and feed them in.

In the paper Untangling Mechanized Proofs there is some nice math rendering for the proof of Gauss.
How is it possible to build this locally? I've found the file hyps.rst but don't know which incantation is needed in order to produce the nice outout.

Within our documentation we are making use of the :ref: role and the :download: role quite heavily. Unfortunately, alectryon.el seems to mark uses of these text-roles as errors (with messages like 'Unknown interpreted text role "ref"') when in the reST view for a .v file with (*| |*) comment blocks.

I'm not very familiar with how alectryon.el is written, but my assumption is that it is simply creating a buffer and transliterating the .v file into it's (isomorphic) .rst form within that buffer. If this is the case, this issue is even more confusing because opening the tangled file manually in emacs (and thus loading the ReST mode directly) doesn't cause the errors to appear.

I have goals with very large context. When hovering over tactics.
I mostly see the initial assumptions. Is there a way to activate some scrolling
or at least have the visible part concentrated on the conclusion?

In coq scripts which contains identifiers with underscores, this character is directly put in the tex file (in particular in the \hypn latex command. For instance the hypothesis H_0 is translated in \begin{hyp}{\hypn{H_0}}, without "_" being escaped nor pygmentized. At the compilation by latex, the classic error about missing dollars interrupts the compilation.

Example

(* underline.v *)

Lemma L (H_0 : 1 = 2)
(H_1 : 2 = 3) :
1 = 3.
Search (?n = S ?n).
Fail eapply lt_trans.
now rewrite H_1.
Qed.

(*

alectryon.py --frontend coq --backend snippets-latex --output-directory . underline.v

pygmentize -S default -f latex > wrapper-underline.pyg

lualatex wrapper-underline.tex

*)

Consider a Coq project organized like this (assume -Q theories Test):

theories/
├── A
│   └── A.v
└── B
    └── A.v

If I call Alectryon as a coqdoc substitute on each these files with --output-directory X, I only get a single file X/A.html in the end. In contrast, coqdoc will generate the files X/Test.A.A.html and X/Test.B.A.html. A more detailed discussion of the coqdoc naming scheme can be found in the coq2html documentation.

Is there a reasonable way of changing the current naming approach to work with the coqdoc scheme?

I'd like to be able to suppress warnings for long lines. But there don't seem to be any relevant flags?

A use case: a PL semantics encoded as an inductive predicate. If that's not hard to add I'd appreciate some pointers :)

AttributeError: 'Values' object has no attribute 'pep_references'
Exiting due to error.  Use "--traceback" to diagnose.
Please report errors to <[email protected]>.
Include "--traceback" output, Docutils version (0.17.1 [release]),
Python version (3.7.3), your OS type & version, and the
command line used.
make: *** [Makefile:1004: alectryon-html-done.timestamp] Error 1

https://github.com/HoTT/HoTT/runs/2369972229#step:6:2123

Is it safe to always run with --traceback? Is it suggested?

Consider the following:

$ cat foo.v
Axiom test : Set.
Check foo.test.
$ ../alectryon/alectryon.py foo.v
!! Coq raised an exception:
       The reference foo.test was not found in the current environment.
   Results past this point may be unreliable.
   The offending chunk is delimited by >>>.<<< below:
       Axiom test : Set.
       Check >>>foo.test<<<.

This causes the Alectryon to not be able to handle HoTT, for example, c.f. https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2158

$ cat foo.v
(* this is a very very very very very very very very very very very very very very very very long comment *)
Check Type.
Check Type.
Check Type.
Check Type.
Check Type.
Check Type.
$ ../alectryon/alectryon.py foo.v
foo.v:7: (WARNING/2) Long line: '(* this is a very very very very very very very very very very very very very very very very long comment *)' (108 characters)

It seems to frequently give warnings on the final line?

We're interested in using Pygments v2.6.1 instead of v2.5.2 (which is currently required). Will there be conflicts if we bump this dependency? If not, it probably makes sense to weaken the dependencies to specify a minimum version of pygments rather than an exact version.

I'd like to be able to click on an identifier in code to jump to it's definition, and click on modules that are Required to jump to their definition. (For example, in https://hott.github.io/HoTT/alectryon-html/HoTT.Classes.interfaces.naturals.html) Additionally, I'd like for the coqdoc generated index links to work (https://hott.github.io/HoTT/alectryon-html/) or else for Alectryon to generate an index for me with links that work. How do I make this happen?

Just use a .v file with

(** printing Derive %\coqdockw{Derive}% *)

coqdoc uses it to configure itself, so it doesn't appear in the output, while alectryon understands it as a comment. This produces a Coqdoc mismatch assertion failure.

Clément,

During Coq bumps at work, we sometimes experience breakages to our documentation caused by delays in corresponding SerAPI bumps on opam. I'm working to engineer a solution locally and I was initially planning to use alectryon.minimal, but I've been running into some problems. In particular, if I try to replace alectryon/alectryon.py with alectryon/alectryon/minimal.py in my Sphinx conf.py file (edit: I changed which pyhon script I invoke for Alectryon within my Makefile), I end up with the following error:

Traceback (most recent call last):
  File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/minimal.py", line 33, in <module>
    from docutils.parsers.rst import directives, roles, Directive # type: ignore
  File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 78, in <module>
    import docutils.frontend
ModuleNotFoundError: No module named 'docutils.frontend'; 'docutils' is not a package
Error in sys.excepthook:
Traceback (most recent call last):
  File "/usr/lib/python3/dist-packages/apport_python_hook.py", line 72, in apport_excepthook
    from apport.fileutils import likely_packaged, get_recent_crashes
  File "/usr/lib/python3/dist-packages/apport/__init__.py", line 5, in <module>
    from apport.report import Report
  File "/usr/lib/python3/dist-packages/apport/report.py", line 32, in <module>
    import apport.fileutils
  File "/usr/lib/python3/dist-packages/apport/fileutils.py", line 26, in <module>
    from apport.packaging_impl import impl as packaging
  File "/usr/lib/python3/dist-packages/apport/packaging_impl.py", line 17, in <module>
    import json
  File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/json.py", line 31, in <module>
    from . import core
ImportError: attempted relative import with no known parent package

Original exception was:
Traceback (most recent call last):
  File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/minimal.py", line 33, in <module>
    from docutils.parsers.rst import directives, roles, Directive # type: ignore
  File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 78, in <module>
    import docutils.frontend
ModuleNotFoundError: No module named 'docutils.frontend'; 'docutils' is not a package

Am I using this file in the wrong way or has this functionality fallen somewhat out of date?

On a related note, how easy would it be for you to add a switch to the regular alectryon.py infrastructure which disables calls to serapi while retaining the regular alectryon functionality? In reality, it seems like we're more interested in a way to avoid breakages caused by bump-lag with serapi; we don't mind very much if we temporarily lose proof movies (if we're able to choose when we want to turn them off).

!! Warning: Unexpected token during syntax-highlighting: '₁'
!! Alectryon's lexer isn't perfect: please send us an example.
!! Context:
        ...carriers_subalgebra A P t &
          in_class (Φ t) x (def_inc_subalgebra A P t y)}
        ∥₋₁./theories/Classes/orders/nat_int.v:176: (WARNING/2) Long line: 'We axiomatize the order on the naturals and the integers as a non trivial' (73 characters)

at https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2547

Hello! Love the project, is there any way to use alectryon as a github action?
For example to publish it to Github Pages?
The README mentions that it could integrate with Sphinx, Docutils, Pelican, readthedocs, Nikola.
Is that the recommended approach?

I'm pretty sure github actions usually use docker, and I could create a dockerfile that essentially does the following

find . -name *.v -exec alectryon.py --frontend coq+rst --backend webpage {} \;

For the moment, alectryon only supports a per sentence way to hide Coq statements. I miss something equivalent to (*begin/end hide *) to remove large chunks of Coq statements like imports, sections, etc.

Is this something that can be supported or is there a particular reason to not support this?
Thanks,

Would it be possible to implement a "quick mode" which would not have any movies but not require building the entire file? E.g. if I've already built my development with coqc, then it would be nice to be able to get non-movie versions generated very quickly.

I'm not sure what to make of

Line 383, character 58, warning: missing newline after ">>" block
Line 19, character 3, warning: unterminated inline ">>"
Line 135, character 6, warning: missing newline after ">>" block
Line 146, character 79, warning: missing newline after ">>" block
Line 115, character 8, warning: missing newline after ">>" block
Line 83, character 65, warning: missing newline after ">>" block
Line 26, character 6, warning: unterminated inline ">>"
Line 32, character 6, warning: unterminated inline ">>"
Line 7, character 6, warning: unterminated inline ">>"
Line 59, character 6, warning: unterminated inline ">>"
Line 347, character 6, warning: unterminated inline ">>"
Line 354, character 6, warning: unterminated inline ">>"
Line 360, character 9, warning: unterminated inline ">>"
Line 14, character 8, warning: unterminated inline ">>"
Line 26, character 8, warning: unterminated inline ">>"
Line 63, character 8, warning: unterminated inline ">>"
Line 87, character 6, warning: unterminated inline ">>"
Line 109, character 6, warning: unterminated inline ">>"
Line 125, character 6, warning: unterminated inline ">>"
Line 17, character 6, warning: unterminated inline ">>"
Line 23, character 6, warning: unterminated inline ">>"
Line 25, character 6, warning: unterminated inline ">>"
Line 151, character 6, warning: unterminated inline ">>"
Line 176, character 6, warning: unterminated inline ">>"
Line 308, character 6, warning: unterminated inline ">>"
Line 128, character 8, warning: unterminated inline ">>"
Line 17, character 6, warning: unterminated inline ">>"
Line 23, character 6, warning: unterminated inline ">>"
Line 93, character 6, warning: unterminated inline ">>"
Line 51, character 6, warning: unterminated inline ">>"
Line 129, character 6, warning: unterminated inline ">>"
Line 279, character 6, warning: unterminated inline ">>"
Line 320, character 6, warning: unterminated inline ">>"
Line 115, character 6, warning: unterminated inline ">>"
Line 127, character 6, warning: unterminated inline ">>"
Line 97, character 24, warning: missing newline after ">>" block
Line 121, character 60, warning: missing newline after ">>" block
Line 197, character 46, warning: missing newline after ">>" block
Line 154, character 14, warning: missing newline after ">>" block
Line 272, character 14, warning: missing newline after ">>" block
Line 367, character 14, warning: missing newline after ">>" block
Line 731, character 9, warning: unterminated inline ">>"
Line 737, character 9, warning: unterminated inline ">>"

at https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2860

Hi @cpitclaudel,

I'm not sure but I believe I found a small bug when processing alectryon.py --frontend coq+rst --backend webpage foo.v

on this foo.v file:

Check nat.
(* .unfold *)

(*| Test

.. code-block:: Coq

   Fixpoint entier_nat_ind (P : entier_nat -> Prop)
   (fZero : P Zero) (fSucc : forall n : entier_nat, P n -> P (Succ n))
   (n : entier_nat) : P n :=
     match n with
     | Zero => fZero
     | Succ n => fSucc n (entier_nat_ind P fZero fSucc n)
     end.
|*)

Check nat.
(* .unfold *)

I got the following page:

Would you have some idea of a fix or a workaround? (for the 2nd "unfold" directive to be processed, I mean)

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?

Hi,

TL;DR: --copy-assets copy copies assets in the input directory. I would have imagined it should copy them in an output directory if provided.

Imagine the following directory structure

./input
./input/d.v 
./output

I want to generate HTML pages in output using

alectryon  --no-header --frontend coqdoc --backend webpage  \
           input/d.v --copy-assets copy -o output/index.html

I get the following instead, forcing a manual move of assets to output

./input
./input/alectryon.css
./input/d.v
./input/alectryon.js
./output
./output/index.html

!! Warning: Unexpected token during syntax-highlighting: '₁'
!! Alectryon's lexer isn't perfect: please send us an example.
!! Context:
        forall x y : A s,
        cong_ker f s x y ->
        (f s x; ❘ (x; 1) ❘₋₁

https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2352

I set up a custom Docker container with Ubuntu (Dockerfile) to be able to run Alectryon with coqdoc on every master branch push for a Coq project. However, I quickly ran into UTF8 encoding issues like this:

'ascii' codec can't encode character '\u2191' in position 6443: ordinal not in range(128)

Note that \u2191 is the "uparrow" Unicode symbol, so the problem came from the use of HEADER in alectryon/html.py.

Even after reading up on Python3 encoding issues, I couldn't figure out exactly where there might be a .encode("utf-8") missing, so I opted to simply remove all UTF8 from all output by Alectryon and coqdoc. However, since the --utf8 option to coqdoc is hardcoded, I had to use a fork of Alectryon (commit). Also, I believe this means the build will break anytime anyone uses an UTF8 character in a Coq file.

Is there a better way to solve this issue? I theorize that one more complete workaround would be to set up a locale (e.g., en_US.UTF8) in the Docker container, but this seems like a cumbersome thing to do in every Docker image where one wants to run Alectryon.

Alectryon translates a "Program Fixpoint" definition into just "Fixpoint"

Require Import Coq.Program.Wf.
Require Import Coq.Arith.Arith.

Program Fixpoint f (n : nat ) {wf lt n} : nat :=
match n with
| 0 => 0
| _ => f (n / 2)
end.

I'm a big fan of the "windowed mode", which essentially gives a display like Proof General. However, with a big proof context that doesn't fully fit on the screen, the focus is always on the top of the context, which typically only changes seldomly in most big proofs. Hence, when I step through a proof, I don't see the changes unless I manually scroll downwards in the proof context window, which is a chore.

Is there a straightforward way to make the focus in the proof context go towards the bottom of the window? I guess this would require additional JavaScript?

When I navigate a document with Ctrl(Cmd)-Down, Alectryon reveals Coq's response but it seems to be impossible to simply close the pop-up window with Coq's response without pressing Ctrl-Down (or Ctrl-Up). Sometimes I just want to have the current line highlighted in bold but no pop-up.

Clicking bubbles does not help in this case because bubbles do not get activated during navigation.

In some of our documentation we dissect each line in a given snippet of Coq code individually. Oftentimes we refer to 'line 2' or 'line 7', but unfortunately Alectryon doesn't (seem to) have support for numbering the snippets in .. coq:: blocks. It would be a nice quality-of-life improvement if line-numbering (similar to how it's done for regular code blocks) was incorporated.

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

With a MELPA-installed alectryon.el and a globally installed alectryon, I got the following error:

Suspicious state from syntax checker alectryon: Flycheck checker alectryon returned 2, but its output contained no errors: /nix/store/66fbv9mmx1j4hrn9y06kcp73c3yb196r-python3-3.8.9/bin/python3: can't open file '/home/theo/.emacs.d/alectryon.py': [Errno 2] No such file or directory

Try installing a more recent version of alectryon, and please open a bug report if the issue persists in the latest release.  Thanks!

I'm suspecting that alectryon.el should also look for an alectryon binary in PATH.

Here is a minimal example:

From QuickChick Require Import QuickChick.
QuickChick (fun _ : bool => true).

This gets stuck with the following error message:

$ alectryon.py --frontend coq+rst --backend webpage quickchick.v -o quickchick.html
Unexpected response: b'QuickChick (fun _ : bool => true)\n'

This example results in an anomaly "grounding a non evar-free term" due to the refine tactic only when run through Alectryon. It has something to do with the evar in the decoder's match: 0 => _.

Class Countable T :=
  inj_countable {
      encode: T -> nat;
      decode: nat -> T;
      encode_decode_ok : forall x, decode (encode x) = x;
    }.

Inductive bin_op :=
  | PlusOp.

Global Instance bin_op_countable : Countable bin_op.
Proof.
  refine (inj_countable bin_op
            (fun op => match op with | PlusOp => 0  end)
            (fun n => match n with | 0 => _ | _ => PlusOp end) _).
  destruct x; auto.
Qed.

After setting alectryon.docutils.CACHE_DIRECTORY, every single one of my .rst files generate a .rst.cache file as it should. Unfortunately, the contents of each file - regardless of what .. coq:: code it contains - are the same "empty" .json:

{
  "metadata": {
    "serapi_args": [
      "-Q",
      "/home/jhaag/dev/bedrock/fm-docs/src,"
    ]
  },
  "chunks": [],
  "annotated": []
}

Whenever I run Alectryon with the coqdoc frontend, e.g.,

alectryon.py --frontend coqdoc --webpage-style windowed \
   --output-directory docs/alectryon theories/Test.v

... I get coqdoc.css in the directory where I ran the command. Looking at coqdoc options, there doesn't seem to be one for avoiding css generation. Is this something that should be solved in Alectryon itself or reported upstream? Or even by the user running Alectryon?

Distributing Alectryon as a PyPi package would make it easier to install. The steps are described here: https://packaging.python.org/tutorials/packaging-projects/

First of all, thanks for the awesome tool!

I have an HTML version of a Coq document lecture01.html and also alectryon.js and alectryon.css in the same directory but when GitHub Pages serves the page it seems that the interactivity and source code highlighting is lost (please see the rendered version here https://anton-trunov.github.io/csclub-coq-course-spring-2021/lectures/lecture01.html). It works locally, though.

Any idea how to fix it? Thanks in advance.

Alectryon seems to generate big files. I realized that when github.io
told me I could not transfer file > 100MB. This file is 228M while its equivalent in Proviola was only 18M
Is it possible to do something?

In our CI we're using Python 3.7.5. I recently attempted to bump our version of alectryon but immediately ran into a syntax error within this line. In particular, the use of the single-starred expression to create a variable length tuple is apparently not supported as it is currently written (i.e. return obj.conclusion, *obj.hypotheses).

I believe that if you change this line to return (obj.conclusion, *obj.hypotheses) then the code will continue working for the versions you test but it will also work with Python 3.7.5

I'd like to be able to process them in GH annotations, and this is tricky without knowing what file they come from

(* commentaire *)

(*|
    test
|*)

$ python alectryon.py test.v --frontend="coq+rst" --backend="webpage"
!! Coq raised an exception:
       Syntax error: illegal begin of vernac.
   Results past this point may be unreliable.
   The offending chunk is delimited by >>>.<<< below:
       (* commentaire *)

        >>>test<<<

This error doesn't occur if there is no comment before, or if we remove the indentation in the "rst comment".

I get examples/tutorial_coq_elpi_command.v:77: (ERROR/3) ... but it still exists with 0, so I can't easily detect in a makefile if the doc contains errors.

Is there a way? I could not find a flag for controlling this.