shikijs · antfu · Aug 11, 2024 · Aug 9, 2024
diff --git a/packages/tm-grammars/NOTICE b/packages/tm-grammars/NOTICE
@@ -2047,6 +2047,32 @@ furnished to do so, subject to the following conditions:
 The above copyright notice and this permission notice shall be included in all
 copies or substantial portions of the Software.
 
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+=========================================================================================================
+Files:   coq.json
+License: https://raw.githubusercontent.com/coq-community/vscoq/main/LICENSE
+SPDX:    MIT
+---------------------------------------------------------------------------------------------------------
+MIT License
+
+Copyright (c) INRIA and contributors
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE

diff --git a/packages/tm-grammars/README.md b/packages/tm-grammars/README.md
@@ -51,6 +51,7 @@ import { grammars } from 'tm-grammars'
 | `codeql` | `ql` | [github/vscode-codeql](https://github.com/github/vscode-codeql/blob/47fa163cb9fffce379458962eb391c9ef9082dcb/syntaxes/ql.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/github/vscode-codeql/main/LICENSE.md) |  | 32.73 kB |
 | `coffee` | `coffeescript` | [microsoft/vscode](https://github.com/microsoft/vscode/blob/ff58f5083f57b50e6a100ab60454dfb72fe21e80/extensions/coffeescript/syntaxes/coffeescript.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/microsoft/vscode/main/LICENSE.txt) | `javascript` | 26.34 kB |
 | `common-lisp` | `lisp` | [qingpeng9802/vscode-common-lisp](https://github.com/qingpeng9802/vscode-common-lisp/blob/79d04dc9ca80d98e65c4f28b3d67a24a7829b18f/syntaxes/commonlisp.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/qingpeng9802/vscode-common-lisp/master/LICENSE) |  | 23.50 kB |
+| `coq` |  | [coq-community/vscoq](https://github.com/coq-community/vscoq/blob/ea0e57916a9c2c74397fbc68ef9392441f116bfe/client/syntax/coq.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/coq-community/vscoq/main/LICENSE) |  | 5.51 kB |
 | `cpp` | `c++` | [microsoft/vscode](https://github.com/microsoft/vscode/blob/6ac83c7c7dda9f27ca1fe9d98675253e010b75d1/extensions/cpp/syntaxes/cpp.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/microsoft/vscode/main/LICENSE.txt) | `cpp-macro` `regexp` `glsl` `sql` | 411.01 kB |
 | `crystal` |  | [crystal-lang-tools/vscode-crystal-lang](https://github.com/crystal-lang-tools/vscode-crystal-lang/blob/c920b0931ec5f05b78447dbff31b172c64f1d734/syntaxes/crystal.json) | [MIT](https://raw.githubusercontent.com/crystal-lang-tools/vscode-crystal-lang/master/LICENSE) | `html` `sql` `css` `c` `javascript` `shellscript` | 31.60 kB |
 | `csharp` | `c#` `cs` | [microsoft/vscode](https://github.com/microsoft/vscode/blob/ed4e6eda599f37bac9a11952403a6e63fd4f5a4d/extensions/csharp/syntaxes/csharp.tmLanguage.json) | [MIT](https://raw.githubusercontent.com/microsoft/vscode/main/LICENSE.txt) |  | 83.26 kB |

diff --git a/packages/tm-grammars/grammars/coq.json b/packages/tm-grammars/grammars/coq.json
@@ -0,0 +1,231 @@
+{
+  "displayName": "Coq",
+  "fileTypes": [
+    "v"
+  ],
+  "name": "coq",
+  "patterns": [
+    {
+      "comment": "Vernacular import keywords",
+      "match": "\\b(From|Require|Import|Export|Local|Global|Include)\\b",
+      "name": "keyword.control.import.coq"
+    },
+    {
+      "comment": "Vernacular scope keywords",
+      "match": "\\b((Open|Close|Delimit|Undelimit|Bind)\\s+Scope)\\b",
+      "name": "keyword.control.import.coq"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "2": {
+          "name": "entity.name.function.theorem.coq"
+        }
+      },
+      "comment": "Theorem declarations",
+      "match": "(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition|Goal)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "2": {
+          "name": "keyword.source.coq"
+        },
+        "3": {
+          "name": "entity.name.assumption.coq"
+        }
+      },
+      "comment": "Assumptions",
+      "match": "\\b(Parameters?|Axioms?|Conjectures?|Variables?|Hypothesis|Hypotheses)(\\s+Inline)?\\b\\s*\\(?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "3": {
+          "name": "entity.name.assumption.coq"
+        }
+      },
+      "comment": "Context",
+      "match": "\\b(Context)\\b\\s*`?\\s*(\\(|\\{)?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "2": {
+          "name": "keyword.source.coq"
+        },
+        "3": {
+          "name": "entity.name.function.coq"
+        }
+      },
+      "comment": "Definitions",
+      "match": "(\\b(?:Program|Local)\\s+)?\\b(Definition|Fixpoint|CoFixpoint|Function|Example|Let(?:\\s+Fixpoint|\\s+CoFixpoint)?|Instance|Equations|Equations?)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        }
+      },
+      "comment": "Obligations",
+      "match": "\\b((Show\\s+)?Obligation\\s+Tactic|Obligations\\s+of|Obligation|Next\\s+Obligation(\\s+of)?|Solve\\s+Obligations(\\s+of)?|Solve\\s+All\\s+Obligations|Admit\\s+Obligations(\\s+of)?|Instance)\\b"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "3": {
+          "name": "entity.name.type.coq"
+        }
+      },
+      "comment": "Type declarations",
+      "match": "(CoInductive|Inductive|Variant|Record|Structure|Class)\\s+(>\\s*)?((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "captures": {
+        "1": {
+          "name": "keyword.source.coq"
+        },
+        "2": {
+          "name": "entity.name.function.ltac"
+        }
+      },
+      "comment": "Ltac declarations",
+      "match": "(Ltac)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)"
+    },
+    {
+      "comment": "Vernacular keywords",
+      "match": "\\b(Hint|Constructors|Resolve|Rewrite|Ltac|Implicit(\\s+Types)?|Set|Unset|Remove\\s+Printing|Arguments|Tactic\\s+Notation|Notation|Infix|Reserved\\s+Notation|Section|Module\\s+Type|Module|End|Check|Print|Eval|Search|Universe|Coercions?|Generalizable\\s+All|Generalizable\\s+Variable?|Existing\\s+Instance|Existing\\s+Class|Canonical|About|Locate|Collection|Typeclasses\\s+(Opaque|Transparent))\\b",
+      "name": "keyword.source.coq"
+    },
+    {
+      "comment": "Proof keywords",
+      "match": "\\b(Proof|Qed|Defined|Save|Abort(\\s+All)?|Undo(\\s+To)?|Restart|Focus|Unfocus|Unfocused|Show\\s+Proof|Show\\s+Existentials|Show|Unshelve)\\b",
+      "name": "keyword.source.coq"
+    },
+    {
+      "comment": "Vernacular Debug keywords",
+      "match": "\\b(Quit|Drop|Time|Redirect|Timeout|Fail)\\b",
+      "name": "keyword.debug.coq"
+    },
+    {
+      "comment": "Admits are bad",
+      "match": "\\b(admit|Admitted)\\b",
+      "name": "invalid.illegal.admit.coq"
+    },
+    {
+      "comment": "Operators",
+      "match": ":|\\||=|<|>|\\*|\\+|-|\\{|\\}|≠|∨|∧|↔|¬|→|≤|≥",
+      "name": "keyword.operator.coq"
+    },
+    {
+      "comment": "Type keywords",
+      "match": "\\b(forall|exists|Type|Set|Prop|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\b|∀|∃",
+      "name": "support.type.coq"
+    },
+    {
+      "comment": "Ltac keywords",
+      "match": "\\b(try|repeat|rew|progress|fresh|solve|now|first|tryif|at|once|do|only)\\b",
+      "name": "keyword.control.ltac"
+    },
+    {
+      "comment": "Common Ltac connectors",
+      "match": "\\b(into|with|eqn|by|move|as|using)\\b",
+      "name": "keyword.control.ltac"
+    },
+    {
+      "comment": "Gallina keywords",
+      "match": "\\b(match|lazymatch|multimatch|fun|with|return|end|let|in|if|then|else|fix|for|where|and)\\b|λ",
+      "name": "keyword.control.gallina"
+    },
+    {
+      "comment": "Ltac builtins",
+      "match": "\\b(intro|intros|revert|induction|destruct|auto|eauto|tauto|eassumption|apply|eapply|assumption|constructor|econstructor|reflexivity|inversion|injection|assert|split|esplit|omega|fold|unfold|specialize|rewrite|erewrite|change|symmetry|refine|simpl|intuition|firstorder|generalize|idtac|exist|exists|eexists|elim|eelim|rename|subst|congruence|trivial|left|right|set|pose|discriminate|clear|clearbody|contradict|contradiction|exact|dependent|remember|case|easy|unshelve|pattern|transitivity|etransitivity|f_equal|exfalso|replace|abstract|cycle|swap|revgoals|shelve|unshelve)\\b",
+      "name": "support.function.builtin.ltac"
+    },
+    {
+      "applyEndPatternLast": 1,
+      "begin": "\\(\\*(?!#)",
+      "end": "\\*\\)",
+      "name": "comment.block.coq",
+      "patterns": [
+        {
+          "include": "#block_comment"
+        },
+        {
+          "include": "#block_double_quoted_string"
+        }
+      ]
+    },
+    {
+      "match": "\\b((0(x|X)[0-9a-fA-F]+)|([0-9]+(\\.[0-9]+)?))\\b",
+      "name": "constant.numeric.gallina"
+    },
+    {
+      "comment": "Gallina builtin constructors",
+      "match": "\\b(True|False|tt|false|true|Some|None|nil|cons|pair|inl|inr|O|S|Eq|Lt|Gt|id|ex|all|unique)\\b",
+      "name": "constant.language.constructor.gallina"
+    },
+    {
+      "match": "\\b_\\b",
+      "name": "constant.language.wildcard.coq"
+    },
+    {
+      "begin": "\"",
+      "beginCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.begin.coq"
+        }
+      },
+      "end": "\"",
+      "endCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.end.coq"
+        }
+      },
+      "name": "string.quoted.double.coq"
+    }
+  ],
+  "repository": {
+    "block_comment": {
+      "applyEndPatternLast": 1,
+      "begin": "\\(\\*(?!#)",
+      "end": "\\*\\)",
+      "name": "comment.block.coq",
+      "patterns": [
+        {
+          "include": "#block_comment"
+        },
+        {
+          "include": "#block_double_quoted_string"
+        }
+      ]
+    },
+    "block_double_quoted_string": {
+      "applyEndPatternLast": 1,
+      "begin": "\"",
+      "beginCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.begin.coq"
+        }
+      },
+      "end": "\"",
+      "endCaptures": {
+        "0": {
+          "name": "punctuation.definition.string.end.coq"
+        }
+      },
+      "name": "string.quoted.double.coq"
+    }
+  },
+  "scopeName": "source.coq"
+}
diff --git a/packages/tm-grammars/index.js b/packages/tm-grammars/index.js
@@ -506,6 +506,20 @@ export const grammars = [
     sha: '79d04dc9ca80d98e65c4f28b3d67a24a7829b18f',
     source: 'https://github.com/qingpeng9802/vscode-common-lisp/blob/79d04dc9ca80d98e65c4f28b3d67a24a7829b18f/syntaxes/commonlisp.tmLanguage.json',
   },
