(bug: lean4.py): Propagate the lakefile

[gaetanserre]

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.

[cpitclaudel]

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?

[gaetanserre]

Indeed, its much better. #fee2fc1 should be fine.

[cpitclaudel]

I think this try..catch is fine, but it might be more readable as

lake_idx = self.user_args.index("--lake")
if lake_idx < 0:
  lake_idx = len(self.user_args) # or -2
  self.user_args += …

[gaetanserre]

I guess the issue is that if --lake is not in user_args, the .index method will raise an error...

[cpitclaudel]

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.

[gaetanserre]

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.

[gaetanserre]

I made a new PR. See #98.