refactor: module-ize Lean (#9330)

.github/workflows/build-template.yml

@@ -199,7 +199,7 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/stage1/bin/lean --stats src/Lean.lean
+          build/stage1/bin/lean --stats src/Lean.lean -Dexperimental.module=true
         if: ${{ !matrix.cross }}
       - name: Test
         id: test

script/bench.sh

@@ -4,12 +4,12 @@ set -euo pipefail
 cmake --preset release -DUSE_LAKE=ON 1>&2
 
 # We benchmark against stage 2 to test new optimizations.
-timeout -s KILL 1h time make -C build/release -j$(nproc) stage2 1>&2
+timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
 export PATH=$PWD/build/release/stage2/bin:$PATH
 
 # The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
 # easier to configure them statically.
-cmake -B build/release/stage2 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
+cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
 
 cd tests/bench
 timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2

src/Init/Control/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Core
 public import Init.BinderNameHint
 
-public section
+@[expose] public section
 
 universe u v w
 

src/Init/Data/String/Basic.lean

@@ -301,7 +301,7 @@ Examples:
 * `"L∃∀N".atEnd ⟨7⟩ = false`
 * `"L∃∀N".atEnd ⟨8⟩ = true`
 -/
-@[extern "lean_string_utf8_at_end"]
+@[extern "lean_string_utf8_at_end", expose]
 def atEnd : (@& String) → (@& Pos) → Bool
   | s, p => p.byteIdx ≥ utf8ByteSize s
 

src/Lean.lean

@@ -3,45 +3,47 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Data
-import Lean.Compiler
-import Lean.Environment
-import Lean.Modifiers
-import Lean.ProjFns
-import Lean.Runtime
-import Lean.ResolveName
-import Lean.Attributes
-import Lean.Parser
-import Lean.ReducibilityAttrs
-import Lean.Elab
-import Lean.Class
-import Lean.LocalContext
-import Lean.MetavarContext
-import Lean.AuxRecursor
-import Lean.Meta
-import Lean.Util
-import Lean.Structure
-import Lean.PrettyPrinter
-import Lean.CoreM
-import Lean.ReservedNameAction
-import Lean.InternalExceptionId
-import Lean.Server
-import Lean.ScopedEnvExtension
-import Lean.DocString
-import Lean.DeclarationRange
-import Lean.LoadDynlib
-import Lean.Widget
-import Lean.Log
-import Lean.Linter
-import Lean.SubExpr
-import Lean.LabelAttribute
-import Lean.AddDecl
-import Lean.Replay
-import Lean.PrivateName
-import Lean.PremiseSelection
-import Lean.Namespace
-import Lean.EnvExtension
-import Lean.ErrorExplanation
-import Lean.ErrorExplanations
-import Lean.DefEqAttrib
-import Lean.Shell
+module
+
+public import Lean.Data
+public import Lean.Compiler
+public import Lean.Environment
+public import Lean.Modifiers
+public import Lean.ProjFns
+public import Lean.Runtime
+public import Lean.ResolveName
+public import Lean.Attributes
+public import Lean.Parser
+public import Lean.ReducibilityAttrs
+public import Lean.Elab
+public import Lean.Class
+public import Lean.LocalContext
+public import Lean.MetavarContext
+public import Lean.AuxRecursor
+public import Lean.Meta
+public import Lean.Util
+public import Lean.Structure
+public import Lean.PrettyPrinter
+public import Lean.CoreM
+public import Lean.ReservedNameAction
+public import Lean.InternalExceptionId
+public import Lean.Server
+public import Lean.ScopedEnvExtension
+public import Lean.DocString
+public import Lean.DeclarationRange
+public import Lean.LoadDynlib
+public import Lean.Widget
+public import Lean.Log
+public import Lean.Linter
+public import Lean.SubExpr
+public import Lean.LabelAttribute
+public import Lean.AddDecl
+public import Lean.Replay
+public import Lean.PrivateName
+public import Lean.PremiseSelection
+public import Lean.Namespace
+public import Lean.EnvExtension
+public import Lean.ErrorExplanation
+public import Lean.ErrorExplanations
+public import Lean.DefEqAttrib
+public import Lean.Shell

src/Lean/AddDecl.lean

@@ -3,10 +3,14 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.CoreM
-import Lean.Namespace
-import Lean.Util.CollectAxioms
+public import Lean.CoreM
+public import Lean.Namespace
+public import Lean.Util.CollectAxioms
+
+public section
 
 namespace Lean
 

src/Lean/Attributes.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.CoreM
-import Lean.MonadEnv
+public import Lean.CoreM
+public import Lean.MonadEnv
+
+public section
 
 namespace Lean
 

src/Lean/AuxRecursor.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.EnvExtension
+public import Lean.EnvExtension
+
+public section
 
 namespace Lean
 

src/Lean/BuiltinDocAttr.lean

@@ -3,9 +3,13 @@ Copyright (c) 2024 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+module
+
 prelude
-import Lean.Compiler.InitAttr
-import Lean.DocString.Extension
+public import Lean.Compiler.InitAttr
+public import Lean.DocString.Extension
+
+public section
 
 namespace Lean
 

src/Lean/Class.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Attributes
+public import Lean.Attributes
+
+public section
 
 namespace Lean
 

src/Lean/Compiler.lean

@@ -3,17 +3,21 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.InlineAttrs
-import Lean.Compiler.Specialize
-import Lean.Compiler.ClosedTermCache
-import Lean.Compiler.ExternAttr
-import Lean.Compiler.ImplementedByAttr
-import Lean.Compiler.NeverExtractAttr
-import Lean.Compiler.IR
-import Lean.Compiler.CSimpAttr
-import Lean.Compiler.FFI
-import Lean.Compiler.MetaAttr
-import Lean.Compiler.NoncomputableAttr
-import Lean.Compiler.Main
-import Lean.Compiler.Old -- TODO: delete after we port code generator to Lean
+public import Lean.Compiler.InlineAttrs
+public import Lean.Compiler.Specialize
+public import Lean.Compiler.ClosedTermCache
+public import Lean.Compiler.ExternAttr
+public import Lean.Compiler.ImplementedByAttr
+public import Lean.Compiler.NeverExtractAttr
+public import Lean.Compiler.IR
+public import Lean.Compiler.CSimpAttr
+public import Lean.Compiler.FFI
+public import Lean.Compiler.MetaAttr
+public import Lean.Compiler.NoncomputableAttr
+public import Lean.Compiler.Main
+public import Lean.Compiler.Old -- TODO: delete after we port code generator to Lean
+
+public section

src/Lean/Compiler/BorrowedAnnotation.lean

@@ -3,8 +3,12 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Expr
+public import Lean.Expr
+
+public section
 namespace Lean
 
 def markBorrowed (e : Expr) : Expr :=

src/Lean/Compiler/CSimpAttr.lean

@@ -3,10 +3,14 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.ScopedEnvExtension
-import Lean.Util.Recognizers
-import Lean.Util.ReplaceExpr
+public import Lean.ScopedEnvExtension
+public import Lean.Util.Recognizers
+public import Lean.Util.ReplaceExpr
+
+public section
 
 namespace Lean.Compiler
 namespace CSimp

src/Lean/Compiler/ClosedTermCache.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Environment
+public import Lean.Environment
+
+public section
 
 namespace Lean
 

src/Lean/Compiler/ExportAttr.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Attributes
+public import Lean.Attributes
+
+public section
 
 namespace Lean
 

src/Lean/Compiler/ExternAttr.lean

@@ -3,13 +3,17 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Init.Data.List.BasicAux
-import Lean.Expr
-import Lean.Environment
-import Lean.Attributes
-import Lean.ProjFns
-import Lean.Meta.Basic
+public import Init.Data.List.BasicAux
+public import Lean.Expr
+public import Lean.Environment
+public import Lean.Attributes
+public import Lean.ProjFns
+public import Lean.Meta.Basic
+
+public section
 
 namespace Lean
 

src/Lean/Compiler/FFI.lean

@@ -3,9 +3,13 @@ Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+module
+
 prelude
-import Init.Data.Array.Basic
-import Init.System.FilePath
+public import Init.Data.Array.Basic
+public import Init.System.FilePath
+
+public section
 
 open System
 

src/Lean/Compiler/IR.lean

@@ -3,33 +3,37 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.AddExtern
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.Format
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.PushProj
-import Lean.Compiler.IR.ElimDeadVars
-import Lean.Compiler.IR.SimpCase
-import Lean.Compiler.IR.ResetReuse
-import Lean.Compiler.IR.NormIds
-import Lean.Compiler.IR.Checker
-import Lean.Compiler.IR.Borrow
-import Lean.Compiler.IR.Boxing
-import Lean.Compiler.IR.RC
-import Lean.Compiler.IR.ExpandResetReuse
-import Lean.Compiler.IR.UnboxResult
-import Lean.Compiler.IR.ElimDeadBranches
-import Lean.Compiler.IR.EmitC
-import Lean.Compiler.IR.Sorry
-import Lean.Compiler.IR.ToIR
-import Lean.Compiler.IR.ToIRType
-import Lean.Compiler.IR.Meta
+public import Lean.Compiler.IR.AddExtern
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Format
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.PushProj
+public import Lean.Compiler.IR.ElimDeadVars
+public import Lean.Compiler.IR.SimpCase
+public import Lean.Compiler.IR.ResetReuse
+public import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.IR.Checker
+public import Lean.Compiler.IR.Borrow
+public import Lean.Compiler.IR.Boxing
+public import Lean.Compiler.IR.RC
+public import Lean.Compiler.IR.ExpandResetReuse
+public import Lean.Compiler.IR.UnboxResult
+public import Lean.Compiler.IR.ElimDeadBranches
+public import Lean.Compiler.IR.EmitC
+public import Lean.Compiler.IR.Sorry
+public import Lean.Compiler.IR.ToIR
+public import Lean.Compiler.IR.ToIRType
+public import Lean.Compiler.IR.Meta
 
 -- The following imports are not required by the compiler. They are here to ensure that there
 -- are no orphaned modules.
-import Lean.Compiler.IR.LLVMBindings
-import Lean.Compiler.IR.EmitLLVM
+public import Lean.Compiler.IR.LLVMBindings
+public import Lean.Compiler.IR.EmitLLVM
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/AddExtern.lean

@@ -4,15 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Zwarich
 -/
 
+module
+
 prelude
-import Lean.CoreM
-import Lean.Compiler.BorrowedAnnotation
-import Lean.Compiler.ExternAttr
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.Boxing
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.ToIRType
-import Lean.Compiler.LCNF.MonoTypes
+public import Lean.CoreM
+public import Lean.Compiler.BorrowedAnnotation
+public import Lean.Compiler.ExternAttr
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Boxing
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.ToIRType
+public import Lean.Compiler.LCNF.MonoTypes
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/Basic.lean

@@ -3,11 +3,15 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Data.KVMap
-import Lean.Data.Name
-import Lean.Data.Format
-import Lean.Compiler.ExternAttr
+public import Lean.Data.KVMap
+public import Lean.Data.Name
+public import Lean.Data.Format
+public import Lean.Compiler.ExternAttr
+
+public section
 /-!
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

src/Lean/Compiler/IR/Borrow.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.ExportAttr
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.ExportAttr
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.NormIds
+
+public section
 
 namespace Lean
 namespace IR

src/Lean/Compiler/IR/Boxing.lean

@@ -3,16 +3,20 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Runtime
-import Lean.Compiler.ClosedTermCache
-import Lean.Compiler.ExternAttr
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.FreeVars
-import Lean.Compiler.IR.ElimDeadVars
-import Lean.Compiler.IR.ToIRType
-import Lean.Data.AssocList
+public import Lean.Runtime
+public import Lean.Compiler.ClosedTermCache
+public import Lean.Compiler.ExternAttr
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.FreeVars
+public import Lean.Compiler.IR.ElimDeadVars
+public import Lean.Compiler.IR.ToIRType
+public import Lean.Data.AssocList
+
+public section
 
 namespace Lean.IR.ExplicitBoxing
 /-!

src/Lean/Compiler/IR/Checker.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.Format
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.Format
+
+public section
 
 namespace Lean.IR.Checker
 

src/Lean/Compiler/IR/CompilerM.lean

@@ -3,14 +3,18 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.CoreM
-import Lean.Environment
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.Format
-import Lean.Compiler.MetaAttr
-import Lean.Compiler.ExportAttr
-import Lean.Compiler.LCNF.PhaseExt
+public import Lean.CoreM
+public import Lean.Environment
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Format
+public import Lean.Compiler.MetaAttr
+public import Lean.Compiler.ExportAttr
+public import Lean.Compiler.LCNF.PhaseExt
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Format
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.Format
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.CompilerM
+
+public section
 
 namespace Lean.IR.UnreachableBranches
 

src/Lean/Compiler/IR/ElimDeadVars.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.FreeVars
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.FreeVars
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/EmitC.lean

@@ -3,16 +3,20 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Runtime
-import Lean.Compiler.NameMangling
-import Lean.Compiler.ExportAttr
-import Lean.Compiler.InitAttr
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.EmitUtil
-import Lean.Compiler.IR.NormIds
-import Lean.Compiler.IR.SimpCase
-import Lean.Compiler.IR.Boxing
+public import Lean.Runtime
+public import Lean.Compiler.NameMangling
+public import Lean.Compiler.ExportAttr
+public import Lean.Compiler.InitAttr
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.EmitUtil
+public import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.IR.SimpCase
+public import Lean.Compiler.IR.Boxing
+
+public section
 
 namespace Lean.IR.EmitC
 open ExplicitBoxing (requiresBoxedVersion mkBoxedName isBoxedName)

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -3,18 +3,22 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
+module
+
 prelude
-import Lean.Runtime
-import Lean.Compiler.NameMangling
-import Lean.Compiler.ExportAttr
-import Lean.Compiler.InitAttr
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.EmitUtil
-import Lean.Compiler.IR.NormIds
-import Lean.Compiler.IR.SimpCase
-import Lean.Compiler.IR.Boxing
-import Lean.Compiler.IR.ResetReuse
-import Lean.Compiler.IR.LLVMBindings
+public import Lean.Runtime
+public import Lean.Compiler.NameMangling
+public import Lean.Compiler.ExportAttr
+public import Lean.Compiler.InitAttr
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.EmitUtil
+public import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.IR.SimpCase
+public import Lean.Compiler.IR.Boxing
+public import Lean.Compiler.IR.ResetReuse
+public import Lean.Compiler.IR.LLVMBindings
+
+public section
 
 open Lean.IR.ExplicitBoxing (isBoxedName)
 

src/Lean/Compiler/IR/EmitUtil.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.InitAttr
-import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.InitAttr
+public import Lean.Compiler.IR.CompilerM
+
+public section
 
 /-! # Helper functions for backend code generators -/
 

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.NormIds
-import Lean.Compiler.IR.FreeVars
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.IR.FreeVars
+
+public section
 
 namespace Lean.IR.ExpandResetReuse
 /-- Mapping from variable to projections -/

src/Lean/Compiler/IR/Format.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Basic
+
+public section
 
 namespace Lean
 namespace IR
@@ -13,7 +17,7 @@ private def formatArg : Arg → Format
   | Arg.var id => format id
   | Arg.erased => "◾"
 
-instance : ToFormat Arg := ⟨formatArg⟩
+instance : ToFormat Arg := ⟨private_decl% formatArg⟩
 
 def formatArray {α : Type} [ToFormat α] (args : Array α) : Format :=
   args.foldl (fun r a => r ++ " " ++ format a) Format.nil
@@ -22,7 +26,7 @@ private def formatLitVal : LitVal → Format
   | LitVal.num v => format v
   | LitVal.str v => format (repr v)
 
-instance : ToFormat LitVal := ⟨formatLitVal⟩
+instance : ToFormat LitVal := ⟨private_decl% formatLitVal⟩
 
 private def formatCtorInfo : CtorInfo → Format
   | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } => Id.run do
