Zulip Chat Archive

Stream: lean4

Topic: Lean.Elab.runFrontend without typechecking


Arthur Paulino (Jul 27 2022 at 18:23):

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

Mac (Jul 27 2022 at 19:53):

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 (Jul 27 2022 at 19:55):

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

Mac (Jul 27 2022 at 19:56):

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

Mac (Jul 27 2022 at 19:56):

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

Arthur Paulino (Jul 27 2022 at 21:12):

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 (Jul 27 2022 at 21:28):

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 (Jul 27 2022 at 21:33):

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 (Jul 27 2022 at 22:09):

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 (Jul 27 2022 at 22:18):

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 (Jul 29 2022 at 14:04):

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 (Jul 29 2022 at 14:04):

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

Locria Cyber (Jul 29 2022 at 14:08):

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

Locria Cyber (Jul 29 2022 at 14:08):

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 (Jul 29 2022 at 17:02):

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

Locria Cyber (Oct 21 2022 at 00:08):

So an REPL is comming soon?

Arthur Paulino (Oct 21 2022 at 00:54):

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


Last updated: Dec 20 2023 at 11:08 UTC