Customize compile time error messages

Stream: lean4

[Raúl Raja Martínez]

I'm in need to parse Lean's compiler error messages and was wondering if:

1. There is a structured output format such as json or similar besides text.
2. Can the output be customized for certain cases. For example I have:

def GTE0 (n : Int) : Prop := n >= 0

example : Prop := GTE0 6 -- works

example : Prop := GTE0 -1
-- failed to synthesize instance
--  HSub (Int → Prop) Nat Prop

I'd like to get a more meaningful error than the type class isn't resolved. Something like -1 is not gte 0
I'm using lean as a backend to verify third party languages whose types may include refinements like the ones above for programs I have no control over.

Thanks!

[Henrik Böving]

But the issue above is not that lean cannot infere automatically that -1 is not gte 0, you are never constructing a proof of that statement, the issue is that lean is not parsing your stuff in the way you expect, this works:

example : Prop := GTE0 (-1)

[Gabriel Ebner]

Your example is parsed as (GTE0) - 1 to be clear.

[Henrik Böving]

I'm also not exactly sure how you are planning to do verification of third party languages in a way where the above would be an issue? Are you planning to just straight up translate their code into Lean code? That seems rather excessive to me, You could instead write inductive types that represent terms of your other language + algorithms on those types + proofs for those algorithms for example

[Sebastian Ullrich]

The direct translation approach is way cooler though (but nowadays you should probably just read https://arxiv.org/abs/2206.07185 instead)

[Raúl Raja Martínez]

Thanks everyone for the input.

I'll try to elaborate more what I'm trying to do in case you have a better idea on how I might accomplish this.
First, I'm new to lean, I'm investigating lean to use as backend for verification of Scala, Kotlin and some other mainstream languages.

We have already developed tools in some of those languages backed by SMT such as https://arrow-kt.io/docs/analysis/conditions/
Here in Arrow analysis we use a form of Hoare logic to have pre, post, invariant conditions over functions to detect common errors that end up in runtime exceptions in most of these languages. For example Arrow analysis can analyze unsafe calls given Kotlin data flow and fail at compile time like this:
Given an imported law such as:

@Law
  inline fun <E> List<E>.getLaw(index: Int): E {
    pre(index >= 0 && index < size) { "index within bounds" }
    return get(index)
  }

The following expression fails to compile

val wrong = emptyList<Int>().get(2)

e: Example.kt: (1, 18): pre-condition `index within bounds` is not satisfied in `get(2)`
  -> unsatisfiable constraint: `((2 >= 0) && (2 < emptyList<Int>().size))`
  -> `2` bound to param `index` in `kotlin.collections.List.get`
  -> main function body

I would like to replace our current scope based approach using SMT for a lean backend.

I'm trying two different approaches.

1. Embed the foreign language into lean using lean's macro and syntax system. Expressing semantics of unknown types is still something I'm not sure how to encode but I got Java and a subset of Kotlin parsed which is missng elab functions to expand to lean command and terms. I even dreamed that If I build first support for antlr grammars I can get syntax automatically using most of the antlr .g4 files for most langs https://github.com/antlr/grammars-v4

2. Directly translate with compiler plugins in Kotlin elsewhere their AST to Lean in a transpiler fashion. I'm not sure here yet how to map foreign symbols in jars and other binaries to which I have no body access. I suppose lean would allow me to declare abstract declarations from which I can still infer interesting things.

If you wanted to verify in Lean something like the example above for unsafe access to an empty list, what would be the equivalent lean code for that example? what kind of error would it produce when it detects an unsafe access?

Thanks!