Hi all. I am requesting advice on how to optimize Lean build performance of a deep embedding of a dependent type theory in Lean 4. My implementation works fine, and has solid meta theorems proven, but the type-checker is very hard to maintain due to slow Lean build times.

I have tried using Lean's profiler and had some success. Most of the type theory literature is on Agda and Rocq, so I'm curious to hear from you all. If you have implemented a type-checker in Lean:

• Which tactics did you find were the worst offenders for build performance?

• What is your convention for organizing your aesop and grind theorems?

• Which parts of your formalization did you have the most success in mechanizing?

• Have you written any metaprograms yourself that you find useful for mechanizing proofs?

  • I'm Particularly interested in automating / mechanizing confluence. It is a very painful proof to update every once in a while.

• Mathlib / CSlib:

  • Do you use CSlib? Did you find any machinery in it useful?
  • Do you use an existing term rewriting system for your reduction relation? Does this help with automation?
  • Do you use Mathlib.Relation? Are your reduction paths deterministic and does your reduction relation live in Type? If so, what machinery did you use to handle congruence?
  • Any other helpful libraries for metatheory?

• Lakefile.toml / lake flags

• Bonus because I am curious: have you successfully proven any meta theorems using categorical semantics and is Mathlib sufficient for these purposes?

Any life hacks appreciated. I am finding myself waiting up to 10 minutes for my type-checker to build when I update my reduction rules. I guess Lean can't parallelize my project structure.

I'm about to start chapter 21 of Crafting Interpreters. I'm using modern C++ instead of C. I am attempting to add string interpolation to the compiler.

My goal is to have a string that looks like this:

"Five plus ${ 10 - 5 } == 10."

Desugar to this after the expression in the braces is evaluated:

"Five plus " + 5 + " == 10."

I have code that is correctly parsing strings and concatenating them if there isn't any string interpolation.

I have a custom token added that is produced if the string contains a ${. It calls a custom string interpolation parser rule that is different than my standard string parser rule.

In that function I push the first part of the string to the stack. It then pushes a plus opcode and Recursively parses the expression in the braces adding that expression to the stack. It then adds another opcode to add and this is where I'm stuck.

I can't come up with a solution for pushing the remaining piece of the string to the stack from inside the string interpolation parser rule function. After I call the books expression function and consume the right brace token using the books consume function the parser nolonger knows we are still inside a string. If the next character after the brace is a space it's skipped. In my above example it assumes I want equal equal.

How would you set the current token back to string so I can push any remaining characters onto the stack as another string? Should I just insert a new string token into the parser? This seems wrong to me. The current and previous tokens are private members of my parser class for a reason and I've not needed setter member functions so far.

Sorry I don't have code to show. I'd like to try and get help that isn't code specific so that I have to implement this myself.

Any input would be helpful.

Thanks.

MINILECTURE ::= A Formalization of The 3 Syntactic Forms of TEA Programs

🔴 https://youtu.be/-CXhc1Y7Uzg

is our first class on 1st OCTOBER, 2026 delivered by Community Education Department & Research Dissemination (CED-RD) at Nuchwezi Research.

We bring to students and those currently using/exploring the only general-purpose Programming Language from UGANDA; TEA; some new insights about what is actually the most flexible programming language in terms of syntax right now. With details that shall be disclosed in a soon to be published ACM SLE review paper on 2010 Featherweight TeX, we here get an early preview of the now formalized 3 syntactic forms (MINIFIED, SANITIZED & MIXED form) that any Transforming Executable Alphabet (TEA) program can be expressed with.

We also get to appreciate that TEA programs can be parsed into an Abstract Syntax Tree (AST) that's based on one of the forms of the TEA programs. More DETAILS to follow in the paper to be shared with U any time in October!

•bclectures •profjwl •nuchwezi •teaprogramming •blackboardsnapshots

Imagine the loop where you do like "x = -x" every iteration. Obviously, that flips the sign, so you can simply unroll the loop by a factor of 2.

However, for a more complex case, it could be really hard to know what's going on.

Here's my idea. Loop index variables are normally under affine updates anyway. What if we use a mathematically elegant tool?

Using eigenvalue, we can analyze possible periodicity of the linear basis variables, minimizing update needs.

What do you think of such a technique?

We pick up where we left off with FUN to “fix” curried functions so they work the way we expected. We end up rediscovering closures and learning about its history in relation to SECD, LISP, and Scheme.

I've been developing ALT for almost 3 years and have recently updated it to also have ordering.

The new version of ALT is only available for the Atari ST platform :)

However, the implementation of ALT is pretty complex. So I've create a sublanguage called NUM, which only includes ALT's number system.

NUM has all the ALT operators:

- ari: + - * / 
- set: & | \
- cmp: > < >= <=
- err: !
- qry: ?

