Ed's question barrage

Stream: general

[Edward Ayers]

Massive thanks to @Mario Carneiro for helping me. I'll buy you beers next time we are in the same physical location to within 100m.

[Edward Ayers]

In the constructor for mvar for expr, are the arguments pretty name, unique name, type? You said that local_consts type argument shouldn't be trusted because its sometimes a placeholder. Is that true for mvars type arg too?

[Edward Ayers]

Also in expr what is macro used for?

[Edward Ayers]

Are they macros in the same sense as C macros?

[Mario Carneiro]

I am not sure about the reliability of mvar types; they aren't found in the local context so probably that's the only place the data is stored, meaning it has to be reliable

[Mario Carneiro]

still, infer_type should always work

[Mario Carneiro]

expr.macro is a C++ thing. Those are basically "promises" to build an expr by some C++ code, you can't build them in lean

[Mario Carneiro]

You can unfold a macro and force it to evaluate

[Mario Carneiro]

They are used for sorry, meta recursive calls (which are not compiled to recursors like the non-meta versions), builtin projections, and they also are ephemeral structures in some specialized tactics

[Edward Ayers]

What are some examples of meta recursive calls?

[Mario Carneiro]

meta def rec := rec

[Mario Carneiro]

meta def rec : nat -> nat | x := rec (x + 1)

[Edward Ayers]

What is a builtin projection?

[Mario Carneiro]

structure foo := (mynat : ℕ)
#print foo.mynat

-- @[reducible]
-- def foo.mynat : foo → ℕ :=
-- λ (c : foo), [foo.mynat c]

the thing in brackets is a macro

[Edward Ayers]

cool

[Edward Ayers]

I am reading decalaration.lean. And I came across

Reducibility hints are used in the convertibility checker.
When trying to solve a constraint such a

       (f ...) =?= (g ...)

where f and g are definitions, the checker has to decide which one will be unfolded.
If f (g) is opaque, then g (f) is unfolded if it is also not marked as opaque,
Else if f (g) is abbrev, then f (g) is unfolded if g (f) is also not marked as abbrev,
Else if f and g are regular, then we unfold the one with the biggest definitional height.
Otherwise both are unfolded.

Is there a way I can get programmatic access to the "definitional height" of a declaration (other than expanding it and calculating it myself)?

[Edward Ayers]

Ah it's an argument to regular

[Edward Ayers]

sorry was on the next line.

[Edward Ayers]

So to get the definitional height you would do

env <- tactic.get_env
defn _ _ _ _ (regular h _ _) _  <- environment.get env my_name
return h

[Edward Ayers]

Is the convertability checker the same thing as the unifier?

[Edward Ayers]

What's the best way of adding some arbitrary data to the environment?. Eg, I've calculated a table for a tactic and I don't want to regenerate this table for every invocation of the tactic, I just want to retrieve it from the environment somehow.

[Mario Carneiro]

You can make a def containing the data

[Edward Ayers]

makes sense.

[Edward Ayers]

That is so much more straightforward than the Isabelle way!

[Mario Carneiro]

your ability to store arbitrary data in the environment is limited; for the most part it's just exprs

[Mario Carneiro]

Ideally you would want to store any vm_obj in the environment, but I don't know any way to do that besides reflecting it to an expr

[Edward Ayers]

I'd make a def with mk_local_def right?

[Mario Carneiro]

no, that's for local constants

[Edward Ayers]

add_meta_definition?

[Mario Carneiro]

oh, I didn't know that one was there, that's useful

[Mario Carneiro]

yes

[Edward Ayers]

When I reflect to an expr, that means it actually has to build an expr tree which represents the data in some way right? It sounds like one would get performance issues if you wanted to save a gigantic rewrite table or similar.

[Mario Carneiro]

The simp_lemmas data structure is designed for handling big rewrite tables

[Mario Carneiro]

You can cache data in special types inside user attributes as well