+  {
+    byteSize: 5642,
+    categories: [
+      'general',
+    ],
+    displayName: 'Coq',
+    lastUpdate: '2024-05-19T17:37:43Z',
+    license: 'MIT',
+    licenseUrl: 'https://raw.githubusercontent.com/coq-community/vscoq/main/LICENSE',
+    name: 'coq',
+    scopeName: 'source.coq',
+    sha: 'ea0e57916a9c2c74397fbc68ef9392441f116bfe',
+    source: 'https://github.com/coq-community/vscoq/blob/ea0e57916a9c2c74397fbc68ef9392441f116bfe/client/syntax/coq.tmLanguage.json',
+  },
   {
     aliases: [
       'c++',

diff --git a/samples/coq.sample b/samples/coq.sample
@@ -0,0 +1,36 @@
+From Coq Require Import ssreflect.
+
+(* ensure proofs are well-structured *)
+Set Default Goal Selector "!".
+#[global] Open Scope general_if_scope.
+
+Module list_playground.
+  (* Let's do a typical proof by induction: we'll define [list] as an inductive,
+     [app] (list append) as a recursive function, and prove that [app] is
+     associative. *)
+  Inductive list (A: Type) :=
+  | nil
+  | cons (x: A) (l: list A).
+
+  (* Fix up implicit arguments. *)
+  Arguments nil {A}.
+  Arguments cons {A} x l.
+  Notation "[]" := nil.
+  Infix "::" := cons.
+
+  Fixpoint app {A} (l1 l2: list A): list A :=
+    match l1 with
+    | [] => l2
+    | x :: l1 => x :: app l1 l2
+    end.
+
+  Infix "++" := app.
+
+  Theorem app_assoc {A} (l1 l2 l3: list A) :
+    (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
+  Proof.
+    induction l1 as [|x l1]; simpl.
+    - reflexivity.
+    - by rewrite IHl1.
+  Qed.
+End list_playground.
diff --git a/sources-grammars.ts b/sources-grammars.ts
@@ -30,6 +30,11 @@ export const sourcesVSCode: GrammarSource[] = [
     source: 'https://github.com/microsoft/vscode/blob/main/extensions/coffeescript/syntaxes/coffeescript.tmLanguage.json',
     categories: ['web', 'scripting', 'general'],
   },
+  {
+    name: 'coq',
+    source: 'https://github.com/coq-community/vscoq/blob/main/client/syntax/coq.tmLanguage.json',
+    categories: ['general'],
+  },
   {
     name: 'cpp',
     aliases: ['c++'],