vim misidentifies some Verilog files as Coq files

[altde]

vim misidentifies some Verilog files as Coq files

[altde]

Wait a second, but V uses the *.vsh or *.vv extension, so shouldn't matter here.

I know almost nothing about V, but the information I've seen indicates that V does use *.v files:

• comments in the code
• comments in the pull request (#12281) and issue (#12274) associated with the commit that added the *.v type detection (80406c2)
• A quick web search found a (the?) V language website with a link to some examples that have *.v source files.

[chrisbra]

Thanks, I think it is fine to commit your last version. We have to draw a line somewhere and if this really turns out to be a problem, we can discuss further enhancements later.

I didn't find your E-Mail in your github profile, so I cannot properly attribute credits (except for mentioning your name of course).

Thanks everybody!

[chrisbra]

Hm, this comes from here:

vim/runtime/autoload/dist/ft.vim

Lines 1182 to 1215 in 7d0abf2

	# Set the filetype of a *.v file to Verilog, V or Cog based on the first 200
	# lines.
	export def FTv()
	if did_filetype()
	# ":setf" will do nothing, bail out early
	return
	endif
	for line in getline(1, 200)
	if line[0] =~ '^\s*/'
	# skip comment line
	continue
	endif
	# Verilog: line ends with ';' followed by an optional variable number of
	# spaces and an optional start of a comment.
	# Example: " b <= a + 1; // Add 1".
	if line =~ ';\(\s*\)\?\(/.*\)\?$'
	setf verilog
	return
	endif
	# Coq: line ends with a '.' followed by an optional variable number of
	# spaces and an optional start of a comment.
	# Example: "Definition x := 10. (*".
	if line =~ '\.\(\s*\)\?\((\*.*\)\?$'
	setf coq
	return
	endif
	endfor
	# No line matched, fall back to "v".
	setf v
	enddef

Can you suggest an improvement?

[chrisbra]

perhaps this patch:

diff --git a/runtime/autoload/dist/ft.vim b/runtime/autoload/dist/ft.vim
index 53c56f6b5..eca5a670a 100644
--- a/runtime/autoload/dist/ft.vim
+++ b/runtime/autoload/dist/ft.vim
@@ -1188,7 +1188,7 @@ export def FTv()
   endif

   for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
+    if line =~ '^\s*[/*]'
       # skip comment line
       continue
     endif

[altde]

That works for my case, but only because I start each line of the block comment with "*" (which is just a readability convention, and not a required part of Verilog block comments).

(Incidentally, your removal of "[0]" is required to make the script skip Verilog comment lines. If I replace my whole block comment with // This Verilog file includes a line comment with a line ending with a period., the current version says it's a Coq file.)

I can think of a few possible solutions:

1. (super simple, and used for some other file-type determinations) If "/*" is found at the beginning of a line (after optional spaces), declare the filetype Verilog and return. This would work for my case, but it wouldn't work for the other file types (coq and v) if they can have lines like that. It also would miss legal Verilog if the block comment started at the end of a line (in my example the line module test could be moved to the beginning of the first line, changing the line /** to module test /**, and still be valid Verilog).

2. (also simple) Give Verilog priority by setting a flag (used to set the return code at the end) when a coq-like line is found, but returning immediately if a Verilog-like line is found.

3. (more complicated) Use a variable to skip the whole block, as in this patch:

diff --git a/../autoload/dist/ft.vim.bak b/../autoload/dist/ft.vim
index 70482fc..2710899 100644
--- a/../autoload/dist/ft.vim.bak
+++ b/../autoload/dist/ft.vim
@@ -1187,8 +1187,22 @@ export def FTv()
     return
   endif

+  var in_comment = 0
   for line in getline(1, 200)
-    if line[0] =~ '^\s*/*'
+    # Skip Verilog comments (lines and blocks).
+    if line =~ '^\s*/\*'
+      # start comment block
+      in_comment = 1
+    endif
+    if in_comment == 1
+      if line =~ '\*/'
+        # end comment block
+        in_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+    if line =~ '^\s*//'
       # skip comment line
       continue
     endif

This patch will usually work, but it is fairly crude:

• It ignores block comments that start later in a line. (Such a block comment is valid Verilog, but is relatively rare.)
• It ignores the whole "*/" line, even though there could be code after it. (This seems OK. It should still find an identifying feature on a later line.)
• It gets confused if a block comment starts on the same line as the end of the previous block comment. This would happen if my Verilog example had this second line: */ /*. (This is possible, though probably rare.)

None of these are perfect, so maybe one of the simpler ones is best (I only thought of them after I did the last one), if somebody with knowledge of the other formats can check it.

[altde]

A comment in the issue that led to this *.v file-identification function (#12274 (comment)) indicates that V also has /**/ and // comments, so option 1 in my previous comment will not work.

[chrisbra]

It seems Coq uses (* *) as comment marker, while Verilog uses /* or // so that should be feasible to decide whether it's Verilog or Coq. Perhaps like this?

diff --git a/runtime/autoload/dist/ft.vim b/runtime/autoload/dist/ft.vim
index 53c56f6b5..6d2c5a4f5 100644
--- a/runtime/autoload/dist/ft.vim
+++ b/runtime/autoload/dist/ft.vim
@@ -1188,9 +1188,14 @@ export def FTv()
   endif

   for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
-      # skip comment line
-      continue
+    if line =~ '^\s*/[/*]'
+      # Verilog comment
+      setf verilog
+      return
+    elseif line =~ '(\*'
+      # Coq comment
+      setf coq
+      return
     endif

[benknoble]

Having worked with both, that patch seems reasonable to me.

[altde]

V apparently also uses /* */ and // for comments (see the link in my previous comment), so I don't think the comment delimiters can be used. Besides that, files won't necessarily include comments (though, of course, they should).

Items 2 and 3 from my list also have a problem I hadn't thought of before: Coq's (* *) comments can presumably span multiple lines, in which case the check for a trailing ; could sometimes misidentify Coq as Verilog.

While trying various patches with my Verilog files, I found another case that causes problems. End-of-line comments ending with . will be identified as Coq. (This won't be a problem if the non-comment part of the line, or an earlier line, ends with ;, but that won't necessarily be the case.)

Here's an example Verilog file with examples of all the problem cases I've found:

/**
* @file       test.v
* @brief      Verilog test file
*
* This Verilog file includes a block comment with a line ending with a period.
*/
// This Verilog file includes a full-line comment ending with a period.

module test // This Verilog file includes an end-of-line comment ending with a period.
  (
    input an_input, // This is another end-of-line comment ending with a period.
    output an_output
  ); // This is an end-of-line comment to make detection a bit harder.

  assign an_output := an_input;/* end-of-line block comment */
end module;//Here's another end-of-line comment, this time without spaces.

Here's a version of my earlier patch that works for this example Verilog file (and all the Verilog files in the project I'm currently working on). I made it skip Coq comments as well as Verilog and V comments. It's not perfect, but should cover the vast majority of files. (I also tweaked a couple of the existing patterns: \s* matches 0 or more spaces, so a \? is not needed.)

diff --git a/../autoload/dist/ft.vim.bak b/../autoload/dist/ft.vim
index 53c56f6..90d0cdf 100644
--- a/../autoload/dist/ft.vim.bak
+++ b/../autoload/dist/ft.vim
@@ -1187,16 +1187,45 @@ export def FTv()
     return
   endif

+  var in_verilog_comment = 0
+  var in_coq_comment = 0
   for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
+    # Skip Verilog and V comments (lines and blocks).
+    if line =~ '^\s*/\*'
+      # start comment block
+      in_verilog_comment = 1
+    endif
+    if in_verilog_comment == 1
+      if line =~ '\*/'
+        # end comment block
+        in_verilog_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+    if line =~ '^\s*//'
       # skip comment line
       continue
     endif

+    # Skip Coq comment blocks.
+    if line =~ '^\s*(\*'
+      # start comment block
+      in_coq_comment = 1
+    endif
+    if in_coq_comment == 1
+      if line =~ '\*)'
+        # end comment block
+        in_coq_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+
     # Verilog: line ends with ';' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: " b <= a + 1; // Add 1".
-    if line =~ ';\(\s*\)\?\(/.*\)\?$'
+    if line =~ ';\s*\(/[/*].*\)\?$'
       setf verilog
       return
     endif
@@ -1204,7 +1233,11 @@ export def FTv()
     # Coq: line ends with a '.' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: "Definition x := 10. (*".
-    if line =~ '\.\(\s*\)\?\((\*.*\)\?$'
+    if line =~ '\.\s*\((\*.*\)\?$'
+      if line =~ '//'
+        # This line appears to have a Verilog or V comment.  Skip it.
+        continue
+      endif
       setf coq
       return
     endif

Here are some limitations of this patch that spring to mind. (I'm sure there are others.)

• It only skips multi-line block comments if they start at the beginning of a line, which should usually be the case, but doesn't have to be. Removing the ^\s* from both start-of-comment-block patterns would skip other block comments, but then it would skip the whole line (not just the comment) and would miss block comments that start on the same line as the end of the previous comment block. I'm not sure which way is better.
• According to Coq documentation, Coq comments can be nested. This patch does not handle that correctly. (Verilog comments cannot be nested.)

[dkearns]

This should also utilise the filetype overrule mechanism. See :help filetype-overrule and other detection functions in ft.vim for details.

[chrisbra]

V apparently also uses /* */ and // for comments (see the link in my previous comment),

Wait a second, but V uses the *.vsh or *.vv extension, so shouldn't matter here.

[altde]

Here's a new version of my patch, adding the filetype overrule mechanism recommended by @dkearns. (I haven't looked for the help file, but presumably that would need to be updated to match.)

diff --git a/ft.vim.bak b/ft.vim
index 53c56f6..5c7e516 100644
--- a/ft.vim.bak
+++ b/ft.vim
@@ -1186,17 +1186,50 @@ export def FTv()
     # ":setf" will do nothing, bail out early
     return
   endif
+  if exists("g:filetype_v")
+    exe "setf " .. g:filetype_v
+    return
+  endif

+  var in_verilog_comment = 0
+  var in_coq_comment = 0
   for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
+    # Skip Verilog and V comments (lines and blocks).
+    if line =~ '^\s*/\*'
+      # start comment block
+      in_verilog_comment = 1
+    endif
+    if in_verilog_comment == 1
+      if line =~ '\*/'
+        # end comment block
+        in_verilog_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+    if line =~ '^\s*//'
       # skip comment line
       continue
     endif

+    # Skip Coq comment blocks.
+    if line =~ '^\s*(\*'
+      # start comment block
+      in_coq_comment = 1
+    endif
+    if in_coq_comment == 1
+      if line =~ '\*)'
+        # end comment block
+        in_coq_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+
     # Verilog: line ends with ';' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: " b <= a + 1; // Add 1".
-    if line =~ ';\(\s*\)\?\(/.*\)\?$'
+    if line =~ ';\s*\(/[/*].*\)\?$'
       setf verilog
       return
     endif
@@ -1204,7 +1237,11 @@ export def FTv()
     # Coq: line ends with a '.' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: "Definition x := 10. (*".
-    if line =~ '\.\(\s*\)\?\((\*.*\)\?$'
+    if line =~ '\.\s*\((\*.*\)\?$'
+      if line =~ '//'
+        # This line appears to have a Verilog or V comment.  Skip it.
+        continue
+      endif
       setf coq
       return
     endif

[dkearns]

V apparently also uses /* */ and // for comments (see the link in my previous comment),

Wait a second, but V uses the *.vsh or *.vv extension, so shouldn't matter here.

All three appear to be used and their own VS code extension supports all three: https://github.com/vlang/vscode-vlang

[dkearns]

Here's a new version of my patch, adding the filetype overrule mechanism recommended by @dkearns. (I haven't looked for the help file, but presumably that would need to be updated to match.)

Yes, please.

vim/runtime/doc/filetype.txt

Lines 135 to 177 in 74512e0

	*filetype-overrule*
	When the same extension is used for multiple filetypes, Vim tries to guess
	what kind of file it is. This doesn't always work. A number of global
	variables can be used to overrule the filetype used for certain extensions:
	file name variable ~
	*.asa g:filetype_asa |ft-aspperl-syntax|
	|ft-aspvbs-syntax|
	*.asm g:asmsyntax |ft-asm-syntax|
	*.asp g:filetype_asp |ft-aspperl-syntax|
	|ft-aspvbs-syntax|
	*.bas g:filetype_bas |ft-basic-syntax|
	*.cfg g:filetype_cfg
	*.cls g:filetype_cls
	*.csh g:filetype_csh |ft-csh-syntax|
	*.dat g:filetype_dat
	*.f g:filetype_f |ft-forth-syntax|
	*.frm g:filetype_frm |ft-form-syntax|
	*.fs g:filetype_fs |ft-forth-syntax|
	*.h g:c_syntax_for_h |ft-c-syntax|
	*.i g:filetype_i |ft-progress-syntax|
	*.inc g:filetype_inc
	*.lsl g:filetype_lsl
	*.m g:filetype_m |ft-mathematica-syntax|
	*.mod g:filetype_mod
	*.p g:filetype_p |ft-pascal-syntax|
	*.pl g:filetype_pl
	*.pp g:filetype_pp |ft-pascal-syntax|
	*.prg g:filetype_prg
	*.r g:filetype_r
	*.sig g:filetype_sig
	*.sql g:filetype_sql |ft-sql-syntax|
	*.src g:filetype_src
	*.sys g:filetype_sys
	*.sh g:bash_is_sh |ft-sh-syntax|
	*.tex g:tex_flavor |ft-tex-plugin|
	*.typ g:filetype_typ
	*.w g:filetype_w |ft-cweb-syntax|
	For a few filetypes the global variable is used only when the filetype could
	not be detected:
	*.r g:filetype_r |ft-rexx-syntax|

[dkearns]

+  var in_verilog_comment = 0
+  var in_coq_comment = 0
   for line in getline(1, 200)
-    if line[0] =~ '^\s*/'

Is slurping 200 lines significantly worse than iterating over a range like most of the other detection functions?

[altde]

Yes, please.

Here's a patch for that filetype.txt. (I assume this one line is all that's needed?)

