Skip to content

Commit

Permalink
readme: Minor tweaks
Browse files Browse the repository at this point in the history
  • Loading branch information
cpitclaudel committed Jun 12, 2022
1 parent 032166f commit 7a3dd67
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 5 deletions.
8 changes: 4 additions & 4 deletions README.rst
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,7 @@
Alectryon
===========

A library to process Coq and Lean snippets embedded in text documents, showing goals and messages for each input sentence. Also a literate programming toolkit. The goal of Alectryon is to make it easy to write textbooks, blog posts, and other documents that mix interactive proofs and prose.

Alectryon originally supported Coq only. Both `Lean 4 <lean4_>`__ and `Lean 3 <lean3_>`__ are supported. `Lean 3 <lean3_>`__ support is preliminary.
A library to process Coq and Lean 4 snippets embedded in text documents, showing goals and messages for each input sentence. Also a literate programming toolkit. The goal of Alectryon is to make it easy to write textbooks, blog posts, and other documents that mix interactive proofs and prose.

.. image:: etc/screenshot.svg
:width: 100%
Expand Down Expand Up @@ -514,6 +512,8 @@ The reStructuredText directive for Lean 4 is ``.. lean4::``, for Markdown/MyST f
See `<recipes/plain-lean4.lean>`__, `<recipes/lean4-tactics.rst>`__, `<recipes/lean4-tactics-myst.md>`__ and `<recipes/literate-lean4.lean>`__ for examples.

Lean 4 support was contributed by Niklas Bülow (@insightmind).

.. _lean3:

Lean 3
Expand Down Expand Up @@ -553,7 +553,7 @@ The following features are missing:
Support for quoting snippets and displaying or hiding sentences is partial.

For a more detailed TODO list, see the header of `<alectryon/lean3.py>`__.

Polyglot documents
------------------

Expand Down
1 change: 1 addition & 0 deletions alectryon/cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -851,6 +851,7 @@ def build_parser():
TRACEBACK_HELP = "Print error traces."
debug.add_argument("--traceback", action="store_true",
default=False, help=TRACEBACK_HELP)

return parser

def parse_arguments():
Expand Down
4 changes: 3 additions & 1 deletion alectryon/core.py
Original file line number Diff line number Diff line change
Expand Up @@ -485,7 +485,9 @@ def run_cli(self, working_directory=None, capture_output=True, more_args=()):
cmd = [self.resolve_driver(self.binpath),
*self.CLI_ARGS, *self.user_args, *more_args]
self._debug_start(cmd)
p = subprocess.run(cmd, cwd=working_directory, capture_output=capture_output, check=False, encoding=self.CLI_ENCODING)
p = subprocess.run(cmd, cwd=working_directory,
capture_output=capture_output, check=False,
encoding=self.CLI_ENCODING)
if p.returncode != 0:
MSG = "Driver {} ({}) exited with code {}:\n{}"
raise ValueError(MSG.format(self.NAME, self.binpath, p.returncode,
Expand Down

0 comments on commit 7a3dd67

Please sign in to comment.