[Edward Ayers]

simp_lemmas looks good but I can only access the data through calls to simp_lemmas.rewrite so I am stuck with simps implementation. Not necessarily a showstopper but I can't retrieve arbitrary exprs from it.

[Edward Ayers]

Please could you give some examples of this?

You can cache data in special types inside user attributes as well

[Mario Carneiro]

I'm referring to the cache_ty and param_ty in user_attribute, but it's not really a solution - param_ty has to be reflectable (so it is probably just stored as an expr) and cache_ty needs to be pure-functionally created from the list of all defs with the attribute in the environment (so it can only depend on things that are ultimately exprs). Still that cache has some promise

[Mario Carneiro]

I'm not positive this is actually working the way you would want, but here's the general idea:

structure mydata := (n : nat)

@[user_attribute]
meta def mydata_attr : user_attribute (name_map mydata) unit :=
{ name := `mydata, descr := "stuff",
  cache_cfg := ⟨λ l, l.mfoldl (λ m n, do
    d ← get_decl n,
    v ← eval_expr mydata d.value,
    return (m.insert n v)) (name_map.mk _), []⟩ }

@[mydata] def X : mydata := ⟨500^2⟩

run_cmd do
  m ← mydata_attr.get_cache,
  v ← m.find ``X,
  trace v.n

[Edward Ayers]

• In pexpr, has it already disambiguated overloaded operators such as +

[Edward Ayers]

• is the process pexpr -> expr called "elaboration"?

[Edward Ayers]

• Filling in the implicit arguments of a pexpr is the same problem as finding a proof. So does it make sense to think of the process pexpr -> expr as a kind of tactic driven by the structure of the pexpr?

[Edward Ayers]

• It seems that you can't do pexpr -> expr without recursively infering the types of the subpexprs of the pexpr. Is this right? In which case why not cache all of the types and then you never have to call infer_type? My guess would be that it would take up too much space.

[Edward Ayers]

• Why does the eval_expr α e tactic need to be given the type of e as well?

[Edward Ayers]

• Is the target tactic the same as get_goals >>= (list.head >> return)?

[Edward Ayers]

• The definition of intro is

meta def intro (n : name) : tactic expr :=
do t ← target,
   if expr.is_pi t ∨ expr.is_let t then intro_core n
   else whnf_target >> intro_core n

But I can't figure out what I am doing wrong in the last two examples below:

example : a -> b -> a :=
begin
    intro hello,
    sorry
end

example : a -> b -> a :=
begin
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

example : a -> b -> a :=
begin
    whnf_target,
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

[Edward Ayers]

• Does get_unused_name n just check if n is currently being used, and if not, sticks an _1/ _2/... on the end?

[Edward Ayers]

• If I invoke local_context, will that always be a list of local_consts or are there ways of getting other forms of expr in the context?

[Rob Lewis]

I can try to save Mario some time and answer a few of these....

• In pexpr, has it already disambiguated overloaded operators such as +

No. But note that + isn't "overloaded," exactly. + is notation for has_add.add which applies to any type with a has_add type class instance. A pexpr using + hasn't filled in the implicit type or the instance yet. And for notation that really is overloaded, a pexpr will represent the ambiguity with a macro, I think.

[Rob Lewis]

• is the process pexpr -> expr called "elaboration"?

Yes.

[Rob Lewis]

• Filling in the implicit arguments of a pexpr is the same problem as finding a proof. So does it make sense to think of the process pexpr -> expr as a kind of tactic driven by the structure of the pexpr?

Yeah, I guess. Notice the tactic to_expr does exactly this.

[Rob Lewis]

• It seems that you can't do pexpr -> expr without recursively infering the types of the subpexprs of the pexpr. Is this right? In which case why not cache all of the types and then you never have to call infer_type? My guess would be that it would take up too much space.

Are you asking why each expr object doesn't store its type? Yeah, this would take up a huge amount of space.

[Rob Lewis]

• Why does the eval_expr α e tactic need to be given the type of e as well?

I'm not 100% clear on how eval_expr works, but here's my intuition, anyway. If you didn't give the expected type, you'd have to "guess" it by inferring the type of e, which would give you an expr, not a type. You need a way to go from this expr to a type, which is why you have the [reflected α] instance.

[Kevin Buzzard]

example : a -> b -> a :=
begin
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

[Rob Lewis]

• Is the target tactic the same as get_goals >>= (list.head >> return)?

I think, roughly. It's the type of the first goal metavariable.

[Rob Lewis]

• The definition of intro is

meta def intro (n : name) : tactic expr :=
do t ← target,
   if expr.is_pi t ∨ expr.is_let t then intro_core n
   else whnf_target >> intro_core n

But I can't figure out what I am doing wrong in the last two examples below:

example : a -> b -> a :=
begin
    intro hello,
    sorry
end

example : a -> b -> a :=
begin
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

example : a -> b -> a :=
begin
    whnf_target,
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

You've noticed the difference between the tactic monad and "interactive mode." When you're using tactics for proofs, in begin/end blocks, they get parsed differently than when you're writing tactics. The intro in begin/end is actually tactic.interactive.intro.

[Edward Ayers]

I think, roughly. It's the type of the first goal metavariable.

The docs for target confused me because they say it returns the "main goal" but this seems to always be the first goal.

[Rob Lewis]

intro_core isn't an interactive tactic. It expects a name, which you'd have to give in the form `hello .

[Rob Lewis]

tactic.intro expects the same. tactic.interactive.intro expects some text to follow that it will parse into a name.

[Kevin Buzzard]

example : a -> b -> a :=
begin
    intro_core hello, -- errors here "unknown identifier 'hello'"
    sorry
end

The intro in a begin end block is tactic.interactive.intronot tactic.intro. I don't know if this helps or whether you're already way ahead of this, but it was something that confused me for a while.

PS just beaten to it by Rob :-)

