test: version clash w/ diamond deps (#11155)

This PR adds a test replicating Kim's diamond dependency example.

The top-level package, `D`, depends on two intermediate packages, `B`
and `C`, which each require semantically different versions of another
package, `A`. The portion of `A` that `B` and `C` publicly use is
unchanged across the versions, but they both privately make use of
changed API. Currently, this causes a version clash. This will be made
to work without error later this quarter.

Author: tydeu

tests/pkg/ver_clash/DiamondExample-A/.gitignore

@@ -0,0 +1 @@
+.lake

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA.lean

@@ -0,0 +1,2 @@
+import DiamondExampleA.Ring.Defs
+import DiamondExampleA.Ring.Lemmas

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Defs.lean

@@ -0,0 +1,9 @@
+module
+
+public class Ring (A : Type) extends Add A, Mul A, Neg A, Zero A, One A where
+  add_assoc : ∀ a b c : A, a + b + c = a + (b + c)
+  add_comm : ∀ a b : A, a + b = b + a
+  add_zero : ∀ a : A, a + 0 = a
+  add_neg : ∀ a : A, a + -a = 0
+  mul_assoc : ∀ a b c : A, a * b * c = a * (b * c)
+  mul_comm : ∀ a b : A, a * b = b * a

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean

@@ -0,0 +1,13 @@
+module
+
+public import DiamondExampleA.Ring.Defs
+
+namespace Ring
+
+public theorem add_left_comm [Ring α] : ∀ a b c : α, a + (b + c) = b + (a + c) := by
+  intros a b c
+  rw [← add_assoc a b c]
+  rw [add_comm a b]
+  rw [add_assoc b a c]
+
+end Ring

tests/pkg/ver_clash/DiamondExample-A/lakefile.toml

@@ -0,0 +1,6 @@
+name = "DiamondExample-A"
+defaultTargets = ["DiamondExampleA"]
+
+[[lean_lib]]
+name = "DiamondExampleA"
+leanOptions.experimental.module = true

tests/pkg/ver_clash/DiamondExample-B/.gitignore

@@ -0,0 +1 @@
+.lake

tests/pkg/ver_clash/DiamondExample-B/DiamondExampleB.lean

@@ -0,0 +1 @@
+import DiamondExampleB.MainResult

tests/pkg/ver_clash/DiamondExample-B/DiamondExampleB/MainResult.lean

@@ -0,0 +1,11 @@
+module
+
+public import DiamondExampleA.Ring.Defs
+import DiamondExampleA.Ring.Lemmas
+
+open Ring
+
+public theorem foo [Ring α] (a b c d : α) : a + (b + (c + d)) = b + c + a + d := by
+  rw [poorly_named_lemma]
+  rw [poorly_named_lemma a c d]
+  rw [← add_assoc, ← add_assoc]

tests/pkg/ver_clash/DiamondExample-B/lakefile.toml

@@ -0,0 +1,11 @@
+name = "DiamondExample-B"
+defaultTargets = ["DiamondExampleB"]
+
+[[require]]
+name = "DiamondExample-A"
+git = "../DiamondExample-A"
+rev = "v1"
+
+[[lean_lib]]
+name = "DiamondExampleB"
+leanOptions.experimental.module = true

tests/pkg/ver_clash/DiamondExample-C/.gitignore

@@ -0,0 +1 @@
+.lake