search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

fix: handle lakefile.toml #58

Closed gaetanserre closed 2 months ago

gaetanserre commented 2 months ago

Description

Change the lakeFile.fileName check in LeanContext.lean/initializeLakeContext in order to handle .toml lakefile, introduced in Lean v4.8.0.

mhuisi commented 2 months ago

This repository is unfortunately effectively unmaintained, but the change looks simple enough and I've quickly checked that lake setup-file works as expected with the TOML config as well, so this seems fine to merge.