[Mario Carneiro]

the "main goal" is the first goal

[Rob Lewis]

• If I invoke local_context, will that always be a list of local_consts or are there ways of getting other forms of expr in the context?

I think it's only local_const exprs, yes.

[Rob Lewis]

• Does get_unused_name n just check if n is currently being used, and if not, sticks an _1/ _2/... on the end?

This one I'm not sure, I've never really paid attention. It will give you a name that starts with n that won't conflict with anything.

[Mario Carneiro]

Why does the eval_expr α e tactic need to be given the type of e as well?

This is done for typechecking purposes. You are given e which is an expr, but you want to return something of type α. What is α? You would need to have a function e.type : expr -> Type to define "the type of e", but that doesn't work because of universe issues. So instead you just assert the type you want and lean checks it (I think, maybe it just crashes if you got it wrong)

[Kevin Buzzard]

could has_one.one be an example of an expr? Or some such thing? I'm wondering when Lean decides that 1 should be a natural if it can't think of any better ideas.

[Mario Carneiro]

has_one.one has a big pi type, but `(has_one.one) is an expr

[Rob Lewis]

I think it's specifically numerals that default to nat if there's no other information, right? This happens at elaboration time.

[Edward Ayers]

What's the best way to discover if expr e has form Exists (a : A), B a? Or alternatively Exists p?

[Simon Hudon]

One simple way is to do:

do `(Exists %%p) <- pure e | fail "e is in bad shape",
       -- do stuff with `p`

[Edward Ayers]

• Am I right in thinking that rbtree doesn't come with function to remove items from it?

[Mario Carneiro]

I... guess you're right

[Mario Carneiro]

that's a bit annoying, I was hoping not to have to touch rbtree

[Edward Ayers]

Could I use rb_map, which does have this?

[Edward Ayers]

If I do a <|> b for the option type, will the VM not evaluate b if a is some _?