@@ -33,7 +37,7 @@ private def formatCtorInfo : CtorInfo → Format
       r := f!"{r}[{name}]"
     r
 
-instance : ToFormat CtorInfo := ⟨formatCtorInfo⟩
+instance : ToFormat CtorInfo := ⟨private_decl% formatCtorInfo⟩
 
 private def formatExpr : Expr → Format
   | Expr.ctor i ys      => format i ++ formatArray ys
@@ -50,7 +54,7 @@ private def formatExpr : Expr → Format
   | Expr.lit v          => format v
   | Expr.isShared x     => "isShared " ++ format x
 
-instance : ToFormat Expr := ⟨formatExpr⟩
+instance : ToFormat Expr := ⟨private_decl% formatExpr⟩
 instance : ToString Expr := ⟨fun e => Format.pretty (format e)⟩
 
 private partial def formatIRType : IRType → Format
@@ -78,7 +82,7 @@ instance : ToString IRType := ⟨toString ∘ format⟩
 private def formatParam : Param → Format
   | { x := name, borrow := b, ty := ty } => "(" ++ format name ++ " : " ++ (if b then "@& " else "") ++ format ty ++ ")"
 
-instance : ToFormat Param := ⟨formatParam⟩
+instance : ToFormat Param := ⟨private_decl% formatParam⟩
 
 def formatAlt (fmt : FnBody → Format) (indent : Nat) : Alt → Format
   | Alt.ctor i b  => format i.name ++ " →" ++ Format.nest indent (Format.line ++ fmt b)

