jixia_db

Parse a Lean repo into structured items, and store them in a PostgreSQL database.

Installation

Install Python deps

python -m venv .venv
source .venv/bin/activate
python -m pip install -r requirements.txt

Install Postgres

1. Download PostgreSQL (you can find the installation guide here).

2. Create database:

   createdb my_database_name
   

   Memorize the database name, you will later need to set it in your .env file.

Install jixia

1. Clone the jixia repo: git clone git@github.com:frenzymath/jixia.git; cd jixia
2. Make sure lean-toolchain in jixia and lean-toolchain in the project you will be indexing match. If Lean versions don't match, you will get "... failed to read file ..., invalid header" error when you try to index the project.
3. Build jixia: lake build (should take around 70s)

Set up the .env file

1. Copy the .env.example file to .env:

   cp .env.example .env

2. Edit the .env file and set the required variables according to your setup.

Usage

Creating database schema

psql -d <database name> -f src/schema.sql

Indexing your Lean project (uses jixia, puts results into PostgreSQL)

python -m src <project root> <prefixes>

Options:

• project root: Path to the project to index. This is where the lakefile.toml or lakefile.lean is located.
• prefixes: Comma-separated list of module prefixes. A module is indexed only if its module path starts with one of prefixes listed here. For example, Init,Lean,Mathlib will include only Init.*, Lean.*, and Mathlib.* modules.

Note: to check what modules are available in your project, and to determine how prefixes work, you can use python -m prefix --project_root <project_root> --prefixes <prefixes> helper command.