From a60501b15f2528917d54bbf61e1459d4f082732d Mon Sep 17 00:00:00 2001 From: Tomas Vallejos Date: Tue, 23 Jul 2024 15:57:45 +0200 Subject: [PATCH 1/2] adding a link to a guide on how to declare mathcomp instances --- HB/howto.elpi | 3 ++- tests/howto.v.out | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index da46e4fbc..295aa959a 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -148,7 +148,8 @@ pp-solutions LLF :- str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):", {about.bulletize SLLF pp-solution}], % print - coq.say {coq.pp->string PpSolutions}, + coq.say {coq.pp->string PpSolutions}, + coq.say "For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances", coq.say. pred pp-solution i:list factoryname, o:coq.pp. diff --git a/tests/howto.v.out b/tests/howto.v.out index a83cbce85..2d1a61fd0 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -8,6 +8,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE @@ -15,6 +16,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_TYPE; Ring_of_AddAG - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE @@ -26,6 +28,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE @@ -33,6 +36,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_TYPE; Ring_of_AddAG - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances The command has indeed failed with message: HB: no solution found, try to increase search depth. @@ -41,15 +45,18 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_AddComoid; BiNearRing_of_AddMonoid - AddAG_of_AddComoid; Ring_of_AddAG - AddAG_of_AddComoid; SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid - Ring_of_AddAG - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid - Ring_of_AddAG - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: nothing to do. From 31d242fa20a01326915c33f03fefa7a81a0304f1 Mon Sep 17 00:00:00 2001 From: Tomas Vallejos Date: Wed, 24 Jul 2024 17:41:51 +0200 Subject: [PATCH 2/2] adding a blank line before suggesting the link --- HB/howto.elpi | 1 + tests/howto.v.out | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/HB/howto.elpi b/HB/howto.elpi index 295aa959a..7d6b6a23c 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -149,6 +149,7 @@ pp-solutions LLF :- {about.bulletize SLLF pp-solution}], % print coq.say {coq.pp->string PpSolutions}, + coq.say, coq.say "For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances", coq.say. diff --git a/tests/howto.v.out b/tests/howto.v.out index 2d1a61fd0..9afb95c2f 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -8,6 +8,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): @@ -16,6 +17,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_TYPE; Ring_of_AddAG - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): @@ -28,6 +30,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): @@ -36,6 +39,7 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_TYPE; Ring_of_AddAG - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances The command has indeed failed with message: @@ -45,18 +49,21 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_AddComoid; BiNearRing_of_AddMonoid - AddAG_of_AddComoid; Ring_of_AddAG - AddAG_of_AddComoid; SemiRing_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid - Ring_of_AddAG - SemiRing_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid - Ring_of_AddAG - SemiRing_of_AddComoid + For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances HB: nothing to do.