forward declarations

Stream: lean4

[Arthur Paulino]

Hello! :wave:
What are the motivations for using forward declarations like these? Why not just state the implementation right away?

[Wojciech Nawrocki]

Most likely it is bootstrapping concerns, or avoiding import cycles. whnf can be used immediately in Lean.Meta.Basic where it is defined without importing all the extra stuff that Lean.Meta.WHNF (where it is implemented) relies on.

[Leonardo de Moura]

Additional remarks:

• When we implemented this code, we were using the Lean 3 frontend, and the support for mutual recursion was very primitive
• We have it today, but it would force us to put inferType, whnf, and isDefEq in the same mutual block. This would be a very big mutual block, and it would dramatically hurt the compilation times.

[Leonardo de Moura]

That being said, we want to have proper forward declaration support in Lean 4 in the future. The current workaround is very hackish.

[Arthur Paulino]

Thanks!

[Henrik Böving]

Leonardo de Moura said:

Additional remarks:

• When we implemented this code, we were using the Lean 3 frontend, and the support for mutual recursion was very primitive
• We have it today, but it would force us to put inferType, whnf, and isDefEq in the same mutual block. This would be a very big mutual block, and it would dramatically hurt the compilation times.

Why do mutual types hurt compilations times so much? Is it because they are had to check?

[Leonardo de Moura]

Henrik Böving said:

Leonardo de Moura said:

Additional remarks:

• When we implemented this code, we were using the Lean 3 frontend, and the support for mutual recursion was very primitive
• We have it today, but it would force us to put inferType, whnf, and isDefEq in the same mutual block. This would be a very big mutual block, and it would dramatically hurt the compilation times.

Why do mutual types hurt compilations times so much? Is it because they are had to check?

In this particular case, it would force us to put a lot of code in a single file src/Lean/Meta/Basic.lean, and many other files depend on it. The file src/Lean/Meta/ExprDefEq.lean is one of the most expensive files to compile. Right now, very few files depend on it because we used the forward declaration hack. This makes my life way more convenient. When I change this file, I don't have to recompile a ton of other files. Without the forward declaration hack, all this code would have to be at src/Lean/Meta/Basic.lean.
Mutual definitions have the other minor and more general performance problems:

• They are treated as a single command. Any modification will force the server to recompile the whole block from scratch.
• If we are not using partial, then we also have the overhead of combining all definitions into a single declaration. If we have hundreds of functions, we will need a big sum type there.