diff --git a/filetype.txt.bak b/filetype.txt
index e35ffb8..97c1ab2 100644
--- a/filetype.txt.bak
+++ b/filetype.txt
@@ -169,6 +169,7 @@ variables can be used to overrule the filetype used for certain extensions:
        *.sh            g:bash_is_sh            |ft-sh-syntax|
        *.tex           g:tex_flavor            |ft-tex-plugin|
        *.typ           g:filetype_typ
+       *.v             g:filetype_v
        *.w             g:filetype_w            |ft-cweb-syntax|

 For a few filetypes the global variable is used only when the filetype could

[altde]

Is slurping 200 lines significantly worse than iterating over a range like most of the other detection functions?

I suppose it depends on how many lines are really needed, which could be quite high in a Verilog file that starts with a large header and a module with many ports (the first ; in such a file is generally at the end of the port list). I don't notice a difference in the time it takes to open my files, but I like the idea of not reading extra lines.

From my last attempt, the change is this:

diff --git a/autoload/dist/ft.vim.checkpoint3 b/autoload/dist/ft.vim
index 5c7e516..5875d58 100644
--- a/autoload/dist/ft.vim.checkpoint3
+++ b/autoload/dist/ft.vim
@@ -1193,7 +1193,8 @@ export def FTv()

   var in_verilog_comment = 0
   var in_coq_comment = 0
