Duper on v4.7.0-rc2

Stream: general

[Utensil Song]

I was updating my Lean toolchain to v4.7.0-rc2 and dependencies (Mathlib, Duper etc.) for a Lean file using duper (require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "main"), I got the following error at import Duper [1]:

`~/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lake setup-file /path/to/my/DuperTest.lean Init Duper --no-build` failed:

stderr:
error: 'Duper' ▸ 'Duper.Tactic' ▸ 'Duper.Interface' ▸ 'Std.Lean.CoreM': no such file or directory (error code: 2)
  file: ./.lake/packages/std/././Std/Lean/CoreM.lean

During debugging, I noticed that duper main branch is one month old [2], and it's not found (thus no CI against the latest toolchain) in https://reservoir.lean-lang.org/ probably due to lack of a lean4 tag [3].

I removed import Std.Lean.CoreM in Duper.Interface and it took a while (using only 25% of CPU [4] which possibly indicates insufficient parallelization ) to reach more errors:

error: 'Auto.Translation' ▸ 'Auto.Translation.Monomorphization' ▸ 'Auto.Embedding.Lift' ▸ 'Std.Data.Int.Basic': no such file or directory (error code: 2)
error: 'Std.Data.BitVec.Basic': no such file or directory (error code: 2)

then simple removal of import Std.Data.Int.Basic and then import Std.Data.BitVec.Basic no longer works, and I'm seeing

image.png

which is a mixed experience of unknown constant 'Std.BitVec.ofNat' and

`Std.BitVec` has been deprecated

but I fail to found where the former is moved to [5] or what is the latter deprecated by [6] unless maybe I do a proper search on Zulip. (Disclaimer: I haven't used Lean for around 2 months due to sickness and work)

Sorry for reporting a series of issues in one go, I marked every one I consider an issue (of Duper or of v4.7.0-rc2) with a [number] for easier reference.

[Kim Morrison]

BitVec has changed namespaces. It's now in _root_, not Std.

[Utensil Song]

Thanks, I just learn that in release notes, but I wonder if the deprecation message could be more clear (for this or future deprecations) in [6], or is it technically possible to avoid "unknown constant" of Std.BitVec.ofNat in [5] due to the deprecation of one-level-up Std.BitVec.

[Utensil Song]

Gently ping @Josh Clune :smiley:

BTW, do you know any projects actively using Duper? In my tests, using Duper means continuingly depending on Duper, as duper? generates calls to duper, so it's better to track it with reservoir[3] to keep it working for new Lean/Mathlib releases.

[Josh Clune]

Thanks for the ping. I'll work on getting Duper working with the latest lean-toolchain as soon as I can, and I'll ping you once I've pushed a version that is compatible with 4.7.0.-rc2.

[Josh Clune]

@Utensil Song I've updated Duper's main branch to use Lean v4.7.0-rc2. I've also added a lean4 tag and LICENSE file to the repository, so if my understanding is correct, Duper should automatically be added to https://reservoir.lean-lang.org/ the next time Lean is updated. This version of Duper should be compatible with the v4.7.0-rc2 branch of Mathlib. Let me know if you run into any issues.

[Utensil Song]

@Josh Clune Many thanks, and my local test now passes after bumping and rebuilding Duper. :tada:

I can also see reservoir has picked up and built Duper successfully but reservoir itself has failed to collect the results due to Error: Unable to download artifact(s): Failed to GetSignedArtifactURL: Unable to make request: ECONNRESET. @Mac Malone , have you noticed the red CI?

[Mac Malone]

@Utensil Song No, sorry, I had not. The good news is that the failure did not repeat today! Sadly, there are intermittent GitHub / hosting failures that lead to the daily update failing sometimes. Thus, expecting weekly updates is often safer.

[Utensil Song]

https://reservoir.lean-lang.org/@leanprover-community/duper :tada: