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: `print-paths` changed to `setup-file` in Lean v4.4.0 #55

Closed utensil closed 10 months ago

utensil commented 10 months ago

Description

LeanInk/Analysis/LeanContext.lean relies on print-paths to initializeLakeContext, but in leanprover/lean4#2858 which is part of Lean v4.4.0 release, print-paths is changed to setup-file, with an extra parameter and changed JSON output.

This PR bumps LeanInk to use v4.4.0-rc1, replacing print-paths with setup-file and handles the parameter and output change accordingly.

There is probably no immediate need to merge this PR as doc-gen4 is using https://github.com/hargoniX/LeanInk/ which is 30+ commits behind leanprover/LeanInk and doesn't have this file, and I'm not aware of other major users.

More discussions on Zulip.

Notable Changes

Additional Notes

utensil commented 10 months ago

Locally it works fine (on Mac and my Ubuntu CI), but CI is red. Will look into that later.

utensil commented 10 months ago

There is no way I can pass the test for LeanInk. I tried the 2 approaches:

  1. bumping Lean for LeanInk, so LeanInk itself and the target Lean program are both on v4.4.0, but tests in LeanInk are outdated by this leap of Lean toolchain, causing many failures that I don't intend to fix in this PR (or should I?). (this is now at my fix-print-path-bump branch)
  2. don't bump Lean for LeanInk, so LeanInk itself is on old Lean (on this PR branch), it works fine for a target Lean program on v4.4.0 (locally), but tests in LeanInk are still failing because now the target Lean programs are the tests in LeanInk on the old Lean toolchain which doesn't play with setup-file.
utensil commented 10 months ago

I'll take approach 1, and fix the tests later. In the meanwhile, code in this PR or branch fix-print-path-nobump can lake build and works for target Lean code on Lean v4.4.0.

femtomc commented 10 months ago

Note that this branch (and its fixes) also fixes my issue #56.