Extracting the internal representation

Stream: lean4

[Andrej Bauer]

How would I go about extracting the internal representation, as represented in the kernel? This is for the purposes of machine learning. The idea is to take a large library, munch all of its files, and obtain the internal representations in a format that can be easily parsed by other tools. Has this been done?

For example, I was able to write a plugin for Agda that works a bit like its documentation plugin, but produces files with s-expressions instead of HTML. It took me about four days to figure it out. If there is a similar plugin for Lean, one that processes files and outputs them in some other format, that might be a good starting point.

[Sebastian Ullrich]

I have written a translator from Lean 4 .olean to a plain-text format: https://github.com/Kha/lean4export

[Jason Rute]

Also in Lean 3 it was easy to write a lean script to loop over the expressions of all the declarations in the library. I assume it is equally easy in Lean 4, but I don’t know the magic innovation. Also, you may be interested in the stream #Machine Learning for Theorem Proving

[Andrej Bauer]

BTW, what's the licensing status of your extension? I am thinking of adapting it so that it outputs s-expressions.

[Andrej Bauer]

One more question if I may: how do I extract the entire content without listing the constants on the command line?

[Sebastian Ullrich]

Andrej Bauer said:

BTW, what's the licensing status of your extension? I am thinking of adapting it so that it outputs s-expressions.

It's Apache now

[Sebastian Ullrich]

Andrej Bauer said:

One more question if I may: how do I extract the entire content without listing the constants on the command line?

That's what should happen by default if you don't use the --

[Sebastian Ullrich]

https://github.com/Kha/lean4export/blob/f1d507ff8c8ba2df2316e78c0186a84c6791305f/Main.lean#L11

[Andrej Bauer]

Thanks for everything. BTW, you should probably fill in the Copyright info at the end of LICENSE (year and your name).

[Sebastian Ullrich]

I think that is meant as a template for source-level copyright comments. The GitHub copyright wizard fills in this information for other licenses where it's needed, but not for Apache

[Andrej Bauer]

Sorry for going on with this, but I understand your code correctly (and based on running it), if no constants are given then it will dump all constants of all imports, recursively. What would be a good way of dumping only the constants that are defined in a given module?

[Mario Carneiro]

you can ask what module a constant is in and skip it if it's not the one you want

[Mario Carneiro]

unfortunately there is no better way to do it since the constants are in a hashmap so they are not meaningfully indexed by anything other than their name

[Mario Carneiro]