[Edward Ayers]

Is anyone doing 23 trees in mathlib?

[Edward Ayers]

I've started coding it up

[Kevin Buzzard]

Is it maths?

[Edward Ayers]

It's a datastructure

[Edward Ayers]

like rbtree

[Edward Ayers]

Is there a way to have conditionals in match statements? Eg something like:

match x with
|(some y)  where  y > 5 := "hello"
|_ := "nope"
end

[Simon Hudon]

"nope"

[Simon Hudon]

No conditions built into match

[Mario Carneiro]

If I do a <|> b for the option type, will the VM not evaluate b if a is some _?

It will evaluate both sides, unless option.orelse is inlined. If you want to avoid this, you can make an option.orelse' that takes a thunk (option A) for its second argument

[Mario Carneiro]

Is anyone doing 23 trees in mathlib? I've started coding it up

I have no current plans for this, go ahead. We would be happy to take it

[Mario Carneiro]

Is there a way to have conditionals in match statements?

No, as Simon said; although in this case you can write the following:

match x with
| (some (y+6)) := "hello"
| _ := "nope"
end

I would recommend just using if though.

[Patrick Massot]

What if he gets tired towards the middle of the task, and ends up with 11 trees instead of 23?

[Simon Hudon]

That's a linked list. We won't be so welcoming because we have those.

[Patrick Massot]

Damn it. What was the probability that roughly cutting in half the number 23 would lead to another meaningful sentence?

[Simon Hudon]

Btw, why do we want 2-3 trees while we have red-back trees? What do you get from 2-3 trees that you don't get from red-black trees?

[Mario Carneiro]

I guess with 12 trees he will have a trie

[Mario Carneiro]

different performance characteristics... I'm okay with implementing datastructures for their own sake because of this

[Mario Carneiro]

but it's true that rb trees already implement the same API as it were, so if you are a programmer who needs a map type and doesn't want to bother with writing data structures you can use them instead

[Simon Hudon]

As I understand it, a red-black tree is basically a 2-3 tree where the balancing invariant is formulated in terms of tree height instead of node degree, that's why I'm surprised it would get a different performance profile

[Mario Carneiro]

From https://www.cs.purdue.edu/homes/ayg/CS251/slides/chap13b.pdf , it seems like 2-3 trees or 2-3-4 trees are actually just simpler versions of rb trees

[Mario Carneiro]

the advantage of rb trees is normalizing the node layout, but this doesn't matter when you are writing inductives in lean

[Sebastian Ullrich]

Huh, that's an interesting slide format

[Kevin Buzzard]

Huh, that's an interesting slide format

Judging by the name of the pdf, this might be a chapter from a book, and books are still traditionally in portrait format I guess.

[Gabriel Ebner]

Those are definitely slides, but more like old-school ones for overhead projectors.

[Patrick Massot]

Maybe Sebastian was referring to the Batman delirium at the end

[Edward Ayers]

Yes I'm just treating making 23 trees as another exercise. I copied the implementation details from Isabelle and then added dependent types to it. I managed to prove that my trees are balanced using just dependent types (each node has a height param in its type). It was fun to see that it worked and I learned a lot. I made no considerations for performance so rbtree is still better and more concise. The deletion algo for 23 trees is horrifying so there is likely a mistake in there, but at least I proved that it's balanced!

Here is a link to the source but I've made no attempt to make it readable yet. I haven't even tested it.
https://github.com/EdAyers/mathlib/blob/tree23/data/tree23.lean

Some thoughts from doing this,
- It can be difficult to decide which typeclasses to use. Should I use linear_order? decidable_rel? And so on.
- The coercions from decidable to if statements are kind of magical.
- There is a lemma lt_min_key_imp_outside which I basically did by taking a random walk through the space of valid tactics until no goals appeared. Any tips on how this can be tightened up would be appreciated.
- Proving anything about the del method will be a nightmare. So if the deletion method for rb trees is simpler then I am happy to abandon these.
- The main thing I learnt is that you are much better off using non-dependent-type driven datatypes and then restricting with propositions at the end. Using dependent types just makes coding too tedious.

