Lake and graph interop failure via `lake-manifest.json`

[davideger]

Description

The serialization of dependencies by lake build into lake-manifest.json is not case sensitive, and downstream tooling fails as a result.

Context

Caveat: I'm looking to do something that is admittedly a hack.

AlphaProof currently accepts a single '.lean file and offers a search to complete sorrys within the file. The file may depend on anything in mathlib4 and a few other standard libraries loaded into Google's Lean. We'd like to extend this service so that AlphaProof might handle a multi-file project -- that is, that a client may be able to transmit the .lean files depended upon within the current package and send them so the server can evaluate completions. We presume any separate packages like mathlib4 are already loaded and compatible in the AlphaProof server.

Import Graph seemed like a good place to look, and my first attempt at using it on Linux fell over.

Steps to Reproduce

Steps to reproduce:

git clone https://github.com/leanprover-community/mathematics_in_lean
cd mathematics_in_lean
lake build           # step 1
lake exe graph   # step 2

Step 1 passes and produces a lake-manifest.json which names the current package "mil" but produces .olean files like MIL.olean.
Step 2 reads lake-manifest.json and guesses the case of the current package as "Mil" but then falls over complaining that it cannot find "Mil.olean"

Expected behavior: Step 2 should create a .dot file of the dependencies within the Mathematics in Lean Project.
Actual behavior: Step 2 fails because it has the wrong expected name Mil.olean instead of MIL.olean

Versions

Lake version 5.0.0-6741444 (Lean version 4.21.0)
Ubuntu derivative / 6.16.12-1rodete2 amd64

This issue does not seem to affect mac, as its filesystems are not case sensitive.

[tydeu]

This is a bug in import-graph. It assumes that the main module of a package is the capitalized form of the the package's name (see here), which is not the case for MIL. I will investigate correcting this behavior with maintainer of import-graph in the new year. In the meantime, you can explicitly tell graph what module to use via the following invocation:

lake exe graph --to MIL