diff --git a/alectryon/coq.py b/alectryon/coq.py index ed1a1ea7..e4b7cb83 100644 --- a/alectryon/coq.py +++ b/alectryon/coq.py @@ -20,6 +20,7 @@ import re import unicodedata +from pathlib import Path Pattern = type(re.compile("")) # LATER (3.7+): re.Pattern @@ -60,19 +61,24 @@ def valid_char(c, allowed): def sub_chars(cls, chars, allowed): return "".join(c if cls.valid_char(c, allowed) else "_" for c in chars) + SUFFIXES = re.compile(r"(?:[.](?:v|rst))+\Z") + @classmethod - def topfile_of_fpath(cls, fpath) -> str: + def topfile_of_fpath(cls, fpath: Path) -> str: """Normalize `fpath` to make its ``name`` a valid Coq identifier. - >>> from pathlib import Path >>> str(CoqIdents.topfile_of_fpath(Path("dir+ex/f:𝖴🄽𝓘ⓒ𝕆Ⓓ𝙴.v"))) 'f_𝖴_𝓘_𝕆_𝙴.v' + >>> str(CoqIdents.topfile_of_fpath(Path("/tmp/abc.def.v.rst"))) + 'abc_def.v' + >>> str(CoqIdents.topfile_of_fpath(Path("/tmp/abc.def.rst.v"))) + 'abc_def.v' >>> str(CoqIdents.topfile_of_fpath(Path("-"))) 'Top.v' """ - stem = fpath.stem - if stem in ("-", ""): + if fpath.name in ("-", ""): return "Top.v" + stem = cls.SUFFIXES.sub("", fpath.name) stem = (cls.sub_chars(stem[0], cls.COQ_IDENT_START) + cls.sub_chars(stem[1:], cls.COQ_IDENT_PART)) - return stem + fpath.suffix + return stem + ".v" diff --git a/recipes/_output/tests/coqc_time_error.html b/recipes/_output/tests/coqc_time_error.html new file mode 100644 index 00000000..5a5b694e --- /dev/null +++ b/recipes/_output/tests/coqc_time_error.html @@ -0,0 +1,37 @@ + + + + + + +Errors from coqc -time + + + + + + + + + +
Built with Alectryon, running Coq+coqc-time. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
+

Errors from coqc -time

+ +

An incomplete file is an error with coqc -time. +To compile:

+
+alectryon --coq-driver=coqc_time coqc_time_error.rst > coqc_time_error.out 2>&1; \
+  echo "exit: $?" >> coqc_time_error.out
+    # ReST → HTML; produces ‘coqc_time_error.out’
+
+
Goal True.
+

Docutils System Messages

+
+

System Message: ERROR/3 (tests/coqc_time_error.rst, line 14)

+coqc exited with code 1: + Error: There are pending proofs: Unnamed_thm. +
+
+
+
+ diff --git a/recipes/_output/tests/coqc_time_error.out b/recipes/_output/tests/coqc_time_error.out new file mode 100644 index 00000000..e06f1fcb --- /dev/null +++ b/recipes/_output/tests/coqc_time_error.out @@ -0,0 +1,4 @@ +tests/coqc_time_error.rst:14: (ERROR/3) coqc exited with code 1: + Error: There are pending proofs: Unnamed_thm. + +exit: 13 diff --git a/recipes/tests.mk b/recipes/tests.mk index e9ad9ff0..8dd303ad 100644 --- a/recipes/tests.mk +++ b/recipes/tests.mk @@ -32,6 +32,11 @@ _output/tests/cli_flags.txt: tests/cli_flags.rst $(alectryon) $< -o - >/dev/null --debug --traceback --expect-unexpected --long-line-threshold=-1 -I . -R ../recipes/ custom_flag_recipes -Q ../alectryon/ custom_flag_alectryon_tests; echo "exit: $$?" > $@ tests_targets += _output/tests/cli_flags.txt +# ReST → HTML +_output/tests/coqc_time_error.out: tests/coqc_time_error.rst + $(alectryon) --coq-driver=coqc_time $< > $@ 2>&1; echo "exit: $$?" >> $@ +tests_targets += _output/tests/coqc_time_error.out + # Coq → HTML _output/tests/corner_cases.html: tests/corner_cases.rst $(alectryon) --stdin-filename $< --frontend rst -o $@ - < $< diff --git a/recipes/tests/coqc_time_error.rst b/recipes/tests/coqc_time_error.rst new file mode 100644 index 00000000..23c61a32 --- /dev/null +++ b/recipes/tests/coqc_time_error.rst @@ -0,0 +1,14 @@ +======================== + Errors from coqc -time +======================== + +An incomplete file is an error with ``coqc -time``. +To compile:: + + alectryon --coq-driver=coqc_time coqc_time_error.rst > coqc_time_error.out 2>&1; \ + echo "exit: $?" >> coqc_time_error.out + # ReST → HTML; produces ‘coqc_time_error.out’ + +.. coq:: + + Goal True.