From d7bf5654137ba5bf44070389a7da7c239562e366 Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Sat, 23 Aug 2025 22:47:12 +0200 Subject: [PATCH 1/5] Update gedit configuration file --- .../resources/soda/translator/documentation/soda.lang | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/translator/src/main/resources/soda/translator/documentation/soda.lang b/translator/src/main/resources/soda/translator/documentation/soda.lang index d93ebba0..c792d1fa 100644 --- a/translator/src/main/resources/soda/translator/documentation/soda.lang +++ b/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 + Copyright 2020-2025 Julian Alfredo Mendez 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 @@ extends abstract end + data + datatype + inductive this subtype supertype @@ -167,14 +170,17 @@ cases constructor exact + forall funext have induction intro + notation rewrite rfl rw simp + theorem with From 0c6750867a768590c0c68077edc1a468a2235dbe Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Mon, 13 Oct 2025 14:22:09 +0200 Subject: [PATCH 2/5] Add Soda.tmLanguage.json --- .../documentation/Soda.tmLanguage.json | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 translator/src/main/resources/soda/translator/documentation/Soda.tmLanguage.json diff --git a/translator/src/main/resources/soda/translator/documentation/Soda.tmLanguage.json b/translator/src/main/resources/soda/translator/documentation/Soda.tmLanguage.json new file mode 100644 index 00000000..a3c37111 --- /dev/null +++ b/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": "\\\\." } + ] + } + ] + } + } +} + From 7a648ed8ae4117fdfa2e9287b89ff5ff046f8286 Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Wed, 11 Mar 2026 10:32:59 +0100 Subject: [PATCH 3/5] Use Lean 4.28.0 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index fb746c0a..c631e159 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1,2 +1,2 @@ -leanprover/lean4:v4.21.0 +leanprover/lean4:v4.28.0 From c3176b72d335d59bf49ac8292cf9db6c90d5bbc0 Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Wed, 11 Mar 2026 10:33:14 +0100 Subject: [PATCH 4/5] Update lakefile.lean --- lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 7e69f2c4..4665dc45 100644 --- a/lakefile.lean +++ b/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 From b167a99bc6da90a22aa205645c8ea9a2eaf5c7a0 Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Wed, 11 Mar 2026 10:36:30 +0100 Subject: [PATCH 5/5] Update lake-manifest.json --- lake-manifest.json | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 23999aa8..c1651b94 100644 --- a/lake-manifest.json +++ b/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",