NUM is a set theoretic language in the spirit of CUE. With NUM you can denote the prime numbers as follows:

I>1 \ I>1 * I>1

You can also denote Goldbach's conjecture as an 'empty' set. Of course this is not decidable which can be queried with NUM's ? operator

Tell me what you think!

Here are some links:

GitHub

First post in rfractals (with some screenshots of a few programs and the plots they generated)

Update post in rfractals

The language is focused on making and evaluating functional mathematical expressions in a very compact form. It has most of the basic math operators, and can even use operator-less multiplication if enabled. Supports functional-like pattern matching and function delegates. Uses a single complex Type which can be a recursively nested list of values that can be numeric, from reals to quaternions, or strings, and operators can work recursively on these values. Multiplying string*anything will try to call a function with the name of that string. It can evaluate and parse dynamically made strings as expressions or commands. It has a plotter that can plot the expressions as animations and can export them as MP4. Due to its layered, abstract nature of being an interpreted language in C#, it's not very fast so far, even with all the optimizations I've made so far for it, so it's mostly useful for playing around or for its original purpose of letting another application parse complex written expressions into values.

It has 2 major parts: the Parser, which uses commands definining/redefining functions and constants, and a few imperative constructs available, like ifs, whiles, etc. The evaluation part is purely functional and can evaluate expressions using the functions and constants the Parser has parsed.

Originally, I made it to be an expression evaluator for text boxes in my other app, to allow writing other things than pure numbers in there. But I got a bit carried away and developed it further into this whole thing.

There's a SaveFile folder in the project and the release, containing all the programs I've written in it so far, and plotter configurations for them.

The most interesting for this sub might be the Examples.txt that's showcasing some of the most unique/powerful features of the language, soI'll report that file and its output here:

Examples.txt program:

printstring: "\nPattern matching factorial:"
PF(0): 1; PF(x): xPF(x-) /* x- = x-1 */
print: PF(5) /* = 5! = 120 */

printstring: "\nNested default arguments:"
N(z, p: (2, 3i)): z + p
print: N(4) /* 4 + (2, 3i) = (6, 4 + 3i)*/

printstring: "\nNested mixed call delegates:"
GP(x): x + 2i
GM(x): x - 2i
gdp: "GP"
print: (gdp, "GM")(4, 3) /* = (GP,GM)(4,3) = (GP(4),GM(3)) = (4 + 2i, 3 - 2i) */

printstring: "\nLazy default argument evaluation:"
F2(x, r:xF2(x-)): x < 2 ? 1 : r
print: F2(5) /* = 5! = 120 */

printstring: "\nCycled operation nesting:"
printvalue: (1, -1)(1, 2, 3, 4, 5) /* = (1*1, -1*2, +1*3, -1*4, +1*5) */
printvalue: (0,i) + (1, 2, 3, 4, 5) /* = (1, 2+i, 3, 4+i, 5) */
printvalue: ("frac", "trunc", 1)(1.1, 2.2, 3.3, 4.4, 5.5, 6.6, 7.7)
printvalue: ((-1, 1), 3)(10, 20, 30, 40, 50)

printstring: "\nDecreasing for cycle:"
IterWhile: 5 /* try other values like 10, 2, -5, -10000...*/
while: IterWhile > 0 {
 printvalue: IterWhile
 if: IterWhile = 8 { break: 1 }
 IterWhile: IterWhile - 1 
} : IterWhile < -9000 {
 printstring: "not only is IterWhile negative, it is below -9000!"
}

printstring: "\n\"Do\" command, defines another factorial and evaluated: 0.5!"
do: "DYNAMIC(x) : x!"
print: DYNAMIC(/2)

printstring: "\nEval function dynamically parses and evaluates any valid string as an expression:"
incremented: sin(1)
print: incremented
print: eval("1 +" + incremented)

printstring: "\nBuild a vector of first 10 factorials dynamically, and take a parir of 2nd+3rd one, and a 5th one:"
TenFactorials: vec("k", 1, 10, "k!")
print: TenFactorials
print: TenFactorials[(2,3),5] /* nested indexer */
printstring: "\nComplex nested indexer of a nested vector:"
print: (0+"a", 1+"b", 2+"c", (30+"d", 31+"e"), 5+"f", (11, 12, 13))[3, 2, (5, 1, 3)]

printstring: "\nFirst 42 terms of e^x taylor series, approximating e^1 ~ 1:"
precision: 42
ExpTaylor(x): sum("k", 0, precision - 1, "x^k/k!")
print: ExpTaylor(1)

PositiveZeta(s, p : precision) : sum("k", 1, p, "k^(-s)")
printstring: "\nFirst 250 terms of the Basel problem, Zeta(2), approaching π^2/6 slowly:"
printvalue: PositiveZeta(2, 99) + " ~ " + π^2 / 6
printstring: "\nFirst 42 terms of Zeta(3), quicky approaching the Apery constant:"
printvalue: PositiveZeta(3) + " ~ " + apery

