Lean.Elab.runFrontend without typechecking

Stream: lean4

[Arthur Paulino]

Hi! How hard would it be to make runFrontend accept code that doesn't typecheck? Where is the call to the kernel? Thanks!

[Mac]

How are you envisioning writing runnable code that doesn't type-check? Lean relies on types to produce executable code (IR) from terms. A term that does not type check cannot be executed.

[Mac]

Furthermore, type checking failures would inhibit many other important features of Lean (e.g., type inference, type class synthesis, etc.).

[Mac]

I seems very unlikely to me that one could write Lean code that is theoretically runnable but not type-checkable.

[Mac]

As such, I feel this may be a case of an #xy problem. Why do you need this feature?

[Arthur Paulino]

We are building a typechecker for a content-addressed environment built from Lean 4 code. We're using runFrontend to generate the Environment and then we work from there. However, to test our typechecker against expressions that shouldn't typecheck, we'd like to be able to generate environments from Lean 4 code that doesn't typecheck. But those declarations don't appear in the environment

[Arthur Paulino]

It's not that I'd like that feature from Lean. I just want to know where the typechecking routine is called so I can implement my own pipeline of functions that would skip that part

[Henrik Böving]

After runFrontend has parsed the Lean code it basically comes down to elaborating the commands one by one which comes down to running elabCommandTopLevel on each of the command syntaxes and at this point the rest of the elaborator takes over, running the appropriate command elaborators which might call into term elaborators, macros, tactics etc. All of those can do type related stuff that might fail. So I'm not quite sure how you are imagining to modify code here.

[Arthur Paulino]

Maybe I am being too naive. Here's another idea: what if I just avoid the part where some exception is thrown when Lean says "term Foo has type Bla but was expected to have type Doo"?

[Henrik Böving]

Well that exception can be thrown whenever you have elabTermEnsuringType right? and this usually gets called from term elaborators so you are pretty much out of luck with that.

[Locria Cyber]

Arthur Paulino said:

We are building a typechecker for a content-addressed environment built from Lean 4 code. We're using runFrontend to generate the Environment and then we work from there. However, to test our typechecker against expressions that shouldn't typecheck, we'd like to be able to generate environments from Lean 4 code that doesn't typecheck. But those declarations don't appear in the environment

heard of Unison (search for UCM on Github)?

[Locria Cyber]

Lean 4 uses nominal type-equality. I doubt you can make it content-addressed.

[Locria Cyber]

https://github.com/google/evcxr/blob/main/evcxr/HOW_IT_WORKS.md

[Locria Cyber]

This Rust REPL uses a custom parser to split statements. You might have to do similar stuff: remove wrong statements from your source code before compiling.

[Arthur Paulino]

Unison was a big inspiration. We've already content addressed Lean environments and now we're working on the typechecker

[Locria Cyber]

So an REPL is comming soon?

[Arthur Paulino]

There is this toy REPL: https://github.com/arthurpaulino/LeanREPL