| import Lake | |
| open Lake DSL | |
| package paxCoder where | |
| name := "pax-coder" | |
| require mathlib from git | |
| "https://github.com/leanprover-community/mathlib4" @ "master" | |
| lean_lib PAX where | |
| roots := #[ | |
| `PAX.ConstraintDAG, | |
| `PAX.IR_DAG, | |
| `PAX.PipelineDAG, | |
| `PAX.Float16_Rounding, | |
| `PAX.WMMA, | |
| `PAX.TrainingData | |
| ] | |