Importing project on past version of Lean.

Stream: general

[Mattias Ehatamm]

I'm trying to create a project that depends on the Lean-QuantumInfo project (https://github.com/Timeroot/Lean-QuantumInfo). As this project exists on toolchain version v4.23.0-rc2, I set my toolchain version similarly to v4.23.0-rc2. First, I tried putting the line require quantumInfo from git "https://github.com/Timeroot/Lean-QuantumInfo" in my lakefile.lean. However, when I cleared my build and cache and ran lake update, this checked out the wrong version of mathlib4 and caused the project to fail to build. I figured this might be because Lean-QuantumInfo only uses the line require "mathlib" from git "https://github.com/leanprover-community/mathlib4.git", instead of specifying a commit. I cloned the repository and imported locally, having changed the desired commit to the tagged commit for the correct toolchain version. This checked out the correct commit of mathlib4, but fails to check out the correct versions of mathlib's dependencies, like batteries. How can I fix this issue?

[Eric Wieser]

You should have only that require in your lakefile, and not another one for mathlib

[Mattias Ehatamm]

I have only that require, the mathlib require is found in the lakefile for Lean-QuantumInfo.

[Eric Wieser]

Then what you described should just work. What was the build failure?

[Mattias Ehatamm]

The build failure was coming about when I was trying to additionally import a second package, but I can isolate the issue to lake update failing to check out the correct versions of packages like battery when I just run that require. My terminal output after lake update begins with:

info: quantumInfo: cloning https://github.com/Timeroot/Lean-QuantumInfo
info: toolchain not updated; already up-to-date
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'da03f176071431c7f212d8262d05aa422b269876'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '240eddc1bb31420fbbc57fe5cc579435c2522493'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '99657ad92e23804e279f77ea6dbdeebaa1317b98'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'dba7fbc707774d1ba830fd44d7f92a717e9bf57f'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6e47cc88cfbf1601ab364e9a4de5f33f13401ff8'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '3b779e9d1c73837a3764d516d81f942de391b6f0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f85ad59c9b60647ef736719c23edd4578f723806'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'a67fc66cd1ebc0855dc064a4be727798771c0f89'
info: Cli: cloning https://github.com/mhuisi/lean4-cli
info: Cli: checking out revision '6667b921594697980586296511fab6a359e802d1'

and I can see that the commit for batteries with that hash is this, which you can see is tagged for v4.24.0-rc1.

[Kim Morrison]

You shouldn't need to require batteries, it will come transitively via mathlib.

[Kim Morrison]

Can you show us your lakefile or repo?

[Mattias Ehatamm]

Sure, my lakefile which results in this code is:

import Lake
open System Lake DSL

package «ATP_Test»{
}

require quantumInfo from git "https://github.com/Timeroot/Lean-QuantumInfo"


@[default_target]
lean_lib ATPTest

As I said, I am only requiring a single import.

[Kim Morrison]

Is there a repo we can clone?

[Mattias Ehatamm]

just made one, though as I haven't done anything substantial so far it consists of essentially just that lakefile, a lean-toolchain, and a basic file importing something from the dependency.

https://github.com/mehatamm/ATP_Test

[Kim Morrison]

@Mac Malone, cloning this repo and running lake build, we get:

$ lake build
info: quantumInfo: cloning https://github.com/Timeroot/Lean-QuantumInfo
info: quantumInfo: checking out revision '69adc042feceede68c6b3507f541c6c42731c1bf'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'da03f176071431c7f212d8262d05aa422b269876'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '240eddc1bb31420fbbc57fe5cc579435c2522493'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '99657ad92e23804e279f77ea6dbdeebaa1317b98'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'dba7fbc707774d1ba830fd44d7f92a717e9bf57f'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '6e47cc88cfbf1601ab364e9a4de5f33f13401ff8'
info: aesop: cloning https://github.com/leanprover-community/aesop
error: external command 'git' exited with code 128

Didn't you make sure at some point that git errors actually propagated to the user? What are we meant to do here?

[Kim Morrison]

Despite this error, lake exe cache get and a second lake build succeeds. @Mattias Ehatamm, does that agree with your experience?

[Kim Morrison]

Actually, attempting this again things seem to work fine. I guess the request to @Mac Malone for better error propagation still holds, but @Mattias Ehatamm, could you describe steps to reproduce your problem?

[Mac Malone]

@Kim Morrison -v would produce more logs, but I believe the indication here is that this is a transient error. Regardless, I do intend to improve the logging here.

[Mattias Ehatamm]

Kim Morrison said:

Actually, attempting this again things seem to work fine. I guess the request to Mac Malone for better error propagation still holds, but Mattias Ehatamm, could you describe steps to reproduce your problem?

To reproduce my problem, clone the repository and run lake update to generate a lake-manifest.json. The command-line output will indicate that the incorrect commit of batteries has been checked out, and the lake-manifest.json agrees with the command-line output in indicating the wrong version. I was not claiming that this specific setup results in a build error, but I believed that the version error in my lake-manifest.json was leading to a build error when I tried to combine this with another package.

[Mattias Ehatamm]

The reason it builds successfully here is that when running lake update immediately after cloning, lake appears to actually check out a different commit of batteries than it claims to or indicates in lake-manifest.json. Looking in .lake\packages\batteries\lean-toolchain indicates that the version of batteries is v4.23.0-rc2, which wouldn't be the case if it had checked out the version it claimed to.

[Mattias Ehatamm]

I talked to @Sebastian Ullrich at the office hours, we dealt with this issue. I was confused about tag history, and it turned out that the batteries commit that was logged was actually the correct version. My multiple dependencies issue was then resolved when I moved the import that required mathlib to the bottom of my lakefile instead of the top.