Skip to content

Commit 06e3469

Browse files
proux01proux01
committed
Compile without Stdlib
1 parent 9d635b5 commit 06e3469

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

71 files changed

+227
-7028
lines changed

‎.github/workflows/main.yml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,7 @@ jobs:
1818
fail-fast: false
1919
matrix:
2020
coq_version:
21-
- '8.18'
22-
- '8.19'
23-
- '8.20'
21+
- '9.0'
2422
steps:
2523
- uses: actions/checkout@v2
2624
- uses: coq-community/docker-coq-action@v1

‎.github/workflows/nix-action-coq-8.18.yml‎

Lines changed: 0 additions & 2056 deletions
This file was deleted.

‎.github/workflows/nix-action-coq-8.19.yml‎

Lines changed: 0 additions & 2416 deletions
This file was deleted.

‎.github/workflows/nix-action-coq-8.20.yml‎

Lines changed: 0 additions & 2342 deletions
This file was deleted.

‎.nix/config.nix‎

Lines changed: 1 addition & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
{
22
format = "1.0.0";
33
attribute = "hierarchy-builder";
4-
default-bundle = "coq-8.20";
4+
default-bundle = "coq-9.0";
55
bundles = let
66
mcHBcommon = {
77
mathcomp.override.version = "master";
@@ -36,24 +36,6 @@
3636
coq-elpi.override.elpi-version = "2.0.7";
3737
};
3838

39-
"coq-8.20".coqPackages = mcHBcommon // {
40-
coq.override.version = "8.20";
41-
coq-elpi.override.version = "master";
42-
coq-elpi.override.elpi-version = "2.0.7";
43-
};
44-
45-
"coq-8.19".coqPackages = mcHBcommon // {
46-
coq.override.version = "8.19";
47-
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
48-
};
49-
50-
"coq-8.18".coqPackages = mcHBcommon // {
51-
coq.override.version = "8.18";
52-
mathcomp-classical.job = false; # Analysis master dropped suppor for 8.18
53-
mathcomp-analysis.job = false;
54-
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
55-
};
56-
5739
};
5840
cachix.coq = {};
5941
cachix.coq-community = {};

‎Changelog.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
# Changelog
22

3+
## Unreleased
4+
5+
Drop support for Coq 8.18, 8.19 and 8.20
6+
37
## [1.8.1] - 2025-01-25
48

59
Compatible with

‎HB/common/compat_acc_clauses_816.elpi‎

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎HB/common/compat_add_secvar_18_19.elpi‎

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎HB/structures.v‎

Lines changed: 35 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
(* Support constants, to be kept in sync with shim/structures.v *)
2-
From Coq Require Import String ssreflect ssrfun.
3-
Export String.StringSyntax.
2+
From Corelib Require Import ssreflect ssrfun.
43

54
Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
65
Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
@@ -300,11 +299,9 @@ Elpi Accumulate Db hb.db.
300299
Elpi Accumulate File "HB/common/stdpp.elpi".
301300
Elpi Accumulate File "HB/common/utils.elpi".
302301
Elpi Accumulate File "HB/common/database.elpi".
303-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
304-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
302+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
305303
Elpi Accumulate File "HB/common/log.elpi".
306-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
307-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
304+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
308305
Elpi Accumulate File "HB/about.elpi".
309306
Elpi Accumulate lp:{{
310307

@@ -335,10 +332,8 @@ Elpi Export HB.about.
335332
Elpi Accumulate Db hb.db.
336333
Elpi Accumulate File "HB/common/stdpp.elpi".
337334
Elpi Accumulate File "HB/common/database.elpi".
338-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
339-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
340-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
341-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
335+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
336+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
342337
Elpi Accumulate File "HB/common/utils.elpi".
343338
Elpi Accumulate File "HB/common/log.elpi".
344339
Elpi Accumulate File "HB/about.elpi".
@@ -379,11 +374,9 @@ Elpi Export HB.howto.
379374
Elpi Accumulate Db hb.db.
380375
Elpi Accumulate File "HB/common/stdpp.elpi".
381376
Elpi Accumulate File "HB/common/database.elpi".
382-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
383-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
377+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
384378
Elpi Accumulate File "HB/common/log.elpi".
385-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
386-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
379+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
387380
Elpi Accumulate File "HB/common/utils.elpi".
388381
Elpi Accumulate File "HB/status.elpi".
389382
Elpi Accumulate lp:{{
@@ -411,10 +404,8 @@ tred file.dot | xdot -
411404
Elpi Accumulate Db hb.db.
412405
Elpi Accumulate File "HB/common/stdpp.elpi".
413406
Elpi Accumulate File "HB/common/database.elpi".
414-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
415-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
416-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
417-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
407+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
408+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
418409
Elpi Accumulate File "HB/common/utils.elpi".
419410
Elpi Accumulate File "HB/common/log.elpi".
420411
Elpi Accumulate File "HB/graph.elpi".
@@ -462,10 +453,8 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
462453
Elpi Accumulate Db hb.db.
463454
Elpi Accumulate File "HB/common/stdpp.elpi".
464455
Elpi Accumulate File "HB/common/database.elpi".
465-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
466-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
467-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
468-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
456+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
457+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
469458
Elpi Accumulate File "HB/common/utils.elpi".
470459
Elpi Accumulate File "HB/common/log.elpi".
471460
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -546,10 +535,8 @@ Elpi Tactic HB.pack_for.
546535
Elpi Accumulate Db hb.db.
547536
Elpi Accumulate File "HB/common/stdpp.elpi".
548537
Elpi Accumulate File "HB/common/database.elpi".
549-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
550-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
551-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
552-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
538+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
539+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
553540
Elpi Accumulate File "HB/common/utils.elpi".
554541
Elpi Accumulate File "HB/common/log.elpi".
555542
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -571,10 +558,8 @@ Elpi Tactic HB.pack.
571558
Elpi Accumulate Db hb.db.
572559
Elpi Accumulate File "HB/common/stdpp.elpi".
573560
Elpi Accumulate File "HB/common/database.elpi".
574-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
575-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
576-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
577-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
561+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
562+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
578563
Elpi Accumulate File "HB/common/utils.elpi".
579564
Elpi Accumulate File "HB/common/log.elpi".
580565
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -649,10 +634,8 @@ HB.structure Definition StructureName params :=
649634
Elpi Accumulate Db hb.db.
650635
Elpi Accumulate File "HB/common/stdpp.elpi".
651636
Elpi Accumulate File "HB/common/database.elpi".
652-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
653-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
654-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
655-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
637+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
638+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
656639
Elpi Accumulate File "HB/common/utils.elpi".
657640
Elpi Accumulate File "HB/common/log.elpi".
658641
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -734,10 +717,8 @@ Elpi Export HB.structure.
734717
Elpi Accumulate Db hb.db.
735718
Elpi Accumulate File "HB/common/stdpp.elpi".
736719
Elpi Accumulate File "HB/common/database.elpi".
737-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
738-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
739-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
740-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
720+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
721+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
741722
Elpi Accumulate File "HB/common/utils.elpi".
742723
Elpi Accumulate File "HB/common/log.elpi".
743724
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -786,10 +767,8 @@ HB.instance Definition N Params := Factory.Build Params T …
786767
Elpi Accumulate Db hb.db.
787768
Elpi Accumulate File "HB/common/stdpp.elpi".
788769
Elpi Accumulate File "HB/common/database.elpi".
789-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
790-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
791-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
792-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
770+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
771+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
793772
Elpi Accumulate File "HB/common/utils.elpi".
794773
Elpi Accumulate File "HB/common/log.elpi".
795774
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -830,10 +809,8 @@ Elpi Export HB.instance.
830809
Elpi Accumulate Db hb.db.
831810
Elpi Accumulate File "HB/common/stdpp.elpi".
832811
Elpi Accumulate File "HB/common/database.elpi".
833-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
834-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
835-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
836-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
812+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
813+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
837814
Elpi Accumulate File "HB/common/utils.elpi".
838815
Elpi Accumulate File "HB/common/log.elpi".
839816
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -915,10 +892,8 @@ HB.end.
915892
Elpi Accumulate Db hb.db.
916893
Elpi Accumulate File "HB/common/stdpp.elpi".
917894
Elpi Accumulate File "HB/common/database.elpi".
918-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
919-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
920-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
921-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
895+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
896+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
922897
Elpi Accumulate File "HB/common/utils.elpi".
923898
Elpi Accumulate File "HB/common/log.elpi".
924899
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -958,10 +933,8 @@ Elpi Export HB.builders.
958933
Elpi Accumulate Db hb.db.
959934
Elpi Accumulate File "HB/common/stdpp.elpi".
960935
Elpi Accumulate File "HB/common/database.elpi".
961-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
962-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
963-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
964-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
936+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
937+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
965938
Elpi Accumulate File "HB/common/utils.elpi".
966939
Elpi Accumulate File "HB/common/log.elpi".
967940
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -1034,10 +1007,8 @@ Export Algebra.Exports.
10341007
Elpi Accumulate Db hb.db.
10351008
Elpi Accumulate File "HB/common/stdpp.elpi".
10361009
Elpi Accumulate File "HB/common/database.elpi".
1037-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1038-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1039-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1040-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
1010+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1011+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
10411012
Elpi Accumulate File "HB/common/utils.elpi".
10421013
Elpi Accumulate File "HB/common/log.elpi".
10431014
Elpi Accumulate File "HB/export.elpi".
@@ -1082,10 +1053,8 @@ Elpi Export HB.export.
10821053
Elpi Accumulate Db hb.db.
10831054
Elpi Accumulate File "HB/common/stdpp.elpi".
10841055
Elpi Accumulate File "HB/common/database.elpi".
1085-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1086-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1087-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1088-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
1056+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1057+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
10891058
Elpi Accumulate File "HB/common/utils.elpi".
10901059
Elpi Accumulate File "HB/common/log.elpi".
10911060
Elpi Accumulate File "HB/export.elpi".
@@ -1167,10 +1136,8 @@ HB.instance Definition _ : Ml ... T := ml.
11671136
Elpi Accumulate Db hb.db.
11681137
Elpi Accumulate File "HB/common/stdpp.elpi".
11691138
Elpi Accumulate File "HB/common/database.elpi".
1170-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1171-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1172-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1173-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
1139+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1140+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
11741141
Elpi Accumulate File "HB/common/utils.elpi".
11751142
Elpi Accumulate File "HB/common/log.elpi".
11761143
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -1205,10 +1172,8 @@ Elpi Export HB.declare.
12051172
Elpi Accumulate Db hb.db.
12061173
Elpi Accumulate File "HB/common/stdpp.elpi".
12071174
Elpi Accumulate File "HB/common/database.elpi".
1208-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1209-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1210-
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1211-
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
1175+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1176+
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
12121177
Elpi Accumulate File "HB/common/utils.elpi".
12131178
Elpi Accumulate File "HB/common/log.elpi".
12141179
Elpi Accumulate lp:{{
@@ -1246,8 +1211,3 @@ Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None)
12461211
Notation "`Error: t `is_not_canonically_a T" := (unify t _ (Some (is_not_canonically_a, T)))
12471212
(at level 0, T at level 0, format "`Error: t `is_not_canonically_a T", only printing) :
12481213
form_scope.
1249-
Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T)))
1250-
(at level 0, msg, T at level 0, format "`Error: t msg T", only printing) :
1251-
form_scope.
1252-
1253-
Global Open Scope string_scope.

‎Makefile‎

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,13 +25,14 @@ TGTS?=
2525
######################################################################
2626

2727
# local context: -----------------------------------------------------
28-
.PHONY: all config build only test-suite clean distclean __always__
28+
.PHONY: all config build only test-suite test-suite-stdlib clean distclean __always__
2929
.SUFFIXES:
3030

3131
H:= $(if $(VERBOSE),,@) # not used yet
3232
TOP = $(dir $(lastword $(MAKEFILE_LIST)))
3333
COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
3434
COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS)
35+
COQMAKE_TESTSUITE_STDLIB = $(MAKE) -f Makefile.test-suite-stdlib.coq $(COQMAKEOPTIONS)
3536
BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
3637
| wc -l | sed 's/ *//g')
3738