[Edward Ayers]

I also had an attempt at proving some things about rbtrees but it is very tedious. I think that I am not using the automation very effectively.

[Edward Ayers]

I'm going to use native.rb_tree in the future instead, but I don't regret implementing this because it taught me a lot about Lean.

[Edward Ayers]

My dream was that I wouldn't have to write tests for my code, because I could just prove that it is correct!

[Simon Hudon]

Have you put your code somewhere on github. We can look at it to see if we can make your proving more effective

[Edward Ayers]

yes see link above in this thread

[Edward Ayers]

https://github.com/EdAyers/mathlib/blob/tree23/data/tree23.lean

[Edward Ayers]

I'll push the rbtree experiments in a few hours.

[Edward Ayers]

Why is it that #check λ x, x + 1 is ℕ → ℕ and not [has_add ?m] [has_one ?m] ?m -> ?m

[Edward Ayers]

What is causing the elaborator to default to nat?

[Bryan Gin-ge Chen]

(deleted)

[Kenny Lau]

I think 1 is default to nat

[Edward Ayers]

Right but where is the defaultness set?

[Kevin Buzzard]

At some point in the elaboration process, Lean sometimes says "if I can't figure out what that 1 is, I'm going to assume it's a nat". I think the point this occurs is near the end, if at all. Maybe you can even concoct something where example behaves differently to definition using this sort of thing.

[Kevin Buzzard]

(deleted nonsense)

[Edward Ayers]

Perhaps 1 is always nat, and there is a type coercion from nat to all of the other kinds of numbers?

[Kevin Buzzard]

That's not how it works, I'm pretty sure.

[Kevin Buzzard]

Unfortunately, as I found out earlier this week, it's very difficult to switch the number literal parser off.

[Kevin Buzzard]

1 is has_one.one

[Edward Ayers]

The thing I can't figure out is if the nat default is set somewhere in init or whether it is baked in to the elaborator.

[Kevin Buzzard]

I think it is baked into the elaborator. I think that #check cannot possibly return [has_add ?m] [has_one ?m] ... because I don't think Lean thinks these are part of the expression.

[Kevin Buzzard]

So eventually it gets to a point where it can't figure out where this type class inference thing is coming from and at that point it decides it's going to go for nat. You should check all this with an expert.

[Mario Carneiro]

The nat default is baked into the elaborator, but it is not necessary for it to operate

[Mario Carneiro]

it could just as easily return ?m -> ?m, and there would be (hidden) subgoals for those typeclasses

[Mario Carneiro]

Perhaps 1 is always nat, and there is a type coercion from nat to all of the other kinds of numbers?

Lean used to work like this, but the current version uses a polymorphic 1 function

[Mario Carneiro]

I find the nat default distateful precisely because it's the only thing about lean definitions which is not configured within lean

[Mario Carneiro]

if kevin decided to write his own core.lean with xnat, lean would probably complain

[Mario Carneiro]

https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L3609-L3610

[Edward Ayers]

I can see why Leo did this though, since nat is initial with respect to has_one and has_add so you don't really lose any generality by doing this and 90% of the time you mean nat anyway.

[Mario Carneiro]

note again that lean does not use anything like nat.cast to get an arbitrary value of type A from a nat

[Mario Carneiro]

If you type 4 : A, it is translated by the parser to bit0 (bit0 1), where bit0 and has_one.one are polymorphic functions

[Mario Carneiro]

this term will make absolutely no reference to nat

[Mario Carneiro]

The reason this was done, I believe, is that without a default type being assigned as a last resort, you can never write a numeral without a type ascription somewhere, so a beginner will type #eval 2 + 2 and get a weird error message instead of the obvious answer

