format_lean:精益文件格式器 源码

精益格式化器 这个原型是一个python库,可将精益文件转换为其他文件,例如html文件的另一个精益文件。 安装 您需要Python 3.7或更高版本以及Lean。 确保已安装python软件包管理器pip 。 克隆此存储库,转到其根目录并运行pip install . (如果需要,请使用sudo -H )。 还建议安装ipython以进行交互使用。 另外,如果您不想弄乱全局python环境,则可以使用专用的虚拟环境。 在更完整的对此进行了说明。 用法 如果您只想使用我的示例格式化程序,则可以简单地运行format_lean (如果pip install . format_lean ,它应该在您的路径中)。 基本用法是: format_lean --inpath limits.lean --outdir build --lib-path /usr/lib/lean-mathlib/src