src/Lean/Compiler/IR/FreeVars.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Basic
+
+public section
 
 namespace Lean.IR
 
@@ -25,7 +29,7 @@ abbrev Collector := Index → Index
 @[inline] private def collectJP (j : JoinPointId) : Collector := collect j.idx
 @[inline] private def seq (k₁ k₂ : Collector) : Collector := k₂ ∘ k₁
 instance : AndThen Collector where
-  andThen a b := seq a (b ())
+  andThen a b := private seq a (b ())
 
 private def collectArg : Arg → Collector
   | .var x  => collectVar x
@@ -121,7 +125,7 @@ def insertParams (s : IndexSet) (ys : Array Param) : IndexSet :=
   fun k₁ k₂ bv fv => k₂ bv (k₁ bv fv)
 
 instance : AndThen Collector where
-  andThen a b := seq a (b ())
+  andThen a b := private seq a (b ())
 
 private def collectArg : Arg → Collector
   | .var x  => collectVar x

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
+module
+
 prelude
-import Init.System.IO
+public import Init.System.IO
+
+public section
 
 namespace LLVM
 /-!
@@ -41,49 +45,49 @@ def AttributeIndex.AttributeFunctionIndex : AttributeIndex := { val := 184467440
 
 structure BasicBlock (ctx : Context)  where
   private mk :: ptr : USize
-instance : Nonempty (BasicBlock ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (BasicBlock ctx) := by exact ⟨{ ptr := default }⟩
 
 structure Builder (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (Builder ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (Builder ctx) := by exact ⟨{ ptr := default }⟩
 
 structure Context where
   private mk :: ptr : USize
-instance : Nonempty Context := ⟨{ ptr := default }⟩
+instance : Nonempty Context := by exact ⟨{ ptr := default }⟩
 
 structure LLVMType (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (LLVMType ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (LLVMType ctx) := by exact ⟨{ ptr := default }⟩
 
 structure MemoryBuffer (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (MemoryBuffer ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (MemoryBuffer ctx) := by exact ⟨{ ptr := default }⟩
 
 structure Module (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (Module ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (Module ctx) := by exact ⟨{ ptr := default }⟩
 
 /-
 structure PassManager (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (PassManager ctx) := by exact ⟨{ ptr := default }⟩
 
 structure PassManagerBuilder (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (PassManagerBuilder ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (PassManagerBuilder ctx) := by exact ⟨{ ptr := default }⟩
 -/
 
 structure Target (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (Target ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (Target ctx) := by exact ⟨{ ptr := default }⟩
 
 structure TargetMachine (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (TargetMachine ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (TargetMachine ctx) := by exact ⟨{ ptr := default }⟩
 
 structure Value (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (Value ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (Value ctx) := by exact ⟨{ ptr := default }⟩
 
 /-- Check if the value is a null pointer. --/
 def Value.isNull (v : Value ctx) : Bool := v.ptr == 0
@@ -93,7 +97,7 @@ opaque Value.getName {ctx : Context} (value : Value ctx) : BaseIO String
 
 structure Attribute (ctx : Context) where
   private mk :: ptr : USize
-instance : Nonempty (Attribute ctx) := ⟨{ ptr := default }⟩
+instance : Nonempty (Attribute ctx) := by exact ⟨{ ptr := default }⟩
 
 @[extern "lean_llvm_initialize_target_info"]
 opaque llvmInitializeTargetInfo : BaseIO (Unit)

src/Lean/Compiler/IR/LiveVars.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.FreeVars
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.FreeVars
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/Meta.lean

@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+module
+
 prelude
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.MetaAttr
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.MetaAttr
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/NormIds.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Basic
+
+public section
 
 namespace Lean.IR.UniqueIds
 

src/Lean/Compiler/IR/PushProj.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.FreeVars
-import Lean.Compiler.IR.NormIds
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.FreeVars
+public import Lean.Compiler.IR.NormIds
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/RC.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Runtime
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.LiveVars
+public import Lean.Runtime
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.LiveVars
+
+public section
 
 namespace Lean.IR.ExplicitRC
 /-!

src/Lean/Compiler/IR/ResetReuse.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.LiveVars
-import Lean.Compiler.IR.Format
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.LiveVars
+public import Lean.Compiler.IR.Format
+
+public section
 
 namespace Lean.IR.ResetReuse
 /-!

src/Lean/Compiler/IR/SimpCase.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.Format
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Format
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/Sorry.lean

@@ -3,8 +3,12 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.CompilerM
+
+public section
 
 namespace Lean.IR
 namespace Sorry

src/Lean/Compiler/IR/ToIR.lean

@@ -3,15 +3,19 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Zwarich
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.CompilerM
-import Lean.Compiler.IR.ToIRType
-import Lean.CoreM
-import Lean.Environment
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.CompilerM
+public import Lean.Compiler.IR.ToIRType
+public import Lean.CoreM
+public import Lean.Environment
+
+public section
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/ToIRType.lean

@@ -3,12 +3,16 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Environment
-import Lean.Compiler.IR.Format
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.MonoTypes
-import Lean.Compiler.LCNF.Types
+public import Lean.Environment
+public import Lean.Compiler.IR.Format
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.Types
+
+public section
 
 namespace Lean
 namespace IR

src/Lean/Compiler/IR/UnboxResult.lean

@@ -3,9 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Data.Format
-import Lean.Compiler.IR.Basic
+public import Lean.Data.Format
+public import Lean.Compiler.IR.Basic
+
+public section
 
 namespace Lean.IR.UnboxResult
 

src/Lean/Compiler/ImplementedByAttr.lean

@@ -3,12 +3,16 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Attributes
-import Lean.Declaration
-import Lean.MonadEnv
-import Lean.Elab.InfoTree
-import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Attributes
+public import Lean.Declaration
+public import Lean.MonadEnv
+public import Lean.Elab.InfoTree
+public import Lean.Compiler.LCNF.PhaseExt
+
+public section
 
 namespace Lean.Compiler
 

src/Lean/Compiler/InitAttr.lean

@@ -3,10 +3,14 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.AddDecl
-import Lean.MonadEnv
-import Lean.Elab.InfoTree.Main
+public import Lean.AddDecl
+public import Lean.MonadEnv
+public import Lean.Elab.InfoTree.Main
+
+public section
 
 namespace Lean
 

src/Lean/Compiler/InlineAttrs.lean

@@ -3,8 +3,12 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Attributes
+public import Lean.Attributes
+
+public section
 
 
 namespace Lean.Compiler
@@ -77,7 +81,7 @@ private def hasInlineAttrCore (env : Environment) (kind : InlineAttributeKind) (
   | some k => kind == k
   | _ => false
 
-abbrev hasInlineAttribute (env : Environment) (declName : Name) : Bool :=
+@[inline] def hasInlineAttribute (env : Environment) (declName : Name) : Bool :=
   hasInlineAttrCore env .inline declName
 
 def hasInlineIfReduceAttribute (env : Environment) (declName : Name) : Bool :=
@@ -89,7 +93,7 @@ def hasNoInlineAttribute (env : Environment) (declName : Name) : Bool :=
 def hasMacroInlineAttribute (env : Environment) (declName : Name) : Bool :=
   hasInlineAttrCore env .macroInline declName
 
-abbrev hasAlwaysInlineAttribute (env : Environment) (declName : Name) : Bool :=
+@[inline] def hasAlwaysInlineAttribute (env : Environment) (declName : Name) : Bool :=
   hasInlineAttrCore env .alwaysInline declName
 
 end Lean.Compiler

src/Lean/Compiler/LCNF.lean

@@ -3,42 +3,46 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.AlphaEqv
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.Bind
-import Lean.Compiler.LCNF.Check
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.CSE
-import Lean.Compiler.LCNF.DependsOn
-import Lean.Compiler.LCNF.ElimDead
-import Lean.Compiler.LCNF.FixedParams
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.JoinPoints
-import Lean.Compiler.LCNF.LCtx
-import Lean.Compiler.LCNF.Level
-import Lean.Compiler.LCNF.Main
-import Lean.Compiler.LCNF.Passes
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.PrettyPrinter
-import Lean.Compiler.LCNF.PullFunDecls
-import Lean.Compiler.LCNF.PullLetDecls
-import Lean.Compiler.LCNF.ReduceJpArity
-import Lean.Compiler.LCNF.Simp
-import Lean.Compiler.LCNF.Specialize
-import Lean.Compiler.LCNF.SpecInfo
-import Lean.Compiler.LCNF.Testing
-import Lean.Compiler.LCNF.ToDecl
-import Lean.Compiler.LCNF.ToExpr
-import Lean.Compiler.LCNF.ToLCNF
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.Util
-import Lean.Compiler.LCNF.ConfigOptions
-import Lean.Compiler.LCNF.MonoTypes
-import Lean.Compiler.LCNF.ToMono
-import Lean.Compiler.LCNF.MonadScope
-import Lean.Compiler.LCNF.Closure
-import Lean.Compiler.LCNF.LambdaLifting
-import Lean.Compiler.LCNF.ReduceArity
-import Lean.Compiler.LCNF.Probing
+public import Lean.Compiler.LCNF.AlphaEqv
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Bind
+public import Lean.Compiler.LCNF.Check
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.CSE
+public import Lean.Compiler.LCNF.DependsOn
+public import Lean.Compiler.LCNF.ElimDead
+public import Lean.Compiler.LCNF.FixedParams
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.JoinPoints
+public import Lean.Compiler.LCNF.LCtx
+public import Lean.Compiler.LCNF.Level
+public import Lean.Compiler.LCNF.Main
+public import Lean.Compiler.LCNF.Passes
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.PrettyPrinter
+public import Lean.Compiler.LCNF.PullFunDecls
+public import Lean.Compiler.LCNF.PullLetDecls
+public import Lean.Compiler.LCNF.ReduceJpArity
+public import Lean.Compiler.LCNF.Simp
+public import Lean.Compiler.LCNF.Specialize
+public import Lean.Compiler.LCNF.SpecInfo
+public import Lean.Compiler.LCNF.Testing
+public import Lean.Compiler.LCNF.ToDecl
+public import Lean.Compiler.LCNF.ToExpr
+public import Lean.Compiler.LCNF.ToLCNF
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.Util
+public import Lean.Compiler.LCNF.ConfigOptions
+public import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.ToMono
+public import Lean.Compiler.LCNF.MonadScope
+public import Lean.Compiler.LCNF.Closure
+public import Lean.Compiler.LCNF.LambdaLifting
+public import Lean.Compiler.LCNF.ReduceArity
+public import Lean.Compiler.LCNF.Probing
+
+public section

src/Lean/Compiler/LCNF/AlphaEqv.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/AuxDeclCache.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.DeclHash
-import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.DeclHash
+public import Lean.Compiler.LCNF.Internalize
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/BaseTypes.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Types
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -3,14 +3,18 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Init.Data.List.BasicAux
-import Lean.Expr
-import Lean.Meta.Instances
-import Lean.Compiler.ExternAttr
-import Lean.Compiler.InlineAttrs
-import Lean.Compiler.Specialize
-import Lean.Compiler.LCNF.Types
+public import Init.Data.List.BasicAux
+public import Lean.Expr
+public import Lean.Meta.Instances
+public import Lean.Compiler.ExternAttr
+public import Lean.Compiler.InlineAttrs
+public import Lean.Compiler.Specialize
+public import Lean.Compiler.LCNF.Types
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Bind.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.InferType
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/CSE.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.ToExpr
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.NeverExtractAttr
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.ToExpr
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.NeverExtractAttr
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Check.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.PrettyPrinter
-import Lean.Compiler.LCNF.CompatibleTypes
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.PrettyPrinter
+public import Lean.Compiler.LCNF.CompatibleTypes
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Closure.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Util.ForEachExprWhere
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Util.ForEachExprWhere
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Closure

src/Lean/Compiler/LCNF/CompatibleTypes.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.InferType
+
+public section
 
 namespace Lean.Compiler.LCNF
 
@@ -21,7 +25,7 @@ We claim it is "defensible" to say this sanity checker is a linter. If the sanit
 and performance may suffer at runtime.
 Here is an example of code that "abuses" dependent types:
 ```
-def Tuple (α : Type u) : Nat → Type u
+@[expose] def Tuple (α : Type u) : Nat → Type u
   | 0   => PUnit
   | 1   => α
   | n+2 => α × Tuple α (n+1)

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.CoreM
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.LCtx
-import Lean.Compiler.LCNF.ConfigOptions
+public import Lean.CoreM
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.LCtx
+public import Lean.Compiler.LCNF.ConfigOptions
+
+public section
 
 namespace Lean.Compiler.LCNF
 /--
@@ -315,8 +319,8 @@ Add the entry `fvarId ↦ fvarId'` to the free variable substitution.
 @[inline, inherit_doc normLetValueImp] def normLetValue [MonadFVarSubst m t] [Monad m] (e : LetValue) : m LetValue :=
   return normLetValueImp (← getSubst) e t
 
-@[inherit_doc normExprImp]
-abbrev normExprCore (s : FVarSubst) (e : Expr) (translator : Bool) : Expr :=
+@[inherit_doc normExprImp, inline]
+def normExprCore (s : FVarSubst) (e : Expr) (translator : Bool) : Expr :=
   normExprImp s e translator
 
 /--

src/Lean/Compiler/LCNF/ConfigOptions.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Data.Options
+public import Lean.Data.Options
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/DeclHash.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 
@@ -42,10 +46,10 @@ private partial def depOn (c : Code) : M Bool :=
   | .return fvarId => fvarDepOn fvarId
   | .unreach _ => return false
 
-abbrev LetDecl.dependsOn (decl : LetDecl) (s : FVarIdSet) :  Bool :=
+@[inline] def LetDecl.dependsOn (decl : LetDecl) (s : FVarIdSet) :  Bool :=
   decl.depOn s
 
-abbrev FunDecl.dependsOn (decl : FunDecl) (s : FVarIdSet) :  Bool :=
+@[inline] def FunDecl.dependsOn (decl : FunDecl) (s : FVarIdSet) :  Bool :=
   typeDepOn decl.type s || depOn decl.value s
 
 def CodeDecl.dependsOn (decl : CodeDecl) (s : FVarIdSet) : Bool :=

src/Lean/Compiler/LCNF/ElimDead.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.InferType
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -3,15 +3,19 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Zwarich
 -/
+module
+
 prelude
-import Lean.Compiler.ClosedTermCache
-import Lean.Compiler.NeverExtractAttr
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.Internalize
-import Lean.Compiler.LCNF.MonoTypes
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.ToExpr
+public import Lean.Compiler.ClosedTermCache
+public import Lean.Compiler.NeverExtractAttr
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.ToExpr
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace ExtractClosed

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Expr
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Expr
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/FixedParams.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
-import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Types
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace FixedParams

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.FVarUtil
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.FVarUtil
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.Types
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/InferType.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.OtherDecl
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.OtherDecl
+
+public section
 
 namespace Lean.Compiler.LCNF
 /-! # Type inference for LCNF -/

src/Lean/Compiler/LCNF/Internalize.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.Bind
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.Bind
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -3,13 +3,17 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.PullFunDecls
-import Lean.Compiler.LCNF.FVarUtil
-import Lean.Compiler.LCNF.ScopeM
-import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PullFunDecls
+public import Lean.Compiler.LCNF.FVarUtil
+public import Lean.Compiler.LCNF.ScopeM
+public import Lean.Compiler.LCNF.InferType
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/LCtx.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.LocalContext
-import Lean.Compiler.LCNF.Basic
+public import Lean.LocalContext
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -3,15 +3,19 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Meta.Instances
-import Lean.Compiler.InlineAttrs
-import Lean.Compiler.LCNF.Closure
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.MonadScope
-import Lean.Compiler.LCNF.Internalize
-import Lean.Compiler.LCNF.Level
-import Lean.Compiler.LCNF.AuxDeclCache
+public import Lean.Meta.Instances
+public import Lean.Compiler.InlineAttrs
+public import Lean.Compiler.LCNF.Closure
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.MonadScope
+public import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.Level
+public import Lean.Compiler.LCNF.AuxDeclCache
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace LambdaLifting

src/Lean/Compiler/LCNF/Level.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Util.CollectLevelParams
-import Lean.Compiler.LCNF.Basic
+public import Lean.Util.CollectLevelParams
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Main.lean

@@ -3,23 +3,27 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.Options
-import Lean.Compiler.ExternAttr
-import Lean.Compiler.IR
-import Lean.Compiler.IR.Basic
-import Lean.Compiler.IR.Checker
-import Lean.Compiler.IR.ToIR
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.Passes
-import Lean.Compiler.LCNF.PrettyPrinter
-import Lean.Compiler.LCNF.ToDecl
-import Lean.Compiler.LCNF.Check
-import Lean.Compiler.LCNF.PullLetDecls
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.CSE
+public import Lean.Compiler.Options
+public import Lean.Compiler.ExternAttr
+public import Lean.Compiler.IR
+public import Lean.Compiler.IR.Basic
+public import Lean.Compiler.IR.Checker
+public import Lean.Compiler.IR.ToIR
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.Passes
+public import Lean.Compiler.LCNF.PrettyPrinter
+public import Lean.Compiler.LCNF.ToDecl
+public import Lean.Compiler.LCNF.Check
+public import Lean.Compiler.LCNF.PullLetDecls
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.CSE
 public import Lean.Compiler.LCNF.Visibility
 
+public section
+
 namespace Lean.Compiler.LCNF
 /--
 We do not generate code for `declName` if
@@ -92,9 +96,11 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   for declName in declNames do
     if let some fnName := Compiler.getImplementedBy? (← getEnv) declName then
       if !isDeclPublic (← getEnv) fnName then
-        if let some decl ← getLocalDecl? fnName then
+        if let some decl ← getLocalDeclAt? fnName .base then
           trace[Compiler.inferVisibility] m!"Marking {fnName} as opaque because it implements {declName}"
           LCNF.markDeclPublicRec .base decl
+          if let some decl ← getLocalDeclAt? fnName .mono then
+            LCNF.markDeclPublicRec .mono decl
   let declNames ← declNames.filterM (shouldGenerateCode ·)
   if declNames.isEmpty then return #[]
   for declName in declNames do

src/Lean/Compiler/LCNF/MonadScope.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Basic
+public import Lean.Compiler.LCNF.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 
@@ -38,4 +42,4 @@ def inScope [MonadScope m] [Monad m] (fvarId : FVarId) : m Bool :=
 @[inline] def withNewScope [MonadScope m] [Monad m] (x : m α) : m α := do
   withScope (fun _ => {}) x
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Meta.InferType
-import Lean.Compiler.LCNF.Util
-import Lean.Compiler.LCNF.BaseTypes
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Meta.InferType
+public import Lean.Compiler.LCNF.Util
+public import Lean.Compiler.LCNF.BaseTypes
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/OtherDecl.lean

@@ -3,9 +3,13 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.BaseTypes
-import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.BaseTypes
+public import Lean.Compiler.LCNF.MonoTypes
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/PassManager.lean

@@ -3,15 +3,19 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Attributes
-import Lean.Environment
-import Lean.Meta.Basic
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Attributes
+public import Lean.Environment
+public import Lean.Meta.Basic
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 
-def Phase.toNat : Phase → Nat
+@[expose] def Phase.toNat : Phase → Nat
   | .base => 0
   | .mono => 1
 

src/Lean/Compiler/LCNF/Passes.lean

@@ -3,24 +3,28 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.PullLetDecls
-import Lean.Compiler.LCNF.CSE
-import Lean.Compiler.LCNF.Simp
-import Lean.Compiler.LCNF.PullFunDecls
-import Lean.Compiler.LCNF.ReduceJpArity
-import Lean.Compiler.LCNF.JoinPoints
-import Lean.Compiler.LCNF.Specialize
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.ToMono
-import Lean.Compiler.LCNF.LambdaLifting
-import Lean.Compiler.LCNF.FloatLetIn
-import Lean.Compiler.LCNF.ReduceArity
-import Lean.Compiler.LCNF.ElimDeadBranches
-import Lean.Compiler.LCNF.StructProjCases
-import Lean.Compiler.LCNF.ExtractClosed
-import Lean.Compiler.LCNF.Visibility
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PullLetDecls
+public import Lean.Compiler.LCNF.CSE
+public import Lean.Compiler.LCNF.Simp
+public import Lean.Compiler.LCNF.PullFunDecls
+public import Lean.Compiler.LCNF.ReduceJpArity
+public import Lean.Compiler.LCNF.JoinPoints
+public import Lean.Compiler.LCNF.Specialize
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.ToMono
+public import Lean.Compiler.LCNF.LambdaLifting
+public import Lean.Compiler.LCNF.FloatLetIn
+public import Lean.Compiler.LCNF.ReduceArity
+public import Lean.Compiler.LCNF.ElimDeadBranches
+public import Lean.Compiler.LCNF.StructProjCases
+public import Lean.Compiler.LCNF.ExtractClosed
+public import Lean.Compiler.LCNF.Visibility
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PassManager
+
+public section
 
 namespace Lean.Compiler.LCNF
 
@@ -91,7 +95,7 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
 
-def DeclExt := PersistentEnvExtension Decl Decl DeclExtState
+@[expose] def DeclExt := PersistentEnvExtension Decl Decl DeclExtState
 
 instance : Inhabited DeclExt :=
   inferInstanceAs (Inhabited (PersistentEnvExtension Decl Decl DeclExtState))
@@ -163,11 +167,14 @@ def getDeclAt? (declName : Name) (phase : Phase) : CoreM (Option Decl) :=
 def getDecl? (declName : Name) : CompilerM (Option Decl) := do
   getDeclAt? declName (← getPhase)
 
-def getLocalDecl? (declName : Name) : CompilerM (Option Decl) := do
-  match (← getPhase) with
+def getLocalDeclAt? (declName : Name) (phase : Phase) : CompilerM (Option Decl) := do
+  match phase with
   | .base => return baseExt.getState (← getEnv) |>.find? declName
   | .mono => return monoExt.getState (← getEnv) |>.find? declName
 
+def getLocalDecl? (declName : Name) : CompilerM (Option Decl) := do
+  getLocalDeclAt? declName (← getPhase)
+
 def getExt (phase : Phase) : DeclExt :=
   match phase with
   | .base => baseExt

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.PrettyPrinter.Delaborator.Options
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.Internalize
+public import Lean.PrettyPrinter.Delaborator.Options
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Internalize
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Probing.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.PassManager
-import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PhaseExt
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/PullFunDecls.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.DependsOn
-import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.DependsOn
+public import Lean.Compiler.LCNF.PassManager
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace PullFunDecls

src/Lean/Compiler/LCNF/PullLetDecls.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.DependsOn
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.DependsOn
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.PassManager
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace PullLetDecls

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.PhaseExt
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.Internalize
+
+public section
 
 namespace Lean.Compiler.LCNF
 /-!

src/Lean/Compiler/LCNF/ReduceJpArity.lean

@@ -3,10 +3,14 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.PassManager
+
+public section
 
 namespace Lean.Compiler.LCNF
 /-!

src/Lean/Compiler/LCNF/Renaming.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 /--

src/Lean/Compiler/LCNF/ScopeM.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 

src/Lean/Compiler/LCNF/Simp.lean

@@ -3,20 +3,24 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.ReduceJpArity
-import Lean.Compiler.LCNF.Renaming
-import Lean.Compiler.LCNF.Simp.Basic
-import Lean.Compiler.LCNF.Simp.FunDeclInfo
-import Lean.Compiler.LCNF.Simp.JpCases
-import Lean.Compiler.LCNF.Simp.Config
-import Lean.Compiler.LCNF.Simp.InlineCandidate
-import Lean.Compiler.LCNF.Simp.SimpM
-import Lean.Compiler.LCNF.Simp.Main
-import Lean.Compiler.LCNF.Simp.InlineProj
-import Lean.Compiler.LCNF.Simp.DefaultAlt
-import Lean.Compiler.LCNF.Simp.SimpValue
-import Lean.Compiler.LCNF.Simp.Used
+public import Lean.Compiler.LCNF.ReduceJpArity
+public import Lean.Compiler.LCNF.Renaming
+public import Lean.Compiler.LCNF.Simp.Basic
+public import Lean.Compiler.LCNF.Simp.FunDeclInfo
+public import Lean.Compiler.LCNF.Simp.JpCases
+public import Lean.Compiler.LCNF.Simp.Config
+public import Lean.Compiler.LCNF.Simp.InlineCandidate
+public import Lean.Compiler.LCNF.Simp.SimpM
+public import Lean.Compiler.LCNF.Simp.Main
+public import Lean.Compiler.LCNF.Simp.InlineProj
+public import Lean.Compiler.LCNF.Simp.DefaultAlt
+public import Lean.Compiler.LCNF.Simp.SimpValue
+public import Lean.Compiler.LCNF.Simp.Used
+
+public section
 
 namespace Lean.Compiler.LCNF
 open Simp

src/Lean/Compiler/LCNF/Simp/Basic.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Meta.Instances
-import Lean.Compiler.InlineAttrs
-import Lean.Compiler.Specialize
-import Lean.Compiler.LCNF.CompilerM
+public import Lean.Meta.Instances
+public import Lean.Compiler.InlineAttrs
+public import Lean.Compiler.Specialize
+public import Lean.Compiler.LCNF.CompilerM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/Config.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Init.Core
+public import Init.Core
+
+public section
 namespace Lean.Compiler.LCNF
 namespace Simp
 

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
-import Init.Data.UInt.Log2
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.PassManager
+public import Init.Data.UInt.Log2
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.PassManager
+
+public section
 
 namespace Lean.Compiler.LCNF.Simp
 namespace ConstantFold

src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Simp.SimpM
+public import Lean.Compiler.LCNF.Simp.SimpM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -3,11 +3,15 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.CompilerM
-import Lean.Compiler.LCNF.Types
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.Simp.Basic
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Types
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.Simp.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/FunDeclInfo.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Simp.Basic
+public import Lean.Compiler.LCNF.Simp.Basic
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Simp.SimpM
+public import Lean.Compiler.LCNF.Simp.SimpM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/InlineProj.lean

@@ -3,8 +3,12 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.Simp.SimpM
+public import Lean.Compiler.LCNF.Simp.SimpM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -3,12 +3,16 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.LCNF.DependsOn
-import Lean.Compiler.LCNF.InferType
-import Lean.Compiler.LCNF.Internalize
-import Lean.Compiler.LCNF.Simp.Basic
-import Lean.Compiler.LCNF.Simp.DiscrM
+public import Lean.Compiler.LCNF.DependsOn
+public import Lean.Compiler.LCNF.InferType
+public import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.Simp.Basic
+public import Lean.Compiler.LCNF.Simp.DiscrM
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -3,19 +3,23 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.ImplementedByAttr
-import Lean.Compiler.LCNF.ElimDead
-import Lean.Compiler.LCNF.AlphaEqv
-import Lean.Compiler.LCNF.PrettyPrinter
-import Lean.Compiler.LCNF.Bind
-import Lean.Compiler.LCNF.Simp.FunDeclInfo
-import Lean.Compiler.LCNF.Simp.InlineCandidate
-import Lean.Compiler.LCNF.Simp.InlineProj
-import Lean.Compiler.LCNF.Simp.Used
-import Lean.Compiler.LCNF.Simp.DefaultAlt
-import Lean.Compiler.LCNF.Simp.SimpValue
-import Lean.Compiler.LCNF.Simp.ConstantFold
+public import Lean.Compiler.ImplementedByAttr
+public import Lean.Compiler.LCNF.ElimDead
+public import Lean.Compiler.LCNF.AlphaEqv
+public import Lean.Compiler.LCNF.PrettyPrinter
+public import Lean.Compiler.LCNF.Bind
+public import Lean.Compiler.LCNF.Simp.FunDeclInfo
+public import Lean.Compiler.LCNF.Simp.InlineCandidate
+public import Lean.Compiler.LCNF.Simp.InlineProj
+public import Lean.Compiler.LCNF.Simp.Used
+public import Lean.Compiler.LCNF.Simp.DefaultAlt
+public import Lean.Compiler.LCNF.Simp.SimpValue
+public import Lean.Compiler.LCNF.Simp.ConstantFold
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp

src/Lean/Compiler/LCNF/Simp/SimpM.lean

@@ -3,18 +3,22 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
-import Lean.Compiler.ImplementedByAttr
-import Lean.Compiler.LCNF.Renaming
-import Lean.Compiler.LCNF.ElimDead
-import Lean.Compiler.LCNF.AlphaEqv
-import Lean.Compiler.LCNF.PrettyPrinter
-import Lean.Compiler.LCNF.Bind
-import Lean.Compiler.LCNF.Internalize
-import Lean.Compiler.LCNF.Simp.JpCases
-import Lean.Compiler.LCNF.Simp.DiscrM
-import Lean.Compiler.LCNF.Simp.FunDeclInfo
-import Lean.Compiler.LCNF.Simp.Config
+public import Lean.Compiler.ImplementedByAttr
+public import Lean.Compiler.LCNF.Renaming
+public import Lean.Compiler.LCNF.ElimDead
+public import Lean.Compiler.LCNF.AlphaEqv
+public import Lean.Compiler.LCNF.PrettyPrinter
+public import Lean.Compiler.LCNF.Bind
+public import Lean.Compiler.LCNF.Internalize
+public import Lean.Compiler.LCNF.Simp.JpCases
+public import Lean.Compiler.LCNF.Simp.DiscrM
+public import Lean.Compiler.LCNF.Simp.FunDeclInfo
+public import Lean.Compiler.LCNF.Simp.Config
+
+public section
 
 namespace Lean.Compiler.LCNF
 namespace Simp