Development

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.62",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "soda",

lakefile.lean

@@ -5,10 +5,10 @@ package «soda» where
   -- add package configuration options here
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries.git" @ "v4.21.0"
+  "https://github.com/leanprover-community/batteries.git" @ "v4.28.0"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.21.0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.28.0"
 
 @[default_target]
 lean_lib «Soda» where

lean-toolchain

@@ -1,2 +1,2 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.28.0
 

translator/src/main/resources/soda/translator/documentation/Soda.tmLanguage.json

@@ -0,0 +1,71 @@
+{
+  "scopeName": "source.soda",
+  "name": "Soda",
+  "fileTypes": ["soda"],
+  "patterns": [
+    { "include": "#comments" },
+    { "include": "#keywords" },
+    { "include": "#operators" },
+    { "include": "#literals" }
+  ],
+  "repository": {
+    "comments": {
+      "patterns": [
+        {
+          "name": "comment.block.soda",
+          "begin": "/\\*",
+          "end": "\\*/"
+        },
+        {
+          "name": "comment.line.soda",
+          "match": "//.*$"
+        }
+      ]
+    },
+    "keywords": {
+      "patterns": [
+        {
+          "name": "keyword.control.soda",
+          "match": "\\b(abstract|any|case|class|data|datatype|def|directive|else|end|extends|fun|if|import|inductive|lambda|match|package|subtype|supertype|then|this)\\b"
+        },
+        {
+          "name": "constant.language.soda",
+          "match": "\\b(true|false)\\b"
+        },
+        {
+          "name": "keyword.other.soda",
+          "match": "\\b(apply|by|cases|constructor|exact|forall|funext|have|induction|intro|notation|rewrite|rfl|rw|simp|theorem|with)\\b"
+        },
+        {
+          "name": "storage.modifier.annotation.soda",
+          "match": "@(new|override|tailrec)|\\bsorry\\b"
+        }
+      ]
+    },
+    "operators": {
+      "patterns": [
+        {
+          "name": "keyword.operator.soda",
+          "match": "(->|-->|:=|==>|=|:|%|\\*|\\+|-|/|<=|>=|<|>|==|and|or|not)"
+        }
+      ]
+    },
+    "literals": {
+      "patterns": [
+        {
+          "name": "constant.numeric.hex.soda",
+          "match": "0x[0-9A-Fa-f]+"
+        },
+        {
+          "name": "string.quoted.double.soda",
+          "begin": "\"",
+          "end": "\"",
+          "patterns": [
+            { "name": "constant.character.escape.soda", "match": "\\\\." }
+          ]
+        }
+      ]
+    }
+  }
+}
+

translator/src/main/resources/soda/translator/documentation/soda.lang

@@ -4,7 +4,7 @@
  This file is part of GtkSourceView
 
  Authors: Julian Alfredo Mendez
-   Copyright 2020-2024 Julian Alfredo Mendez <julian.mendez@gmail.com>
+   Copyright 2020-2025 Julian Alfredo Mendez <julian.mendez@gmail.com>
 
  GtkSourceView is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
@@ -135,6 +135,9 @@
             <keyword>extends</keyword>
             <keyword>abstract</keyword>
             <keyword>end</keyword>
+            <keyword>data</keyword>
+            <keyword>datatype</keyword>
+            <keyword>inductive</keyword>
             <keyword>this</keyword>
             <keyword>subtype</keyword>
             <keyword>supertype</keyword>
@@ -167,14 +170,17 @@
             <keyword>cases</keyword>
             <keyword>constructor</keyword>
             <keyword>exact</keyword>
+            <keyword>forall</keyword>
             <keyword>funext</keyword>
             <keyword>have</keyword>
             <keyword>induction</keyword>
             <keyword>intro</keyword>
+            <keyword>notation</keyword>
             <keyword>rewrite</keyword>
             <keyword>rfl</keyword>
             <keyword>rw</keyword>
             <keyword>simp</keyword>
+            <keyword>theorem</keyword>
             <keyword>with</keyword>
         </context>