olean-rs

KO | EN

gitlite — search

#javascript #python #hacktoberfest #react #ai #typescript #llm #go #golang #android #machine-learning #rust #deep-learning #linux

★ 13 Open GitHub ↗

parser/viewer for olean files (lean 3)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[![Build Status](https://travis-ci.org/cipher1024/olean-rs.svg?branch=master)](https://travis-ci.org/cipher1024/olean-rs)

# olean-rs
Parser/viewer for olean files, written in Rust and Lean.

See `olean.lean` for the lean version, and build with `cargo` for the Rust version. Currently the Rust version is faster by a factor of a hundred or so, so I don't know if I will continue to keep the Lean version up to speed.

Why look at olean files? The `olean` file format is an unstable binary format used by lean for caching successfully parsed files. As such, it is much easier to parse from a third party position than a `lean` file. Second, although lean supports an export format, the format is quite lossy, essentially only representing the expressions that are defined in the file. By contrast, the `olean` file contains lots of other information like notation declarations, attributes, `protected` status and namespace locations (which are not accessible through lean metaprogramming), and VM code. So `olean` parsing is the first step to a number of other processing or analysis passes.

## Building the Rust project

```shell
rustup toolchain install nightly
rustup override set nightly
cargo build
```

## Getting Started

```
Usage: target/debug/olean-rs path/to/file.olean [options]

Options:
    -D, --dump FILE      dump olean parse
    -L                   give location of lean library
    -d, --deps lean.name view all dependents of the target file
    -p DIR               set current working directory
    -l lean.name         test lexer
    -t lean.name         testing
    -h, --help           print this help menu
```

olean-rs

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README