-  for line in getline(1, 200)
+  for lnum in range(1, min([line("$"), 200]))
+    var line = getline(lnum)
     # Skip Verilog and V comments (lines and blocks).
     if line =~ '^\s*/\*'
       # start comment block

Here's the full patch:

diff --git a/autoload/dist/ft.vim.bak b/autoload/dist/ft.vim
index 53c56f6..5875d58 100644
--- a/autoload/dist/ft.vim.bak
+++ b/autoload/dist/ft.vim
@@ -1186,17 +1186,51 @@ export def FTv()
     # ":setf" will do nothing, bail out early
     return
   endif
+  if exists("g:filetype_v")
+    exe "setf " .. g:filetype_v
+    return
+  endif

-  for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
+  var in_verilog_comment = 0
+  var in_coq_comment = 0
+  for lnum in range(1, min([line("$"), 200]))
+    var line = getline(lnum)
+    # Skip Verilog and V comments (lines and blocks).
+    if line =~ '^\s*/\*'
+      # start comment block
+      in_verilog_comment = 1
+    endif
+    if in_verilog_comment == 1
+      if line =~ '\*/'
+        # end comment block
+        in_verilog_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+    if line =~ '^\s*//'
       # skip comment line
       continue
     endif

+    # Skip Coq comment blocks.
+    if line =~ '^\s*(\*'
+      # start comment block
+      in_coq_comment = 1
+    endif
+    if in_coq_comment == 1
+      if line =~ '\*)'
+        # end comment block
+        in_coq_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+
     # Verilog: line ends with ';' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: " b <= a + 1; // Add 1".
