Branch unification #132

New Issue

aniva · 2024-12-05T15:34:19-08:00

aniva commented

2024-12-05 15:34:19 -08:00

Can we merge two goal states from two different search paths?

aniva added the

part/Goal

category

feature

labels 2024-12-05 15:34:19 -08:00

aniva self-assigned this 2024-12-05 15:34:19 -08:00

aniva commented

2024-12-05 15:35:24 -08:00

This will probably involve some application of the MetaTranslateM monad. If a goal state has two children, their metavariable names may clash, and there would need to be a distinguishing factor to tell apart if the two children share a mvar because of their common ancestry or because of coincidence.

This will probably involve some application of the `MetaTranslateM` monad. If a goal state has two children, their metavariable names may clash, and there would need to be a distinguishing factor to tell apart if the two children share a mvar because of their common ancestry or because of coincidence.

aniva added the

priority

low

label 2024-12-05 16:43:52 -08:00

aniva added the

part/Serial

label 2025-03-14 12:33:13 -07:00

aniva added a new dependency 2025-03-28 00:57:13 -07:00

#177 feat: Update `CoreM` options from parsed header

aniva changed title from ~~Proof state merger~~ to Branch unification

2025-03-28 00:57:19 -07:00

aniva commented

2025-03-29 19:07:02 -07:00

Useful comment from Environment.lean:

Note [Environment Branches]

The kernel environment type Lean.Kernel.Environment enforces a linear order on the addition of
declarations: addDeclCore takes an environment and returns a new one, assuming type checking
succeeded. On the other hand, the metaprogramming-level Lean.Environment wrapper must allow for
branching environment transformations so that multiple declarations can be elaborated
concurrently while still being able to access information about preceding declarations that have
also been branched out as soon as they are available.

The basic function to introduce such branches is addConstAsync, which takes an environment and
returns a structure containing two environments: one for the "main" branch that can be used in
further branching and eventually contains all the declarations of the file and one for the "async"
branch that can be used concurrently to the main branch to elaborate and add the declaration for
which the branch was introduced. Branches are "joined" back together implicitly via the kernel
environment, which as mentioned cannot be changed concurrently: when the main branch first tries to
access it, evaluation is blocked until the kernel environment on the async branch is complete.
Thus adding two declarations A and B concurrently can be visualized like this:

o addConstAsync A
|\
| \
|  \
o addConstAsync B
|\   \
| \   o elaborate A
|  \  |
|   o elaborate B
|   | |
|   | o addDeclCore A
|   |/
|   o addDeclCore B
|  /
| /
|/
o .olean serialization calls Environment.toKernelEnv

While each edge represents a Lean.Environment that has its own view of the state of the module,
the kernel environment really lives only in the right-most path, with all other paths merely holding
an unfulfilled Task representing it and where forcing that task leads to the back-edges joining
paths back together.

Useful comment from `Environment.lean`: # Note [Environment Branches] The kernel environment type `Lean.Kernel.Environment` enforces a linear order on the addition of declarations: `addDeclCore` takes an environment and returns a new one, assuming type checking succeeded. On the other hand, the metaprogramming-level `Lean.Environment` wrapper must allow for *branching* environment transformations so that multiple declarations can be elaborated concurrently while still being able to access information about preceding declarations that have also been branched out as soon as they are available. The basic function to introduce such branches is `addConstAsync`, which takes an environment and returns a structure containing two environments: one for the "main" branch that can be used in further branching and eventually contains all the declarations of the file and one for the "async" branch that can be used concurrently to the main branch to elaborate and add the declaration for which the branch was introduced. Branches are "joined" back together implicitly via the kernel environment, which as mentioned cannot be changed concurrently: when the main branch first tries to access it, evaluation is blocked until the kernel environment on the async branch is complete. Thus adding two declarations A and B concurrently can be visualized like this: ```text o addConstAsync A |\ | \ | \ o addConstAsync B |\ \ | \ o elaborate A | \ | | o elaborate B | | | | | o addDeclCore A | |/ | o addDeclCore B | / | / |/ o .olean serialization calls Environment.toKernelEnv ``` While each edge represents a `Lean.Environment` that has its own view of the state of the module, the kernel environment really lives only in the right-most path, with all other paths merely holding an unfulfilled `Task` representing it and where forcing that task leads to the back-edges joining paths back together.

Sign in to join this conversation.