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

`sertop` ignores `COQPATH` #1

Closed jhaag closed 3 years ago

jhaag commented 4 years ago

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.

cpitclaudel commented 4 years ago

Great point, I've opened an issue in the serapi repo (https://github.com/ejgallego/coq-serapi/issues/221)

cpitclaudel commented 3 years ago

Fixed upstream.