[Edward Ayers]

What is the difference between synthesizing and elaborating?

[Edward Ayers]

My guess is synthesizing is when the elaborator tries to guess an expr for a given type sig

[Mario Carneiro]

I'm not sure there is a difference, they are both fairly general terms

[Mario Carneiro]

elaboration is broadly the process of taking a parsed pre-expression, an AST, and including and inferring all missing type information to make it a valid term of the formal logic

[Mario Carneiro]

synthesis is just what you call putting data into one of these holes

[Edward Ayers]

Ok. So when you make the proof to a lemma by writing out a proof term. Making that a valid expr is elaboration. Does the process of making a valid proof term using begin ... end also count as elaboration?

[Mario Carneiro]

There are multiple methods used by the elaborator to synthesize expressions, but the major workhorses are unification and typeclass inference

[Mario Carneiro]

I'm not sure I would call tactic evaluation a part of elaboration, but it occurs in the middle of the elaboration cycle, yes

[Mario Carneiro]

you could view the tactic framework as a giant plugin to the elaborator

[Edward Ayers]

Yes that's how I'm viewing it. It's a beautiful way of doing it.

[Edward Ayers]

When I write def asdf (myarg : mytype . mytactic) : ... := .... I can't quite figure out what the tactic is doing. Is Lean making a tactic state with the goal as mytype and myarg as a local constant?

[Edward Ayers]

So I use this by writing asdf (myvalue). Or is the idea that the mytactic should be used to synthesize myarg if it is not provided explicitly?

[Edward Ayers]

Also, expr has the argument elaborated := tt. I am guessing that expr tt is a term that has been elaborated, and hence is valid. Whereas a expr ff has not been checked to be valid, eg I just made a nonsense term myself from the expr constructors. So expr ff/expr tt is like term/cterm in Isabelle.

[Edward Ayers]

But then I can make expr tt from the expr constructors too, so that can't be it.

[Edward Ayers]

But in that case I can't see what the difference could be between expr tt and expr ff.

[Mario Carneiro]

Or is the idea that the mytactic should be used to synthesize myarg if it is not provided explicitly?

this

[Mario Carneiro]

it is a variant on optional parameters where the default value is synthesized by a tactic

[Mario Carneiro]

Whereas a expr ff has not been checked to be valid, eg I just made a nonsense term myself from the expr constructors.

Not quite. expr ff is the same as pexpr, and it represents those pre-expressions I mentioned

[Edward Ayers]

So an expr ff can have wildcard holes in it?

[Mario Carneiro]

They actually differ from expr structurally, i.e. if I write x + y then the pexpr for this is has_add.add x y with 2 arguments, and the expr is has_add.add ?m1 ?m2 x y or has_add.add nat nat.has_add x y with 4 arguments

[Edward Ayers]

nice

[Mario Carneiro]

they could have been defined as separate inductive types, but they share enough of the major structure that it seemed redundant

[Mario Carneiro]

lean 4 will have these separate, with pexpr becoming syntax which is completely different

[Mario Carneiro]

it will be much more like an AST for lean

[Edward Ayers]

Ah I just found @[reducible] meta def pexpr := expr ff in source

[Edward Ayers]

meta constant pexpr.mk_placeholder : pexpr seems to be the magic constant that lets you do placeholders. You can't use metavariables because you might not be in a tactic monad so you can't make fresh ones.

[Mario Carneiro]

mk_placeholder is basically the AST corresponding to _ as a token

[Edward Ayers]

Am I right in thinking that the placeholder is distinct from metavars, but elaborating a pexpr turns these into metavars?

[Mario Carneiro]

there is only one, and it is elaborated to a new metavariable every time

[Edward Ayers]

Will the elaborator for Lean 4 be written in Lean rather than C++?

[Mario Carneiro]

parser yes, elaborator maybe

[Edward Ayers]

That would blow my mind

