[WIP] feat - start parsing metaprogramming functions

[lakesare]

This PR

Creates indexing for metaprogramming functions in Lean 4.

Instructions for what to do on production server

1. Run python -m database migrate
2. Run

   python -m database jixia <project root TODO> <prefixes TODO> --project-name=metaprogramming
   python -m database informal
   python -m database vector-db --project-name=metaprogramming
   

Instructions for reindexing mathlib and metaprogramming next time

1. Run make reset
2. Run python -m database migrate
3. To index mathlib, run

   python -m database jixia <project root> <prefixes> --project-name=mathib
   python -m database informal
   python -m database vector-db --project-name=mathlib
   

4. To index metaprogramming functions, run

   python -m database jixia <project root> <prefixes> --project-name=metaprogramming
   python -m database informal
   python -m database vector-db --project-name=metaprogramming
   

TODOs

• ensure all of this is backwards-compatible
• write instructions for how to index mathlib from now on (without thinking about caching)
• rewrite README.md to include --project-name

---

Eric Wieser (link):

If you want to exclude things like tactic parsers / metaprogramming, then probably dropping (or rather, filtering) things in the Lean namespace is a reasonable approximation. Dropping based on which folder things are in probably isn't a good heuristic.