search

argumentcomputer / LSpec

A Testing Framework for Lean
MIT License
44 stars 7 forks source link

Having trouble importing against mathlib 4.12 #47

Closed seanmcl closed 4 hours ago

seanmcl commented 4 hours ago

Hi! Relatively new to Lean, so forgive me if this is a newbie error.

I have a project using mathlib at 4.12.0

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.12.0"

I tried LSpec at your 4.12.0 tag

require LSpec from git
  "https://github.com/argumentcomputer/LSpec.git" @ "v4.12.0-toolchain"

When I tried to import LSpec I get

import LSpec.SlimCheck.Gen failed, environment already contains 'SlimCheck.Gen.listOf._rarg._cstage2' from Mathlib.Testing.SlimCheck.Gen

Did I do something wrong here? Thanks.

mpenciak commented 4 hours ago

Hey! Thanks for taking interest in LSpec.

LSpec uses the SlimCheckmodule to do property testing, and large parts of the SlimCheck module is taken from SlimCheck in Mathlib. The error you're getting is probably a result of imports from the two copies of Slimcheck in Mathlib and LSpec overlapping.

A workaround to this is being more granular about your Mathlib and/or LSpec imports to avoid repeatedly importing the SlimCheck module..

seanmcl commented 4 hours ago

Great, thank you. Importing Mathlib.Tactic was the culprit. May be nice if SlimCheck became its own repo!

mpenciak commented 4 hours ago

Great, thank you. Importing Mathlib.Tactic was the culprit. May be nice if SlimCheck became its own repo!

No problem! I believe a large part of SlimCheck has been factored out into https://github.com/leanprover-community/plausible very recently. In fact, slimcheck has already been removed from mathlib at the more recent tags.