`alectryon.minimal` and a no-`coq-serapi` use-case #60

jhaag · 2021-08-16T18:14:21Z

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).

The text was updated successfully, but these errors were encountered:

cpitclaudel · 2021-08-19T19:23:02Z

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/?

cpitclaudel · 2021-08-19T19:23:22Z

https://github.com/cpitclaudel/alectryon/tree/gh-60-coqc

jhaag · 2021-08-23T12:13:14Z

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

cpitclaudel · 2021-08-23T14:15:05Z

No worries at all. Hope you got better!

jhaag · 2021-08-26T18:42:24Z

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?

cpitclaudel · 2021-08-28T22:27:23Z

Wild guess: could it be rocq-archive/coq-serapi#249 ?

In the meantime, you could turn off the sphinx feature that treats warnings as errors (remove SPHINXOPTS="-W" from your makefile)

jhaag · 2021-08-30T13:08:08Z

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.

cpitclaudel · 2021-08-30T13:27:16Z

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 (#57)

jhaag · 2021-09-02T16:36:53Z

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:

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?
Would it be possible for you to upstream the logic that I added to my sphinx/conf.py file above?
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?
Do you expect that 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 :~)
- edit: I receive the following warnings when running the 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]

cpitclaudel · 2021-09-03T18:21:55Z

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.

@jhaag

Part of GH-60 (`coqc` adds a `.v` suffix to its input if it doesn't have one). Reported-by: @jhaag

cpitclaudel · 2021-09-03T23:22:10Z

I will double-check.

Found and fixed, thanks.

@jhaag

Part of GH-60 (`coqc` adds a `.v` suffix to its input if it doesn't have one). Reported-by: @jhaag

cpitclaudel · 2021-09-04T16:58:56Z

I have merged the gh-60 branch, with an updated changelog.

jhaag · 2021-09-07T17:24:14Z

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.

cpitclaudel · 2021-09-07T18:15:18Z

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.

jhaag added bug kind: feature labels Aug 16, 2021

jhaag assigned cpitclaudel Aug 16, 2021

cpitclaudel removed the bug label Aug 19, 2021

cpitclaudel mentioned this issue Aug 19, 2021

Quick mode? #52

Closed

cpitclaudel added the status: implemented label Aug 24, 2021

cpitclaudel added a commit that referenced this issue Sep 3, 2021

coq: Ensure that the result of CoqIdents.topfile_of_path ends in ".v"

43ce4b3

Part of GH-60 (`coqc` adds a `.v` suffix to its input if it doesn't have one). Reported-by: @jhaag

cpitclaudel added a commit that referenced this issue Sep 4, 2021

coq: Ensure that the result of CoqIdents.topfile_of_path ends in ".v"

467ca7a

Part of GH-60 (`coqc` adds a `.v` suffix to its input if it doesn't have one). Reported-by: @jhaag

cpitclaudel added the status: pending label Sep 11, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`alectryon.minimal` and a no-`coq-serapi` use-case #60

`alectryon.minimal` and a no-`coq-serapi` use-case #60

jhaag commented Aug 16, 2021 •

edited

Loading

cpitclaudel commented Aug 19, 2021

cpitclaudel commented Aug 19, 2021

jhaag commented Aug 23, 2021

cpitclaudel commented Aug 23, 2021

jhaag commented Aug 26, 2021

cpitclaudel commented Aug 28, 2021

jhaag commented Aug 30, 2021

cpitclaudel commented Aug 30, 2021

jhaag commented Sep 2, 2021 •

edited by cpitclaudel

Loading

cpitclaudel commented Sep 3, 2021

cpitclaudel commented Sep 3, 2021

cpitclaudel commented Sep 4, 2021

jhaag commented Sep 7, 2021

cpitclaudel commented Sep 7, 2021 •

edited

Loading

alectryon.minimal and a no-coq-serapi use-case #60

alectryon.minimal and a no-coq-serapi use-case #60

Comments

jhaag commented Aug 16, 2021 • edited Loading

cpitclaudel commented Aug 19, 2021

cpitclaudel commented Aug 19, 2021

jhaag commented Aug 23, 2021

cpitclaudel commented Aug 23, 2021

jhaag commented Aug 26, 2021

cpitclaudel commented Aug 28, 2021

jhaag commented Aug 30, 2021

cpitclaudel commented Aug 30, 2021

jhaag commented Sep 2, 2021 • edited by cpitclaudel Loading

cpitclaudel commented Sep 3, 2021

cpitclaudel commented Sep 3, 2021

cpitclaudel commented Sep 4, 2021

jhaag commented Sep 7, 2021

cpitclaudel commented Sep 7, 2021 • edited Loading

`alectryon.minimal` and a no-`coq-serapi` use-case #60

`alectryon.minimal` and a no-`coq-serapi` use-case #60

jhaag commented Aug 16, 2021 •

edited

Loading

jhaag commented Sep 2, 2021 •

edited by cpitclaudel

Loading

cpitclaudel commented Sep 7, 2021 •

edited

Loading