I think it would look something like this:

  let some target := env.getModuleIdx? `foo | throw (.userError "module not found")
  M.run env do
    env.constants.forM fun c _ => do
      if !c.isInternal && env.getModuleIdxFor? c == target then
        let _ ← dumpConstant c

[Andrej Bauer]

Is there a way to load a file, rather than to instruct Lean to import a module by name? That would be more useful to me. (And find out which constants were defined in the file.)

[Andrej Bauer]

Even better, can I just load .olean files and extract stuff from them? (Looking at Environment.lean now.)

[Andrej Bauer]

So Environment.ModuleData seems to perfectly fit my bill. Now just need to find out how to load an .olean file...

[Andrej Bauer]

Is Environment.readModuleData the one I want? Let me try.

[Andrej Bauer]

The .olean file contains entries like this:

IO.println._at.main._spec_1
IO.println._at.main._spec_1._cstage2
Nat.foo._cstage1
Nat.foo
main
main._cstage1
Nat.foo._cstage2
Array.forInUnsafe.loop._at.main._spec_2
List.forIn.loop._at.main._spec_3
main.match_1
main._cstage2
main.match_1._cstage1
Array.forInUnsafe.loop._at.main._spec_2._cstage2
List.forIn.loop._at.main._spec_3._cstage2

Is there a reliable way to tell which ones are "generated"? These would be _cstage and _spec stuff. BTW, what are they?

[Andrej Bauer]

Perhaps they have an attribute I can test.

[Henrik Böving]

They are both entries auto generated while doing code (old) generation iirc.

[Adam Topaz]

there's docs4#Lean.Name.isInternal

[Kyle Miller]

Mathlib has a function that uses that along with a few other checks: https://github.com/leanprover-community/mathlib4/blob/01da6a3c22053b87a02f5a4a7d78c10d6cb25160/Mathlib/Lean/Name.lean#L19

[Andrej Bauer]

Is it possible that an .olean file would contain a cyclic datastructure, so that naive traversal will cycle forever/

[Mario Carneiro]

no, all lean objects are cycle free (this is important for the RC collector to work)

[Mario Carneiro]

although I'm not exactly sure how IO.Refs are garbage collected

[Mario Carneiro]

you would need an unsafe inductive to create a structure that can have references to itself, I think

[Jannis Limperg]

I use a cyclic data structure in Aesop (involving unsafe and IO.Ref), but it never ends up in any .olean. I'd assume that the serialisation procedure for .oleans doesn't support cyclic data in the first place.

[Andrej Bauer]

For some reason Mathlib/Order/Copy.olean causes https://github.com/andrejbauer/lean2sexp to allocate 25GB of RAM and just sit around wasting 100% of CPU. So I thought maybe there are cycles, because lean2sexp simply traverses the constants and outputs ConstantInfo as S-expressions. I suppose I'll just have to debug a bit.

[Andrej Bauer]

If I suspect that something is wrong with the internal encoding of proof_8 (or something close to that name) in build/lib/Mathlib/Order/Copy.olean, how would I double-check?

[Mario Carneiro]

What kind of problem? if it is something you can see with lean code you are best off using loadModuleData to get at the olean and start hacking around in it with an eval block

[Mario Carneiro]

if it is something below that (i.e. in the actual byte representation and encoding) you could try using https://github.com/gebner/oleanparser, which is written like a more traditional parser (it does not use anything from Lean directly and could equally well be written in python) and produces some fairly low level output which you could use to debug the binary format

[Mario Carneiro]

(BTW, proof_8 is not enough to find the theorem in question, as a lot of things have a proof_8. Hopefully that is the last name component in some theorem's full name, which might help to debug this from the perspective of the source that generated it)

[Andrej Bauer]

I am getting somewhere. I am converting the content of an olean file to s-expressions (see https://github.com/andrejbauer/lean2sexp). The file build/lib/Mathlib/Order/Copy.olean is 2.1MB in size, but somehow in s-expression form that has everything except applications and lambdas pruned, it becomes 227MB. This seems like an amazingly efficient way of comperssing information in olean. Do olean files contain something other than abstract syntax trees? Are they optimized in some way?

[Andrej Bauer]

And build/lib/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.olean is even worse, it outputs 1.3 GB of stuff.

[Mario Carneiro]

Are you dag-sharing?

[Mario Carneiro]

because if not this will have massive blowup

[Mario Carneiro]

lean expressions are maximally shared in olean files IIRC

[Andrej Bauer]

Aha, that would do it. It's just amazing that there would be so much sharing. Where is it coming from? Surely no human produces such dags with bare hands.

[Mario Carneiro]

One common source of sharing is the names

[Mario Carneiro]

stuff like namespaces and particular theorem names are repeated many thousands of times in the average lean file

[Mario Carneiro]

I think actually interesting term sharing in proofs isn't that common, lean itself sometimes has trouble with it so it's not a particularly good thing to rely on

[Andrej Bauer]

I measured the size of the proof trees, counting applications and lambdas only. In build/lib/Mathlib/Order/Copy.olean there is a constant called CompleteLattice.copy.proof_8 whose size is 1342037. This is not caused by name sharing, since it contains that many applications and lambdas. And looking around, it looks like the really large ones are always called Foo.bar.proof_X.

[Mario Carneiro]

well the bulk of most proofs will be in definitions named something like that

[Mario Carneiro]

so that's not a huge indicator of anything

[Andrej Bauer]

But such huge proofs must have been generated by tactics, and moreover, are very likely proofs in Prop, no?
I mean, who would care about them?

[Mario Carneiro]

I think I can guess why CompleteLattice.copy is big: it's probably instantiating a structure with a deep inheritance hierarchy in one go using a very large structure instance

[Andrej Bauer]

So the type-class mechanism might be doing it?

[Mario Carneiro]

not quite

[Andrej Bauer]

If there is an identifiable way for me to detect that there are very large proofs that will not be very informative, I am more than happy to throw them away.

[Mario Carneiro]

To demonstrate why this leads to exponential growth or (more accurately) highly shared subterms, let's consider a smaller example:

class A (X : Type) where
  x : Nat
  y : Nat

def foo (X) [A X] : Nat := A.x X

class B (X : Type) extends A X where
  z : Nat
  h : foo X = z


def bla : B Int := {
  x := Nat.zero -- for a smaller pp.all
  y := Nat.succ Nat.zero
  z := Nat.zero
  h := rfl
}
-- set_option pp.explicit true
#print bla
-- def bla : B Int :=
-- @B.mk Int (@A.mk Int Nat.zero (Nat.succ Nat.zero)) Nat.zero bla.proof_1
#print bla.proof_1
-- def bla.proof_1 : @Eq Nat (@foo Int (@A.mk Int Nat.zero (Nat.succ Nat.zero)))
--   (@foo Int (@A.mk Int Nat.zero (Nat.succ Nat.zero))) :=
-- @rfl Nat (@foo Int (@A.mk Int Nat.zero (Nat.succ Nat.zero)))

[Mario Carneiro]

What is interesting here is that the type of h, which is filled in by bla.proof_1, is

@foo Int { x := Nat.zero, y := Nat.succ Nat.zero } = @foo Int { x := Nat.zero, y := Nat.succ Nat.zero }

where { x := Nat.zero, y := Nat.succ Nat.zero } is the first half of the structure just constructed

[Mario Carneiro]

in other words, each occurrence of foo (or more generally, any typeclass function) contains the complete record constructed by the structure instance. In practice this happens a lot, because for example groups extend monoids which extend ... which extend Add, which means that when you construct a group it uses the instance it derives for Add from the monoid, and then your instance which builds a group will have a subgoal saying something like (x + y) + z = x + (y + z) where every single + there is actually HAdd.hAdd .... (addOfMonoid { add := bla, add_zero := by simp, zero_add := by horrible proof term })

[Mario Carneiro]

so now you have 6 occurrences of the monoid structure in the group structure, and then to build the ring structure you will reference the group structure 6 times...

[Mario Carneiro]

rinse and repeat and by the time you get to CompleteLattice which probably has something like 12 parent structures in it things are kind of ridiculous

[Andrej Bauer]

Is there any way to detect the sharing present in ModuleData? Maybe some sort of physical equality?

[Mario Carneiro]

yes, you can use pointer equality if you need to do this from lean

[Mario Carneiro]

there is an unsafe function for it

[Mario Carneiro]

you can also compare hashes and make a cache, this is what most expr traversals in lean do

[Andrej Bauer]

Although, it seems that a saner option would be to elide all this stuff from the output. The output is meant to represent syntax trees to be used for machine learning. I am not sure machines will learn much from implicit arguments that were not given by the user directly.

[Mario Carneiro]

yeah, you can just pretty print everything

[Mario Carneiro]

or leave out implicit arguments from the sexprs which is a kind of basic version of pretty printing

[Andrej Bauer]

Even if I keep the shared structures, I am just postponing the problem to the next person (who is a machine learner), because they will hit the same problem. Just traversing these structures takes forever.

[Andrej Bauer]

Can I tell from olean which implicit arguments were filled by the machine and which ones by the human?

[Mario Carneiro]

that information does not exist

[Mario Carneiro]

you could look at the input syntax I suppose, but it's not really possible to truly know what was machine written

[Andrej Bauer]

Let me try omitting just instImplicit first. Perhaps that'll help.

[Andrej Bauer]

"Machine written" is not a well-defined notion, because a user could write a tactic which computes a term T Did the user "write T"?

[Mario Carneiro]

or even if text is in the lean file, was it created by a code action? (or by mathport, which probably has authorship on 70+% of mathlib4 right now by a strict reading)

[Mario Carneiro]

the line seems pretty impossible to draw

[Mario Carneiro]

but then again, isn't that the point of ITP?

[Andrej Bauer]

In all of Agda that we extracted to s-expressions, there is just one file that is unreasonably large (30MB). There are no, or close to none, type classes in Agda. I wonder what would happen with Coq.

[Mario Carneiro]

I think these issues are mostly deficiencies in lean, places where it is generating something dumb and when it shows up on a profile sometimes we try to fix it

[Andrej Bauer]

But what is one to think of the fact that the "trivial" information reconstructed by the type class mechanism in some cases is 99% of the proof?

[Mario Carneiro]

type class inference is a hugely expensive part of lean processing (that and defeq checking are the majority of compile time)

[Andrej Bauer]

Ugh. When staring at Expr.app e1 e2 it's actually quite difficult to tell whether e2 is an implicit argument.

[Mario Carneiro]

from a detached standpoint it all looks pretty crazy, but when you get into the weeds there aren't any obvious fixes - almost all of the typeclass system is actually being used in some way in mathlib in practice

[Mario Carneiro]

the way to find implicits is to get the type of the function symbol and traverse the pis

[Mario Carneiro]

are you working in a context where inferType does something useful?

[Andrej Bauer]

But the type of the function symbol need not be in normal form.

[Andrej Bauer]

I am just loading .olean files, so whatever is in them.

[Mario Carneiro]

I mean can you load them into an environment such that the usual lean functions work

[Mario Carneiro]

there is a function by the name forallTelescopeReducing which does the normalization

[Andrej Bauer]

You tell me :-) It's Lean4 and I am loading them in with Lean.readModuleData (and throwing away the compacted region, cause I don't know what that's for).

[Mario Carneiro]

that's for freeing the data, if you discard it then it will live until the end of the program, which is usually fine

[Andrej Bauer]

In particular, I am not loading the dependencies, so I can't really process anything.

[Mario Carneiro]

yeah that's what I was afraid of

[Mario Carneiro]

you should probably do that, it is not that expensive

[Andrej Bauer]

This is machine learning, we should look for a practical solution.

[Mario Carneiro]

I think there is a function which automatically handles all this

[Mario Carneiro]

withImportModules

[Mario Carneiro]

or I guess importModules

[Andrej Bauer]

I could store dag's if I wanted to, my output format allows it.

[Andrej Bauer]

Is it just me, or do .olean files reference entities by their short names, i.e., one has to rely on import statements to figure out what a given name refers to? Is there some way to get fully qualified names?

[Mario Carneiro]

I would be very surprised for that to be the case

[Mario Carneiro]

(also you mean namespace / open, not import. import changes the set of names in the environment but not the names you can use to refer to them)

[Andrej Bauer]

Sorry, false alarm.

[Andrej Bauer]

Next weirdness: is it possible that the order of entries in .olean is not the same as in .lean, i.e., the definitions get mixed up? (Either that, or I have a bug.)

[Mario Carneiro]

I'm not even sure they are stored in any order

[Mario Carneiro]

isn't it a hashmap?

[Andrej Bauer]

According to ModuleData.constants, they are stored in an Array, which sounds sorted to me.

[Andrej Bauer]

But perhaps the complier mixes them up.

[Mario Carneiro]

yeah

  let constants  := env.constants.foldStage2 (fun cs _ c => cs.push c) #[]

where env.constants is a hashmap

[Mario Carneiro]

that's how the constants : Array ConstantInfo is populated

[Mario Carneiro]

agreed that this is a bit odd