XPost: linux.debian.bugs.dist

Source: ssreflect
Version: 2.3.0-1
Severity: minor
Tags: trixie sid ftbfs
User: [email protected]
Usertags: ftbfs-shuffle

Hi,

GNU Make now has a --shuffle option that simulates non-deterministic ordering of target prerequisites. See https://trofi.github.io/posts/238-new-make-shuffle-mode.html and also previous work in Debian by Santiago Vila: https://people.debian.org/~sanvila/make-shuffle/

This package fails to build with make --shuffle=reverse.
This is likely to be caused by a missing dependency in
debian/rules or an upstream Makefile.

More information about this mass bug filing is available at https://wiki.debian.org/qa.debian.org/FTBFS/Shuffle

Relevant part (hopefully):

make[2]: Entering directory '/build/reproducible-path/ssreflect-2.3.0/mathcomp'
Makefile.common:55: update target 'Makefile.coq' due to: target does not exist
/usr/bin/coq_makefile -f Make -o Makefile.coq
Makefile.common:149: update target 'doc' due to: target is .PHONY
mkdir -p _build_doc/
cp -r algebra/all_algebra.v algebra/archimedean.v algebra/countalg.v algebra/finalg.v algebra/fraction.v algebra/intdiv.v algebra/interval.v algebra/matrix.v algebra/mxalgebra.v algebra/mxpoly.v algebra/mxred.v algebra/polydiv.v algebra/poly.v algebra/

polyXY.v algebra/qpoly.v algebra/rat.v algebra/ring_quotient.v algebra/ssralg.v algebra/ssrint.v algebra/ssrnum.v algebra/vector.v algebra/zmodp.v algebra/sesquilinear.v algebra/spectral.v all/all.v character/all_character.v character/character.v
character/classfun.v character/inertia.v character/integral_char.v character/mxabelem.v character/mxrepresentation.v character/vcharacter.v field/algC.v field/algebraics_fundamentals.v field/algnum.v field/all_field.v field/closed_field.v field/
cyclotomic.v field/falgebra.v field/fieldext.v field/finfield.v field/galois.v field/qfpoly.v field/separable.v fingroup/action.v fingroup/all_fingroup.v fingroup/automorphism.v fingroup/fingroup.v fingroup/gproduct.v fingroup/morphism.v fingroup/perm.v
fingroup/presentation.v fingroup/quotient.v solvable/abelian.v solvable/all_solvable.v solvable/alt.v solvable/burnside_app.v solvable/center.v solvable/commutator.v solvable/cyclic.v solvable/extraspecial.v solvable/extremal.v solvable/finmodule.v
solvable/frobenius.v solvable/gfunctor.v solvable/gseries.v solvable/hall.v solvable/jordanholder.v solvable/maximal.v solvable/nilpotent.v solvable/pgroup.v solvable/primitive_action.v solvable/sylow.v ssreflect/all_ssreflect.v ssreflect/bigop.v
ssreflect/binomial.v ssreflect/choice.v ssreflect/div.v ssreflect/eqtype.v ssreflect/finfun.v ssreflect/fingraph.v ssreflect/finset.v ssreflect/fintype.v ssreflect/generic_quotient.v ssreflect/order.v ssreflect/path.v ssreflect/prime.v ssreflect/seq.v
ssreflect/ssrAC.v ssreflect/ssrbool.v ssreflect/ssreflect.v ssreflect/ssrfun.v ssreflect/ssrmatching.v ssreflect/ssrnat.v ssreflect/ssrnotations.v ssreflect/tuple.v -t _build_doc/ --parents

cp Make Makefile* _build_doc
mkdir -p _build_doc/htmldoc
. ../etc/utils/builddoc_lib.sh; \
cd _build_doc && mangle_sources algebra/all_algebra.v algebra/archimedean.v algebra/countalg.v algebra/finalg.v algebra/fraction.v algebra/intdiv.v algebra/interval.v algebra/matrix.v algebra/mxalgebra.v algebra/mxpoly.v algebra/mxred.v algebra/

