Open jhaag opened 3 years ago
Am I using this file in the wrong way or has this functionality fallen somewhat out of date?
This is an issue with relative imports: it will happen if alectryon/alectryon/
is in your PYTHONPATH (sys.path
). That causes Alectryon's json
and docutils
modules to shadow the system ones.
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?
Not too hard, and you can still get a bit of functionality by usign coqc -time
, which splits the document into sentences. Can you try the gh-60-coqc
branch and the recipes in recipes/
?
Clement,
Thanks for your quick replies regarding my issue/feature request. Unfortunately I was ill last week which has thrown a wrench in some of my other work-plans for August; I don't think that I will have a chance to test this until later this week (or next week). With that being said, I will be sure to respond as soon as I get my hands on that branch!
~Jasper
No worries at all. Hope you got better!
Thanks for the well wishes; I am indeed feeling better now.
I spent some time today trying to get things working but I've continued to run into problems. In particular, before I was able to test out your branch I wanted to ensure that I had the most up-to-date version of Alectryon, so I switched from v1.0-28-g0216b93 <0216b934fb7a0f2e68f3eee048a92ef6dde8cd2e>
- which was fixed as a submodule - to master
. However, upon doing so I immediately noticed that a warning which used to be ignored silently was now treated as an error:
Warning, treated as error:
/home/jhaag/dev/bedrock/fm-docs/sphinx/a_first_specification.rst:35:Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/hw_models/theories
> [cannot-open-path,filesystem]
make[1]: *** [Makefile:112: refman-private-html] Error 2
The first half of the path (/home/jhaag/.opam/4.07.1+flambda/lib/coq/
) is passed via the COQLIB
environment variable when we invoke sphinx-build
, and the second half is the path for one of our internal libraries; our internal library paths are included via a COQPATH
command line variable, and my sphinx/conf.py
parses them out and manually updates SERTOP_ARGS
with the necessary -Q
and -I
options.
I've noticed this warning in the past but I could never trace it down (and I didn't get around to opening a bug report). However, this is now becoming a blocker for me w.r.t testing out your other changes. Do you know why/where we prepend the COQLIB
to the -Q
arguments that are provided to sertop
?
Wild guess: could it be https://github.com/ejgallego/coq-serapi/pull/249 ?
In the meantime, you could turn off the sphinx feature that treats warnings as errors (remove SPHINXOPTS="-W"
from your makefile)
That does look related; we'll probably wait a bit to bump serapi, but removing that SPHINXOPTS
option should be sufficient. However, I'm a bit surprised that these warnings were not previously treated as errors given that I've had this option enabled since before I attempted to bump the Alectryon version that we're using.
However, I'm a bit surprised that these warnings were not previously treated as errors given that I've had this option enabled since before I attempted to bump the Alectryon version that we're using.
It's expected: errors and warnings produced by Alectryon were not integrated into Docutils and Sphinx' error-reporting system until very recently (https://github.com/cpitclaudel/alectryon/issues/57)
Clément,
After removing the -W
option from my Makefile, I was able to successfully try out your gh-60-coqc
branch. In particular, I found that adding the following to my sphinx/conf.py
- and building using ALECTRYON_DRIVER=SERTOP_NOEXEC make
- was sufficient to build the documentation without resulting in any of output being printed:
# NOTE: Clément resolved the sphinx docinfo issue, but we still need to grab the
# paths for bedrock to feed to SerAPI, so we're still using this.
#
# Clément notes that this is deprecated; what can we do instead?
alectryon.docutils.AlectryonTransform.SERTOP_ARGS = sertop_args
if 'ALECTRYON_DRIVER' in os.environ:
if os.environ.get('ALECTRYON_DRIVER') == 'SERTOP_NOEXEC':
alectryon.docutils.AlectryonTransform.LANGUAGE_DRIVERS = {"coq": "sertop_noexec"}
alectryon.docutils.AlectryonTransform.DRIVER_ARGS["sertop_noexec"] = list(sertop_args)
elif os.environ.get('ALECTRYON_DRIVER') == 'COQC_TIME':
alectryon.docutils.AlectryonTransform.LANGUAGE_DRIVERS = {"coq": "coqc_time"}
else:
raise ValueError('')
Unfortunately, when I try to use coqc_time
I get the following error message (stack-trace included):
Exception occurred while building, starting debugger:
Traceback (most recent call last):
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/cmd/build.py", line 280, in build_main
app.build(args.force_all, filenames)
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/application.py", line 352, in build
self.builder.build_update()
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/builders/__init__.py", line 296, in build_update
self.build(to_build,
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/builders/__init__.py", line 310, in build
updated_docnames = set(self.read())
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/builders/__init__.py", line 417, in read
self._read_serial(docnames)
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/builders/__init__.py", line 438, in _read_serial
self.read_doc(docname)
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/builders/__init__.py", line 478, in read_doc
doctree = read_doc(self.app, self.env, self.env.doc2path(docname))
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/io.py", line 221, in read_doc
pub.publish()
File "/home/jhaag/.local/lib/python3.8/site-packages/docutils/core.py", line 219, in publish
self.apply_transforms()
File "/home/jhaag/.local/lib/python3.8/site-packages/docutils/core.py", line 200, in apply_transforms
self.document.transformer.apply_transforms()
File "/home/jhaag/.local/lib/python3.8/site-packages/sphinx/transforms/__init__.py", line 86, in apply_transforms
super().apply_transforms()
File "/home/jhaag/.local/lib/python3.8/site-packages/docutils/transforms/__init__.py", line 171, in apply_transforms
transform.apply(**kwargs)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 301, in apply
self._apply()
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 421, in _apply
self.apply_coq()
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 389, in apply_coq
generator, annotated = self.annotate(pending_nodes)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 375, in annotate
return self.annotate_cached(chunks, driver_cls, driver_args)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/docutils.py", line 368, in annotate_cached
annotated = cache.update(chunks, driver)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/json.py", line 329, in update
annotated = super().update(*args, **kwargs)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/json.py", line 230, in update
annotated = driver.annotate(chunks)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/coqc_time.py", line 86, in annotate
return list(document.recover_chunks(fragments))
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/core.py", line 295, in strip_separators
for fragments in grouped:
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/core.py", line 269, in _recover_chunks
fragments = deque(positioned_fragments)
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/core.py", line 240, in intersperse_text_fragments
for st in positioned_sentences:
File "/home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/coqc_time.py", line 71, in _find_sentences
raise ValueError(MSG.format(coqc.returncode, stderr))
ValueError: coqc exited with code 1:
Error:
Can't find file /tmp/alectryon_coq-time8jue5zr3/a_first_specification.rst.v
> /home/jhaag/dev/bedrock/fm-docs/alectryon/alectryon/coqc_time.py(71)_find_sentences()
-> raise ValueError(MSG.format(coqc.returncode, stderr))
Do you have any ideas why this error might be occurring? Fwiw, I use the normal alectryon.py
script to tangle my .v
files into .rst
files before sphinx
is invoked, and sphinx then uses alectryon
as a plugin.
A few other related items:
gh-60-coqc
branch?sphinx/conf.py
file above?AlectryonTransform.SERTOP_ARGS
is deprecated; what is the new solution for pre-charging serapi with the appropriate custom-library paths from within the sphinx/conf.py
file?sertop_noexec
will work in an environment that lacks a serapi executable? I'm planning to test this locally later today while I bump our documentation docker image, but I figured that you'd know the answer :~)
sertop_noexec
driver, so maybe serapi still is being invoked:
...
...
...
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_classes/simple_classes_cpp_spec.rst:699: WARNING: Orphaned message for sid b'48':
> manhattan_distance =
> λ p1 p2 : Point,
> (Z.abs_N (_x p1 - _x p2) + Z.abs_N (_y p1 - _y p2))%N
> : Point → Point → N
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_classes/simple_classes_cpp_spec.rst:437: WARNING: Coq raised an exception:
> (in proof Point_interface_sound): Attempt to save an incomplete proof
The offending chunk is delimited by >>>…<<< below:
> >>>End with_Σ.<<<
Results past this point may be unreliable.
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_classes/simple_classes_cpp_spec.rst:437: WARNING: Orphaned message for sid b'110':
> Tactic open_any_fwd is deprecated since 2021-05-29.
> use work to unfold [deprecated-tactic,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_classes/simple_classes_cpp_spec.rst:437: WARNING: Orphaned message for sid b'178':
> (in proof Point_interface_sound): Attempt to save an incomplete proof
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:3: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/hw_models/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:3: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/cpp2v/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:3: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/cpp2v-core/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:3: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/fm-docs/src
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'16':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'16':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'16':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'16':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'17':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'17':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'17':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'17':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'19':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'19':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'19':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'19':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'21':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'21':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'21':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'21':
> Notation _eq is deprecated since 2020-12-07.
> no longer needed
> [deprecated-syntactic-definition,deprecated]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/simple_linked_list/simple_linked_list_hpp_spec_exercises.rst:294: WARNING: Orphaned message for sid b'30':
> Not a truly recursive fixpoint.
> [non-recursive,fixpoints]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/warmup/warmup_cpp_spec.rst:112: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/hw_models/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/warmup/warmup_cpp_spec.rst:112: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/cpp2v/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/warmup/warmup_cpp_spec.rst:112: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/bhv/fmdeps/cpp2v-core/theories
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/warmup/warmup_cpp_spec.rst:112: WARNING: Orphaned message for sid b'0':
> Cannot open /home/jhaag/.opam/4.07.1+flambda/lib/coq//home/jhaag/dev/bedrock/fm-docs/src
> [cannot-open-path,filesystem]
/home/jhaag/dev/bedrock/fm-docs/sphinx/tangles/warmup/warmup_cpp_spec.rst:57: WARNING: Orphaned message for sid b'23':
> Tactic simplifying is deprecated since 2021-03-18.
> workv3 now hints the reduction behavior of `simplifying`.
> [deprecated-tactic,deprecated]
Do you have any ideas why this error might be occurring?
I will double-check.
Fwiw, I use the normal alectryon.py script to tangle my .v files into .rst files before sphinx is invoked, and sphinx then uses alectryon as a plugin.
Ah! You don't need to do that; you can just drop .v
file your sphinx folders and they will be translated and compiled as part of the sphinx build.
When might you expect the alternative driver options to get merged and tagged? In the meantime, shall I continue to use the gh-60-coqc branch?
Soon ^^ I was waiting for feedback from @gmalecha since part of this patch was for his use case, but I'm ready to move ahead.
Would it be possible for you to upstream the logic that I added to my sphinx/conf.py file above?
I'm wary of adding yet another configuration mechanism. But fortunately we can simplify things a bit. Would the following work, in your sphinx config?
alectryon.docutils.AlectryonTransform.DRIVER_ARGS["sertop"] = sertop_args
alectryon.docutils.AlectryonTransform.DRIVER_ARGS["sertop_noexec"] = sertop_args
alectryon.docutils.AlectryonTransform.LANGUAGE_DRIVERS["coq"] = os.environ.get('ALECTRYON_DRIVER', 'sertop')
I noticed that AlectryonTransform.SERTOP_ARGS is deprecated; what is the new solution for pre-charging serapi with the appropriate custom-library paths from within the sphinx/conf.py file?
You already have the fix, it's DRIVER_ARGS['sertop']
Do you expect that sertop_noexec will work in an environment that lacks a serapi executable?
Definitely not. sertop_noexec
is Serapi, it just doesn't execute the proofs. It's basically the patch that @gmalecha had proposed.
I will double-check.
Found and fixed, thanks.
I have merged the gh-60 branch, with an updated changelog.
Thanks for your thoughtful response to my (long) message and for merging gh-60
! I will incorporate your suggestions - switching to the (hopefully-)now-working coqc_time
driver - later this week, or potentially next week. If you don't mind I'd propose that we leave this issue open until I have the time to actually deploy this solution.
Yep. But beware: the coqc -time
driver is just a stopgap for compiling documents when SerAPI isn't working: it doesn't capture goals, it only segments the document into sentences and checks them for correctness.
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 replacealectryon/alectryon.py
withalectryon/alectryon/minimal.py
in mySphinx
conf.py
file (edit: I changed which pyhon script I invoke forAlectryon
within myMakefile
), I end up with the following error: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 toserapi
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 withserapi
; 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).