Omit derived files from repo (generate them locally instead) #1960
Description
This repository contains several files that are dynamically generated from other files in the repository. This ticket is about omitting those generated files from the repository and, instead:
- Documenting how developers can generate them locally as-needed
- Updating GitHub Actions to generate them so they are included in the package that gets published to PyPI
Related: #1602
One team member suggested that ideas in this area be prototyped in a temporary fork of this repository — so that they can be tested, demonstrated, and discussed without interfering with this repository.