From 521adf9a11f990c5c83ba518ed43243c73b984dc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Dec 2024 10:39:05 +0100 Subject: [PATCH 1/2] improve error message missing mixin dep --- HB/common/synthesis.elpi | 2 +- Makefile.test-suite.coq.local | 3 ++- tests/err_miss_dep.v | 6 ++++++ tests/err_miss_dep.v.out | 2 ++ 4 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 tests/err_miss_dep.v create mode 100644 tests/err_miss_dep.v.out diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index c596fc5c4..b0ca0d9d2 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -243,7 +243,7 @@ instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- factory-alias->gref TmGR M, std.mem! ML M, !, - mixin-for T M X, !, + if (mixin-for T M X) true (coq.error "Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, instantiate-all-these-mixin-args (F X) T ML R. instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !, @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m). diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index b69480aa0..23f814bff 100644 --- a/Makefile.test-suite.coq.local +++ b/Makefile.test-suite.coq.local @@ -23,4 +23,5 @@ post-all:: $(call DIFF, tests/howto.v) $(call DIFF, tests/missing_join_error.v) $(call DIFF, tests/not_same_key.v) - $(call DIFF, tests/hnf.v) \ No newline at end of file + $(call DIFF, tests/hnf.v) + $(call DIFF, tests/err_miss_dep.v) \ No newline at end of file diff --git a/tests/err_miss_dep.v b/tests/err_miss_dep.v new file mode 100644 index 000000000..3aa1a0263 --- /dev/null +++ b/tests/err_miss_dep.v @@ -0,0 +1,6 @@ +From HB Require Import structures. +HB.mixin Record IsAddComoid A := {}. +HB.structure Definition AddComoid := { A of IsAddComoid A }. +HB.mixin Record IsAbelianGrp A of IsAddComoid A := {}. +HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }. +Fail HB.mixin Record IsRing K of IsAbelianGrp K (*& IsAddComoid K*) := {}. diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out new file mode 100644 index 000000000..c8eeb6476 --- /dev/null +++ b/tests/err_miss_dep.v.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +Unable to find mixin err_miss_dep_IsAddComoid on subject K From 9d592eea5f2ed747b0b32afef6a3275a2e9bffac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Dec 2024 11:18:52 +0100 Subject: [PATCH 2/2] Apply suggestions from code review --- HB/common/synthesis.elpi | 2 +- tests/err_miss_dep.v.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index b0ca0d9d2..da322cd7d 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -243,7 +243,7 @@ instantiate-all-these-mixin-args (fun _ Tm F) T ML R :- factory-alias->gref TmGR M, std.mem! ML M, !, - if (mixin-for T M X) true (coq.error "Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, + if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !, instantiate-all-these-mixin-args (F X) T ML R. instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !, @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m). diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out index c8eeb6476..32784f55b 100644 --- a/tests/err_miss_dep.v.out +++ b/tests/err_miss_dep.v.out @@ -1,2 +1,2 @@ The command has indeed failed with message: -Unable to find mixin err_miss_dep_IsAddComoid on subject K +HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K