[Mario Carneiro]

I think the idea is to completely self host

[Edward Ayers]

I can't wait for Lean 4

[Mario Carneiro]

but it's hard, not the least because the lean VM is currently not efficient enough to support this

[Mario Carneiro]

so they will need to implement a real lean compiler to machine code

[Edward Ayers]

To do the elaborator in Lean you would need some kind of super simple bootstrap elaborator in C++ with everything explicit and build up from there.

[Mario Carneiro]

even in core lean for much of the files you don't have the tactic framework set up yet so it's all explicit terms

[Mario Carneiro]

I don't know exactly how the full bootstrap process would work, it might just run itself on the previous version of lean to avoid messy business

[Edward Ayers]

Right but then you can't build Lean from scratch which would be sad, you would then need to maintain both C++ and Lean elaborators.

[Mario Carneiro]

@Sebastian Ullrich can tell you more about the extent of current bootstrapping plans

[Edward Ayers]

I'm reading through the kernel code. Let me just write down what I think is happening and then I can be corrected.
- expr.cpp is doing roughly the same thing as expr.lean, just a big inductive type with helper methods.
- type_checker infers the type for a given expr or throws if it isn't a valid expr. Saying that a given expr typechecks is equivalent to saying that the expr can be built just using the inference rules of CIC (up to being able to synthesize metavars later).
- You inject a normalizer_extension into the kernel to dictate how the typechecker should put terms in WHNF. If there is a bug in the injected normalizer_extension then the kernel will be compromised too. So quotients and inductives are normalizer_extensions.
- So the kernel is happy when it is given an environment, which is an ordered dictionary of declarations indexed by name, and all of the declarations' exprs typecheck.

[Edward Ayers]

In the system description for Lean it says that the typechecker can also produce unification constraints, but this feature doesn't seem to be in thetype_checker.h, although I could not be reading thoroughly enough, where is the code that does type_checking and also spits out some unification constraints?

[Leonardo de Moura]

@Edward Ayers You have to go back in time to see the unification constraints :) https://github.com/leanprover/lean/blob/CADE25/src/kernel/type_checker.h
We abandoned this approach in Lean 3. Now, the kernel type checker is simpler and has no support for meta-variables (unification variables). The elaborator uses a different module for inferring types and solving unification constraints.

[Sebastian Ullrich]

@Mario Carneiro

I don't know exactly how the full bootstrap process would work, it might just run itself on the previous version of lean to avoid messy business

Yes, this is how all bootstrapping compilers work. But instead of a binary file, we want to store the previous version as extracted C++ code, which should be at least slightly more inspectable and git-friendly

[Edward Ayers]

Thanks Leo. Also elab_context.h is confusing me. The comment talks about tactic_context. But I can't find any other mentions of tactic_context. I also can't spot the definition of type_context, only type_context_old

[Edward Ayers]

I'm really keen to see the C++ code that is used to keep track of metavariables, local context and so on while a tactic or elaborator is being run. It seems to be type_context_old but I'm not sure because of the old suffix.

[Gabriel Ebner]

type_context was renamed to type_context_old in the preparation of the changes for Lean 4. You should really be looking at type_context_old, it was the type_context for most of Lean 3.

[Edward Ayers]

In the type_context.h there is a large comment starting with NEW DESIGN notes. (This is work in progress), is this how Lean 3 works or is it how Lean 4 works?

[Gabriel Ebner]

This is a change that was introduced late in Lean 3, and the todo is also implemented now with the unfreeze_local_intstances tactic.

[Simon Hudon]

@Edward Ayers I recommend you start using different topics for your different questions so that other people may determine at a glance if the discussion is relevant to what they're working on.

[Edward Ayers]

ok will do

[Simon Hudon]

Thanks!

[Kevin Buzzard]

I like the question barrage :-) but I do see Simon's logic. I often start new threads with more descriptive titles now and it works better for search when I come back to them later.