Lake sometimes ignores text mode

[Vtec234]

Description

In certain situations, Lake does not correctly pass the text mode setting to

lean4/src/lake/Lake/Build/Common.lean

Line 406 in 27e5e21

public def fetchFileHash (file : FilePath) (text := false) : JobM Hash := do

My best guess for a fix is to use computeArtifact file ext text as in Vtec234@e00b1de, but I don't understand the code well enough to make a PR.

Context

This has led to the issue described here. ProofWidgets relies on text-based hashing here in order not to rebuild its JS artifacts.

Steps to Reproduce

Only occurs in very specific cases. It seems the text-mode file must be part of a package that is a transitive dependency not specified directly in the lakefile, e.g. when depending on mathlib, which in turn depends on ProofWidgets.

1. git clone https://git.unnamed.website/leantest/
2. lake build (kill it after the proofwidgets error shows up)
3. cat .lake/packages/proofwidgets/widget/package-lock.json.hash and observe that it stores the binary-mode hash.

Note that if lake build mathlib or lake build proofwidgets is ran instead, the correct hash is calculated.

Expected behavior: package-lock.json is hashed in text mode

Actual behavior: package-lock.json is hashed in binary mode

Versions

4.25.0 as well as Lean 4.26.0, commit eba5a5a6ef478086246b5f9ef72bf949a2aed6d5

Additional Information

SHA-256: ba30505ac4dad0c299914b13eed2cf7d030d8d0eada1ca7846aa401d04723708 .lake/packages/proofwidgets/widget/package-lock.json
Text mode hash: 0186e1ad4f7ac1f8
Binary mode hash: b782184005d5892a

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.