@@ -74,6 +75,11 @@ Makefile.coq: $(COQPROJECT) Makefile
7475
Makefile.test-suite.coq: $(COQPROJECT).test-suite Makefile
7576
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite -o Makefile.test-suite.coq
7677

78+
# Test suite Stdlib --------------------------------------------------
79+
80+
Makefile.test-suite-stdlib.coq: $(COQPROJECT).test-suite-stdlib Makefile
81+
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite-stdlib -o Makefile.test-suite-stdlib.coq
82+
7783
# Global config, build, clean and distclean --------------------------
7884
config: sub-config this-config
7985

@@ -83,12 +89,14 @@ only: sub-only this-only
8389

8490
test-suite: sub-test-suite this-test-suite
8591

92+
test-suite-stdlib: sub-test-suite-stdlib this-test-suite-stdlib
93+
8694
clean: sub-clean this-clean
8795

8896
distclean: sub-distclean this-distclean
8997

9098
# Local config, build, clean and distclean ---------------------------
91-
.PHONY: this-config this-build this-only this-test-suite this-distclean this-clean
99+
.PHONY: this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean
92100

93101
this-config:: __always__
94102

@@ -101,13 +109,18 @@ this-only:: this-config Makefile.coq
101109
this-test-suite:: build Makefile.test-suite.coq
102110
+$(COQMAKE_TESTSUITE)
103111

112+
this-test-suite-stdlib:: build Makefile.test-suite-stdlib.coq
113+
+$(COQMAKE_TESTSUITE_STDLIB)
114+
104115
this-distclean:: this-clean
105116
rm -f Makefile.coq Makefile.coq.conf
106117
rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf
118+
rm -f Makefile.test-suite-stdlib.coq Makefile.test-suite-stdlib.coq.conf
107119

108120
this-clean:: __always__
109121
@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
110122
@if [ -f Makefile.test-suite.coq ]; then $(COQMAKE_TESTSUITE) cleanall; fi
123+
@if [ -f Makefile.test-suite-stdlib.coq ]; then $(COQMAKE_TESTSUITE_STDLIB) cleanall; fi
111124

112125
# Install target -----------------------------------------------------
113126
.PHONY: install
@@ -141,5 +154,6 @@ endif
141154
structures.vo : %.vo: __always__ Makefile.coq
142155
+$(COQMAKE) $@
143156

144-
$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq
157+
$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq Makefile.test-suite-stdlib.coq
145158
+$(COQMAKE_TESTSUITE) $@
159+
+$(COQMAKE_TESTSUITE_stdlib) $@

0 commit comments

Comments
 (0)