test: version clash w/ diamond deps

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

tests/pkg/ver_clash/DiamondExample-C/DiamondExampleC.lean

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

tests/pkg/ver_clash/DiamondExample-C/DiamondExampleC/MainResult.lean

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

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

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

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

@@ -0,0 +1,2 @@
+.lake
+produced.out

tests/pkg/ver_clash/DiamondExample-D/DiamondExampleD.lean

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

tests/pkg/ver_clash/DiamondExample-D/DiamondExampleD/MainResult.lean

@@ -0,0 +1,11 @@
+module
+
+import DiamondExampleB.MainResult
+import DiamondExampleC.MainResult
+
+open Ring
+
+-- This uses `foo` from `DiamondExampleB` and `bar` from `DiamondExampleC`
+example [Ring α] (a b c d : α) : a + (b + (c + d)) = a + (b + c) + d := by
+  rw [foo]
+  rw [bar]

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

@@ -0,0 +1,16 @@
+name = "DiamondExample-D"
+defaultTargets = ["DiamondExampleD"]
+
+[[require]]
+name = "DiamondExample-B"
+git = "../DiamondExample-B"
+rev = "master"
+
+[[require]]
+name = "DiamondExample-C"
+git = "../DiamondExample-C"
+rev = "v2"
+
+[[lean_lib]]
+name = "DiamondExampleD"
+leanOptions.experimental.module = true

tests/pkg/ver_clash/clean.sh

@@ -0,0 +1,3 @@
+rm -rf DiamondExample-*/.git
+rm -rf DiamondExample-*/.lake DiamondExample-*/lake-manifest.json
+rm -f DiamondExample-D/produced.out

tests/pkg/ver_clash/test.sh

@@ -0,0 +1,79 @@
+#!/usr/bin/env bash
+source ../../lake/tests/common.sh
+./clean.sh
+
+# This directory contains a unified version of the "ring example"
+# developed by Kim across the following 4 repositories:
+#
+# * https://github.com/kim-em/DiamondExample-A
+# * https://github.com/kim-em/DiamondExample-B
+# * https://github.com/kim-em/DiamondExample-C
+# * https://github.com/kim-em/DiamondExample-D
+#
+# 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 (i.e., `Ring`) is unchanged
+# across the versions, but they both privately make use of changed API (i.e.,
+# `poorly_named_lemma` and its rename, `add_left_comm`).
+#
+# Currently, this causes a version clash, which is tested here.
+
+# ---
+# Setup
+# ---
+
+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the repositories on each test.
+
+pushd DiamondExample-A
+sed_i s/add_left_comm/poorly_named_lemma/ DiamondExampleA/Ring/Lemmas.lean
+$LAKE update
+init_git
+git tag v1
+sed_i s/poorly_named_lemma/add_left_comm/ DiamondExampleA/Ring/Lemmas.lean
+git commit -am "rename lemma"
+git tag v2
+popd
+
+pushd DiamondExample-B
+$LAKE update
+init_git
+popd
+
+pushd DiamondExample-C
+sed_i s/v2/v1/ lakefile.toml
+sed_i s/add_left_comm/poorly_named_lemma/ DiamondExampleC/MainResult.lean
+$LAKE update
+init_git
+git tag v1
+sed_i s/v1/v2/ lakefile.toml
+sed_i s/poorly_named_lemma/add_left_comm/ DiamondExampleC/MainResult.lean
+$LAKE update
+git commit -am "use v2"
+git tag v2
+popd
+
+pushd DiamondExample-D
+sed_i s/v2/v1/ lakefile.toml
+$LAKE update
+init_git
+git tag v1
+sed_i s/v1/v2/ lakefile.toml
+$LAKE update
+git commit -am "use v2"
+git tag v2
+popd
+
+# ---
+# Main tests
+# ---
+
+cd DiamondExample-D
+
+# Test build succeeds on v1
+git switch v1 --detach
+test_run build
+
+# Test build fails on v2
+git switch v2 --detach
+test_err 'Unknown identifier `poorly_named_lemma`' build