Closed gaetanserre closed 3 weeks ago
Thanks a lot!
Looking at the code, it seems that the --lake
argument is removed from the user_args
earlier to populate the self.lake_file_path
field. Wouldn't it be simpler to leave it in the user_args
rather than removing it first and then re-adding it?
Indeed, its much better. #fee2fc1 should be fine.
Sorry, I meant to rebase on main and merge, but Github only let me do the first step and marked the PR closed; can you reopen it by force-pushing to it? (Sorry for the trouble)
I have one last question: this will pass a dummy --lake lakefile.lean
if none is specified. Is that desirable / expected? The previous version of the code added this only if a lakefile had been found.
Sorry, I meant to rebase on main and merge, but Github only let me do the first step and marked the PR closed; can you reopen it by force-pushing to it? (Sorry for the trouble)
I am sorry, I don't know how to do that right now but I'll look into it.
I have one last question: this will pass a dummy --lake lakefile.lean if none is specified. Is that desirable / expected? The previous version of the code added this only if a lakefile had been found.
I guess it depends on the behaviour of LeanInk. In any case, a Lean project must have a lakefile so if the user is not providing one, I think pass a dummy --lake lakefile.lean
is desirable. But we could also throw an error if the user did not provide a lakefile and no "dummy" lakefile (lakefile.{lean|toml}
) has been found in the working directory.
I made a new PR. See #98.
The lakefile path was not propagated to the Lean4 driver. As Lean recently changed their lakefile format from .lean to .toml, it can cause Alectryon + LeanInk to fail on any recent Lean4 project.