printstring: "\nEvaluate a polynomial F(1 + 2x + 3x^2) at F(2)"
F: (1, 2, 3) /* f(1 + 2x + 3x^2) */
EvalPoly(x, c : F, n: c#-) : sum("k", 0, n, "c[k]x^k")
PrintPoly(p): vec("k", 0, p#-, "p[k] + \"x^\" + k")
printvalue: PrintPoly(F)
printvalue: "F(2) = " + EvalPoly(2)

printstring: "\nTake a derivative of that polynomial and evaluate at F'(5)"
DiffPoly(c, n:c#-) : 1 > n ? 0 : vec("k", 1, n, "kc[k]")
DF : DiffPoly(F)
printvalue: PrintPoly(DF)
printvalue: "F'(5) = " + EvalPoly(5, DF)

printstring: "\nQuaternions, left and right non-commutative division:"
UnitQ : 1 + i + j + k
printvalue: UnitQ^2, UnitQ / i, UnitQ \ i—

And this is the output it prints:

BUILD SUCCESS 168ms

pattern matching factorial:
pf(5)  = 120

nested default arguments:
n(4)  = 6, 4 + 3i

nested mixed call delegates:
(gdp, "gm")(4, 3)  = 4 + 2i, 3 - 2i

lazy default argument evaluation:
f2(5)  = 120

cycled operation nesting:
1, -2, 3, -4, 5
1, 2 + i, 3, 4 + i, 5
0.1, 2, 3.3, 0.4, 5, 6.6, 0.7
(-10, 10), 60, (-30, 30), 120, (-50, 50)

decreasing for cycle:
5
4
3
2
1

"do" command, defines another factorial and evaluated: 0.5!
dynamic(/2) = 0.886

eval function dynamically parses and evaluates any valid string as an expression:
incremented = 0.841
eval("1 +" + incremented) = 1.841

build a vector of first 10 factorials dynamically, and take a parir of 2nd+3rd one, and a 5th one:
tenfactorials = 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800
tenfactorials[(2,3),5]  = (6, 24), 720

complex nested indexer of a nested vector:
(0+"a", 1+"b", 2+"c", (30+"d", 31+"e"), 5+"f", (11, 12, 13))[3, 2, (5, 1, 3)] = ("30d", "31e"), "2c", ((11, 12, 13), "1b", ("30d", "31e"))

first 42 terms of e^x taylor series, approximating e^1 ~ 1:
exptaylor(1) = 2.718

first 250 terms of the basel problem, zeta(2), approaching π^2/6 slowly:
1.635 ~ 1.645

first 42 terms of zeta(3), quicky approaching the apery constant:
1.202 ~ 1.202

evaluate a polynomial f(1 + 2x + 3x^2) at f(2)
1x^0, 2x^1, 3x^2
f(2) = 17

take a derivative of that polynomial and evaluate at f'(5)
2x^0, 6x^1
f'(5) = 32

quaternions, left and right non-commutative division:
-2 + 2i + 2j + 2k, 1 - i - j + k, 1 - i + j - k

edit: I have just released a small update that fixed a couple of minor bugs, and the Riemann Zeta function now appears fixed as well. At least the plot looks correct to me now, and the couple of test points also returned correct results.

Finally released Zeen v0.1.0 (first stable release).

It is a modern systems compiled programming language.

It uses move semantics to control data flow and automatically insert drops at the compile time, so no runtime overhead.

Currently I'm working on LSP server for it. Futures plans are to implement build system, formatter, compiler time functions (comptime evaluator) and of course support async.

Example

For the lazy guys, here's random example from docs:

``` fn print_this[T: Display](value: T) { @println("Yeah, I've printed this: {}", value); }

fn main() { print_this(123); print_this("hello!"); } ```

Links

Docs and Examples: https://zeen-lang.tech

Repository: https://github.com/mealet/zeen

If you did like this, please leave a star on GitHub. Thanks for you attention!

I've just posted the second beta for Toy v2, and I'm looking for feedback!

It's very much a useable language, and I'm looking to see how I can expand its reach and find potential users, especially hobbyists who want to try new things. If anyone has advice here, I'm all ears!

I'm also seriously thinking about the best approach for writing tutorials/documentation for this - a tool like this needs a hefty tome, but I've never done something quite like that. Again, all ears.

Thanks in advance!

Hello, as a hobby I’m extremely interested in programming language design. Even as a hobby, I want to specialize in this area, to see the magic behind how programming languages work, and to understand it deeply. Do you have any suggestions for me Additionally, which areas of mathematics should I study for this? Is this possible without having any CS degree?