-    if line =~ ';\(\s*\)\?\(/.*\)\?$'
+    if line =~ ';\s*\(/[/*].*\)\?$'
       setf verilog
       return
     endif
@@ -1204,7 +1238,11 @@ export def FTv()
     # Coq: line ends with a '.' followed by an optional variable number of
     # spaces and an optional start of a comment.
     # Example: "Definition x := 10. (*".
-    if line =~ '\.\(\s*\)\?\((\*.*\)\?$'
+    if line =~ '\.\s*\((\*.*\)\?$'
+      if line =~ '//'
+        # This line appears to have a Verilog or V comment.  Skip it.
+        continue
+      endif
       setf coq
       return
     endif

[chrisbra]

+    # Skip Coq comment blocks.
+    if line =~ '^\s*(\*'
+      # start comment block
+      in_coq_comment = 1

I suppose we know here already, that this is a coq file, so we can simply use:

# Coq comment blocks.
 if line =~ '^\s*(\*'
       setf coq
       return

[benknoble]

For the record, it's possible to end a Coq line with ;, too, though I would expect that to occur only after the first .-ended line. Though this is valid if ugly syntax:

Theorem foo: forall a, a -> a. Proof. intros;
auto. Qed.

[altde]

I suppose we know here already, that this is a coq file, so we can simply use:

Good point. In fact, I think this can be combined with the Coq-detection block, to make it detect either an end-of-line . or a comment (rather than a . followed by an optional comment). In addition, the check to exclude Verilog and V comments can be combined with the main Coq condition (and made to consider the order of the delimiters):

    # Coq: line ends with a '.' followed by an optional variable number of
    # spaces or contains the start of a comment, but not inside a Verilog or V
    # comment.
    # Example: "Definition x := 10. (*".
    if (line =~ '\.\s*$' && line !~ '/[/*]') || (line =~ '(\*' && line !~ '/[/*].*(\*')
      setf coq
      return
    endif

To make sure a semicolon in a Coq comment can't cause a file to be identified as Verilog, the Coq check should now come first. Here's the whole patch with that change:

diff --git a/autoload/dist/ft.vim.bak b/autoload/dist/ft.vim
index 53c56f6..2423fd4 100644
--- a/autoload/dist/ft.vim.bak
+++ b/autoload/dist/ft.vim
@@ -1186,26 +1186,46 @@ export def FTv()
     # ":setf" will do nothing, bail out early
     return
   endif
+  if exists("g:filetype_v")
+    exe "setf " .. g:filetype_v
+    return
+  endif

-  for line in getline(1, 200)
-    if line[0] =~ '^\s*/'
+  var in_comment = 0
+  for lnum in range(1, min([line("$"), 200]))
+    var line = getline(lnum)
+    # Skip Verilog and V comments (lines and blocks).
+    if line =~ '^\s*/\*'
+      # start comment block
+      in_comment = 1
+    endif
+    if in_comment == 1
+      if line =~ '\*/'
+        # end comment block
+        in_comment = 0
+      endif
+      # skip comment-block line
+      continue
+    endif
+    if line =~ '^\s*//'
       # skip comment line
       continue
     endif

-    # Verilog: line ends with ';' followed by an optional variable number of
-    # spaces and an optional start of a comment.
-    # Example: " b <= a + 1; // Add 1".
-    if line =~ ';\(\s*\)\?\(/.*\)\?$'
-      setf verilog
+    # Coq: line ends with a '.' followed by an optional variable number of
+    # spaces or contains the start of a comment, but not inside a Verilog or V
+    # comment.
+    # Example: "Definition x := 10. (*".
+    if (line =~ '\.\s*$' && line !~ '/[/*]') || (line =~ '(\*' && line !~ '/[/*].*(\*')
+      setf coq
       return
     endif

-    # Coq: line ends with a '.' followed by an optional variable number of
+    # Verilog: line ends with ';' followed by an optional variable number of
     # spaces and an optional start of a comment.
-    # Example: "Definition x := 10. (*".
-    if line =~ '\.\(\s*\)\?\((\*.*\)\?$'
-      setf coq
+    # Example: " b <= a + 1; // Add 1".
+    if line =~ ';\s*\(/[/*].*\)\?$'
+      setf verilog
       return
     endif
   endfor

[altde]

For the record, it's possible to end a Coq line with ;, too, though I would expect that to occur only after the first .-ended line. Though this is valid if ugly syntax:

Theorem foo: forall a, a -> a. Proof. intros;
auto. Qed.

That looks like a hard one to detect. :, ,, .,and -> can all occur in Verilog, so I can't think of a simple pattern to distinguish that from Verilog.

Is it reasonable to ignore that case? Some wiggle room is provided by the caveat in :help filetype-overrule: "... Vim tries to guess what kind of file it is. This doesn't always work." For users who have code like that, the help file gives some ways to override the automatic detection, though they may not be suitable for a casual user.