Rename coq -> rocq

lib/rouge/lexers/coq.rb → lib/rouge/lexers/rocq.rb

@@ -3,11 +3,15 @@
 
 module Rouge
   module Lexers
-    class Coq < RegexLexer
-      title "Coq"
-      desc 'Coq (coq.inria.fr)'
-      tag 'coq'
-      mimetypes 'text/x-coq'
+    class Rocq < RegexLexer
+      title "Rocq"
+      desc 'The Rocq Prover (rocq-prover.org)'
+      tag 'rocq'
+
+      # Coq was renamed to Rocq
+      # https://github.com/rocq-prover/rfcs/blob/coq-roadmap/text/069-coq-roadmap.md#change-of-name-coq---the-rocq-prover
+      aliases 'coq'
+      mimetypes 'text/x-coq', 'text/x-rocq'
 
       def self.gallina
         @gallina ||= Set.new %w(
@@ -176,6 +180,8 @@ def self.classify(x)
         rule %r(:=|=>|;|:>|:|::|_), Punctuation
         rule %r(->|/\\|\\/|;|:>|[⇒→↔⇔≔≡∀∃∧∨¬⊤⊥⊢⊨∈λ]), Operator
 
+        # [jneen] TODO: it is not ideal that we don't actually yield all of the
+        # consumed text here.
         rule id do |m|
           @name = m[0]
           @id_dotted = false
@@ -251,5 +257,8 @@ def self.classify(x)
         end
       end
     end
+
+    # legacy
+    Coq = Rocq
   end
 end

spec/lexers/coq_spec.rb → spec/lexers/rocq_spec.rb

@@ -1,14 +1,15 @@
 # -*- coding: utf-8 -*- #
 # frozen_string_literal: true
 
-describe Rouge::Lexers::Coq do
-  let(:subject) { Rouge::Lexers::Coq.new }
+describe Rouge::Lexers::Rocq do
+  let(:subject) { Rouge::Lexers::Rocq.new }
 
   describe 'guessing' do
     include Support::Guessing
 
     it 'guesses by mimetype' do
       assert_guess :mimetype => 'text/x-coq'
+      assert_guess :mimetype => 'text/x-rocq'
     end
   end
 end