polydiv.v algebra/poly.v algebra/polyXY.v algebra/qpoly.v algebra/rat.v algebra/ring_quotient.v algebra/ssralg.v algebra/ssrint.v algebra/ssrnum.v algebra/vector.v algebra/zmodp.v algebra/sesquilinear.v algebra/spectral.v all/all.v character/all_
character.v character/character.v character/classfun.v character/inertia.v character/integral_char.v character/mxabelem.v character/mxrepresentation.v character/vcharacter.v field/algC.v field/algebraics_fundamentals.v field/algnum.v field/all_field.v
field/closed_field.v field/cyclotomic.v field/falgebra.v field/fieldext.v field/finfield.v field/galois.v field/qfpoly.v field/separable.v fingroup/action.v fingroup/all_fingroup.v fingroup/automorphism.v fingroup/fingroup.v fingroup/gproduct.v fingroup/
morphism.v fingroup/perm.v fingroup/presentation.v fingroup/quotient.v solvable/abelian.v solvable/all_solvable.v solvable/alt.v solvable/burnside_app.v solvable/center.v solvable/commutator.v solvable/cyclic.v solvable/extraspecial.v solvable/extremal.v
solvable/finmodule.v solvable/frobenius.v solvable/gfunctor.v solvable/gseries.v solvable/hall.v solvable/jordanholder.v solvable/maximal.v solvable/nilpotent.v solvable/pgroup.v solvable/primitive_action.v solvable/sylow.v ssreflect/all_ssreflect.v
ssreflect/bigop.v ssreflect/binomial.v ssreflect/choice.v ssreflect/div.v ssreflect/eqtype.v ssreflect/finfun.v ssreflect/fingraph.v ssreflect/finset.v ssreflect/fintype.v ssreflect/generic_quotient.v ssreflect/order.v ssreflect/path.v ssreflect/prime.v
ssreflect/seq.v ssreflect/ssrAC.v ssreflect/ssrbool.v ssreflect/ssreflect.v ssreflect/ssrfun.v ssreflect/ssrmatching.v ssreflect/ssrnat.v ssreflect/ssrnotations.v ssreflect/tuple.v

cd _build_doc && /usr/bin/make -f Makefile.coq --no-print-directory
COQDEP VFILES
Makefile.coq:416: update target 'all' due to: target is .PHONY
/usr/bin/make --no-print-directory -f "Makefile.coq" pre-all Makefile.coq:483: update target 'pre-all' due to: target is .PHONY
# Extension point
if [ "8.20.1" != "8.20.1" ]; then\
echo "W: This Makefile was generated by Coq 8.20.1";\
echo "W: while the current Coq version is 8.20.1";\
fi
/usr/bin/make --no-print-directory -f "Makefile.coq" real-all Makefile.coq:817: update target 'ssreflect/ssrnotations.vo' due to: target does not exist
echo ""COQC ssreflect/ssrnotations.v
COQC ssreflect/ssrnotations.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrnotations.v

true
Makefile.coq:817: update target 'ssreflect/ssreflect.vo' due to: target does not exist
echo ""COQC ssreflect/ssreflect.v
COQC ssreflect/ssreflect.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssreflect.v

true
Makefile.coq:817: update target 'ssreflect/ssrfun.vo' due to: target does not exist
echo ""COQC ssreflect/ssrfun.v
COQC ssreflect/ssrfun.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrfun.v

true
Makefile.coq:817: update target 'ssreflect/ssrbool.vo' due to: target does not exist
echo ""COQC ssreflect/ssrbool.v
COQC ssreflect/ssrbool.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrbool.v

true
Makefile.coq:817: update target 'ssreflect/eqtype.vo' due to: target does not exist
echo ""COQC ssreflect/eqtype.v
COQC ssreflect/eqtype.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/eqtype.v

true
Makefile.coq:817: update target 'ssreflect/ssrnat.vo' due to: target does not exist
echo ""COQC ssreflect/ssrnat.v
COQC ssreflect/ssrnat.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrnat.v

true
Makefile.coq:817: update target 'ssreflect/seq.vo' due to: target does not exist
echo ""COQC ssreflect/seq.v
COQC ssreflect/seq.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/seq.v

true
Makefile.coq:817: update target 'ssreflect/path.vo' due to: target does not exist
echo ""COQC ssreflect/path.v
COQC ssreflect/path.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/path.v

true
Makefile.coq:817: update target 'ssreflect/div.vo' due to: target does not exist
echo ""COQC ssreflect/div.v
COQC ssreflect/div.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/div.v

true
Makefile.coq:817: update target 'ssreflect/choice.vo' due to: target does not exist
echo ""COQC ssreflect/choice.v
COQC ssreflect/choice.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/choice.v

true
Makefile.coq:817: update target 'ssreflect/fintype.vo' due to: target does not exist
echo ""COQC ssreflect/fintype.v
COQC ssreflect/fintype.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/fintype.v

true
Makefile.coq:817: update target 'ssreflect/tuple.vo' due to: target does not exist
echo ""COQC ssreflect/tuple.v
COQC ssreflect/tuple.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/tuple.v

true
Makefile.coq:817: update target 'ssreflect/ssrmatching.vo' due to: target does not exist
echo ""COQC ssreflect/ssrmatching.v
COQC ssreflect/ssrmatching.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrmatching.v

true
Makefile.coq:817: update target 'ssreflect/finfun.vo' due to: target does not exist
echo ""COQC ssreflect/finfun.v
COQC ssreflect/finfun.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/finfun.v

true
Makefile.coq:817: update target 'ssreflect/bigop.vo' due to: target does not exist
echo ""COQC ssreflect/bigop.v
COQC ssreflect/bigop.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/bigop.v

