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

Part of GH-60 (`coqc` adds a `.v` suffix to its input if it doesn't have one). Reported-by: @jhaag
cpitclaudel · Sep 4, 2021 · 467ca7a · 467ca7a
1 parent 9c5cdb9
commit 467ca7a
Show file tree

Hide file tree

Showing 5 changed files with 71 additions and 5 deletions.
diff --git 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
@@ -0,0 +1,37 @@
+<?xml version="1.0" encoding="utf-8" ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
+<title>Errors from coqc -time</title>
+<link rel="stylesheet" href="alectryon.css" type="text/css" />
+<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
+<link rel="stylesheet" href="pygments.css" type="text/css" />
+<script type="text/javascript" src="alectryon.js"></script>
+<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
+<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
+<meta name="viewport" content="width=device-width, initial-scale=1">
+</head>
+<body>
+<div class="alectryon-root alectryon-centered"><div class="alectryon-banner">Built with <a href="https://github.com/cpitclaudel/alectryon/">Alectryon</a>, running Coq+coqc-time. Bubbles (<span class="alectryon-bubble"></span>) indicate interactive fragments: hover for details, tap to reveal contents. Use <kbd>Ctrl+↑</kbd> <kbd>Ctrl+↓</kbd> to navigate, <kbd>Ctrl+🖱️</kbd> to focus. On Mac, use <kbd>⌘</kbd> instead of <kbd>Ctrl</kbd>.</div><div class="document" id="errors-from-coqc-time">
+<h1 class="title">Errors from coqc -time</h1>
+
+<p>An incomplete file is an error with <tt class="docutils literal">coqc <span class="pre">-time</span></tt>.
+To compile:</p>
+<pre class="literal-block">
+alectryon --coq-driver=coqc_time coqc_time_error.rst &gt; coqc_time_error.out 2&gt;&amp;1; \
+  echo &quot;exit: $?&quot; &gt;&gt; coqc_time_error.out
+    # ReST → HTML; produces ‘coqc_time_error.out’
+</pre>
+<pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-wsp"><span class="kn">Goal</span> <span class="kt">True</span>.</span></pre><div class="system-messages section">
+<h1>Docutils System Messages</h1>
+<div class="system-message">
+<p class="system-message-title">System Message: ERROR/3 (<tt class="docutils">tests/coqc_time_error.rst</tt>, line 14)</p>
+coqc exited with code 1:
+   Error: There are pending proofs: Unnamed_thm.
+</div>
+</div>
+</div>
+</div></body>
+</html>
diff --git a/recipes/_output/tests/coqc_time_error.out 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
@@ -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
@@ -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.