15
$\begingroup$

It seems Lean can produce .olean files from Lean files, and the mathlib project provides an infrastructure to download olean files, which seems to allow the developer to edit a module without having to load and process its dependencies.

But what are they exactly? What is their format, and what do they contain?

$\endgroup$
3
  • $\begingroup$ Unless someone writes a response I’ll summarize the discussion from leanprover.zulipchat.com/#narrow/stream/113488-general/topic/… as an answer in due time $\endgroup$ Feb 10, 2022 at 17:43
  • 1
    $\begingroup$ I would be interested in a list of things that would be found in the file, not necessarily with too much detail though, and I don't know the complete answer, so I'd be happy to see someone else give it a shot. $\endgroup$ Feb 10, 2022 at 20:40
  • 3
    $\begingroup$ In that case, please change the title to something like "What are the contents of .olean files?" $\endgroup$ Feb 10, 2022 at 22:17

2 Answers 2

13
$\begingroup$

(My answer is for Lean 3. I don't know how .oleans changed in Lean 4.)

Also, see this discussion on the Lean Zulip.

TL;DR

An .olean is a "compiled" .lean file. They make everything faster.

For users of Lean 3

A .lean file is computationally expensive to check and process each time. Checking all of Lean's mathlib library for example would take hours. By running lean --make one can "compile" a lean file and all its dependencies to .olean files. (Here "compile" is maybe best thought of an analogy.)

In particular there is a hash in the .olean to make sure it is in sync with the .lean files. If the files are in sync, then when you import a dependency, Lean will skip the .lean file and only look at the .olean file. This is orders of magnitude faster. (Actually, it is even possible to just have use .olean files without the corresponding .lean files.)

Because of the huge speedup, when one uses a project based on mathlib, one should get the .olean files as well. (This is naturally done with leanproject.) Also, if Lean all of a sudden gets slow or takes a lot of memory, it is possible you accidentally opened or touched a dependency file in a way which is is making Lean reprocess that file and everything that depends on that file, skipping the .olean files.

For advanced use (such as working on mathlib), see the advice here.

More technical details

An .olean file

  • ...is basically a dump of everything in the Lean environment for that file.
  • ...doesn't contain any information about the tactic proofs. Instead it only contains the term proofs which are much faster to check. (I don't think Lean even checks the proofs in an .olean file when it is loaded, but I'm not positive.)
  • ...contains all the information needed by the Lean VS Code extension (which is run using the Lean language server). For example if you hover over a definition, VS Code will give you information about the location of that definition, its type, and its value. You can also jump to that definition. This is because that information is stored in the .olean file.
  • ...provides all the information needed to parse a Lean file. Notation, definition names and types, and tactic parsing code is stored in the .olean files in some form or another.
  • ...provides all the information about the environment that tactics need. Some tactics like library_search need to search over all theorems in the environment. Others tactics like simp look at a list of simp lemmas to apply. That data is all stored in the .olean files.
  • ...provides all the information needed by #print. This includes the term proof of a theorem. (Yet another reason why the term proof is in the .olean file.)
  • ...can be used by other checkers to double check that the proofs are correct. There are a few external checkers available for .olean files. They implement the same logic as in Lean's kernel. This provides an extra guarantee that your proof is correct. (I could be mistaken, but I think the continuous integration of mathlib runs at least one external checker on all of mathlib every time there is a PR.)
  • ...is not in a human readable format. I think it is stored as a sort of linked graph similar to how it is stored internally in Lean.
  • ...is not well documented. The best documentation is likely Mario's olean-parser mentioned in Joachim's answer.
  • ...is probably not the best way to access Lean information. One of the best ways to get and work with the information in the .olean files is through Lean meta-programming. Basically you can write a Lean program to traverse the environment. This isn't well documented either, but there are a lot of knowledgeable folks and examples on the Lean Zulip chat.
$\endgroup$
2
$\begingroup$

One possible source for an answer to this is the source code of the independent olean-parser digama0/olean-rs, in particular the types.rs file.

Based on this, an olean file contains a header with a magic string version number and a hash, followed by a sequence of entries (“modifications”). These can be:

  • Declarations, which can be a definition, a theorem, a constant or an axiom. All declarations have a names and a type. Definitions and theorems also have a value, i.e. the right-hand side (and it is worth noting that the values, i.e. the proof objects, of theorems are retained and stored here). Definitions also have a “ReducibilityHints” which can also be Opaque or Abbrev and likely control reduction.

  • Export declarations, which seems to export a set of names under a different name.

  • Position information, mapping a name to its position in the module.

  • Inductive declarations, for inductive definitions including their constructors (here called rules)

  • Modifications related to namespace management (AuxRec, Protected, Private…)

  • Classes, Instances and

  • Notation definitions

  • Attributes like noncomputable

  • Virtual machine code

  • Docstrings, as a mapping from name to String.

  • Quite a number of more entries where I can’t with good conscience guess what they are (GInd, Inverse)

$\endgroup$
3
  • $\begingroup$ Hmm, this is the best I can come up with, but I am not actually happy with this answer; it’s a bit too detailed, and doesn't see the forest for all the trees. Maybe someone else will find a better answer, or improve this one, or maybe it’s just hard. $\endgroup$ Feb 11, 2022 at 21:28
  • 1
    $\begingroup$ Forest for trees answer: It is a "compiled" lean file. It contains the term proofs produced by the tactics, and everything needed for later Lean files. When you start up Lean and say load mathlib, if you have up-to-date oleans for all your dependencies, Lean loads instantly. If not (or if you change a dependency without recompiling it, so the olean is out of date) then Lean will have to rerun the lean files. And, yes, olean files can be used by external tools for rechecking a Lean proof giving an even high degree of confidence it is correct, but that is not their main purpose as I see it. $\endgroup$
    – Jason Rute
    Feb 11, 2022 at 21:35
  • $\begingroup$ Thanks, Jason! But what does “compiled” mean? To proof terms? Or something lower? Does it contain just what user need to know to use the module? Or also what's needed to independently check the module (again, coming back to proof terms). $\endgroup$ Feb 11, 2022 at 22:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.