true
Makefile.coq:817: update target 'ssreflect/ssrAC.vo' due to: target does not exist
echo ""COQC ssreflect/ssrAC.v
COQC ssreflect/ssrAC.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/ssrAC.v

true
Makefile.coq:817: update target 'ssreflect/prime.vo' due to: target does not exist
echo ""COQC ssreflect/prime.v
COQC ssreflect/prime.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/prime.v

true
Makefile.coq:817: update target 'ssreflect/finset.vo' due to: target does not exist
echo ""COQC ssreflect/finset.v
COQC ssreflect/finset.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/finset.v

true
Makefile.coq:817: update target 'ssreflect/order.vo' due to: target does not exist
echo ""COQC ssreflect/order.v
COQC ssreflect/order.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/order.v

File "./ssreflect/order.v", line 3523, characters 0-76:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 4700, characters 0-159:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 4715, characters 0-99:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 4747, characters 0-88:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 4759, characters 0-95:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 6060, characters 0-64:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./ssreflect/order.v", line 6117, characters 0-64:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
true
Makefile.coq:817: update target 'ssreflect/generic_quotient.vo' due to: target does not exist
echo ""COQC ssreflect/generic_quotient.v
COQC ssreflect/generic_quotient.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/generic_quotient.v

true
Makefile.coq:817: update target 'ssreflect/fingraph.vo' due to: target does not exist
echo ""COQC ssreflect/fingraph.v
COQC ssreflect/fingraph.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/fingraph.v

true
Makefile.coq:817: update target 'ssreflect/binomial.vo' due to: target does not exist
echo ""COQC ssreflect/binomial.v
COQC ssreflect/binomial.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/binomial.v

true
Makefile.coq:817: update target 'ssreflect/all_ssreflect.vo' due to: target does not exist
echo ""COQC ssreflect/all_ssreflect.v
COQC ssreflect/all_ssreflect.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp ssreflect/all_ssreflect.v

true
Makefile.coq:817: update target 'algebra/ssralg.vo' due to: target does not exist
echo ""COQC algebra/ssralg.v
COQC algebra/ssralg.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp algebra/ssralg.v

File "./algebra/ssralg.v", line 4601, characters 0-88:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./algebra/ssralg.v", line 4988, characters 0-77:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./algebra/ssralg.v", line 5016, characters 0-58:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
true
Makefile.coq:817: update target 'algebra/countalg.vo' due to: target does not exist
echo ""COQC algebra/countalg.v
COQC algebra/countalg.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp algebra/countalg.v

true
Makefile.coq:817: update target 'algebra/poly.vo' due to: target does not exist
echo ""COQC algebra/poly.v
COQC algebra/poly.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp algebra/poly.v

File "./algebra/poly.v", line 2955, characters 0-88:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
File "./algebra/poly.v", line 2957, characters 0-91:
Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]
true
Makefile.coq:817: update target 'fingroup/fingroup.vo' due to: target does not exist
echo ""COQC fingroup/fingroup.v
COQC fingroup/fingroup.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp fingroup/fingroup.v

true
Makefile.coq:817: update target 'fingroup/morphism.vo' due to: target does not exist
echo ""COQC fingroup/morphism.v
COQC fingroup/morphism.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp fingroup/morphism.v

true
Makefile.coq:817: update target 'fingroup/perm.vo' due to: target does not exist
echo ""COQC fingroup/perm.v
COQC fingroup/perm.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp fingroup/perm.v

true
Makefile.coq:817: update target 'fingroup/automorphism.vo' due to: target does not exist
echo ""COQC fingroup/automorphism.v
COQC fingroup/automorphism.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp fingroup/automorphism.v

true
Makefile.coq:817: update target 'fingroup/quotient.vo' due to: target does not exist
echo ""COQC fingroup/quotient.v
COQC fingroup/quotient.v
"/usr/bin/////coqc" -q '-w' '-projection-no-head-constant' '-w' '-redundant-canonical-projection' '-w' '-notation-overridden' '-w' '+duplicate-clear' '-w' '-ambiguous-paths' '-w' '+non-primitive-record' '-w' '+undeclared-scope' '-w' '+deprecated-

hint-without-locality' '-w' '+deprecated-hint-rewrite-without-locality' '-w' '-elpi.add-const-for-axiom-or-sectionvar' '-w' '-opaque-let' '-w' '-argument-scope-delimiter' '-w' '-overwriting-delimiting-key' '-w' '-closed-notation-not-level-0' '-w' '-
postfix-notation-not-level-1' "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -I . -R . mathcomp fingroup/quotient.v

true
Makefile.coq:817: update target 'fingroup/action.vo' due to: target does not exist
echo ""COQC fingroup/action.v
COQC fingroup/action.v

[continued in next message]

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)