Source: coq-highschoolgeometry Version: 8.4+20150620-1 Severity: serious Justification: fails to build from source User: [email protected] Usertags: ftbfs X-Debbugs-Cc: [email protected]
Dear Maintainer,
coq-highschoolgeometry fails to build from source in unstable/amd64:
[…]
dh_auto_configure
dh_auto_build
make -j1
make[1]: Entering directory '«BUILDDIR»'
coqdep -c -glob -slash -R . HighSchoolGeometry "complements_cercle.v" >
"complements_cercle.v.d" || ( RV=$?; rm -f "complements_cercle.v.d"; exit ${RV}
)
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_analytique.v" >
"complexes_analytique.v.d" || ( RV=$?; rm -f "complexes_analytique.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_inversion.v" >
"complexes_inversion.v.d" || ( RV=$?; rm -f "complexes_inversion.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "contact.v" > "contact.v.d" ||
( RV=$?; rm -f "contact.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "equations_cercles.v" >
"equations_cercles.v.d" || ( RV=$?; rm -f "equations_cercles.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "inversion.v" >
"inversion.v.d" || ( RV=$?; rm -f "inversion.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "puissance_cercle.v" >
"puissance_cercle.v.d" || ( RV=$?; rm -f "puissance_cercle.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "transformations_contact.v" >
"transformations_contact.v.d" || ( RV=$?; rm -f "transformations_contact.v.d";
exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "vecteur.v" > "vecteur.v.d" ||
( RV=$?; rm -f "vecteur.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "trigo.v" > "trigo.v.d" || (
RV=$?; rm -f "trigo.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "similitudes_directes.v" >
"similitudes_directes.v.d" || ( RV=$?; rm -f "similitudes_directes.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Rutile.v" > "Rutile.v.d" || (
RV=$?; rm -f "Rutile.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "rotation_plane.v" >
"rotation_plane.v.d" || ( RV=$?; rm -f "rotation_plane.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "representant_unitaire.v" >
"representant_unitaire.v.d" || ( RV=$?; rm -f "representant_unitaire.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "repere_plan.v" >
"repere_plan.v.d" || ( RV=$?; rm -f "repere_plan.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "repere_ortho_plan.v" >
"repere_ortho_plan.v.d" || ( RV=$?; rm -f "repere_ortho_plan.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "reflexion_plane.v" >
"reflexion_plane.v.d" || ( RV=$?; rm -f "reflexion_plane.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "projection_orthogonale.v" >
"projection_orthogonale.v.d" || ( RV=$?; rm -f "projection_orthogonale.v.d";
exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "produit_scalaire.v" >
"produit_scalaire.v.d" || ( RV=$?; rm -f "produit_scalaire.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Plans_paralleles.v" >
"Plans_paralleles.v.d" || ( RV=$?; rm -f "Plans_paralleles.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Plan_espace.v" >
"Plan_espace.v.d" || ( RV=$?; rm -f "Plan_espace.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "parallelisme_concours.v" >
"parallelisme_concours.v.d" || ( RV=$?; rm -f "parallelisme_concours.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "orthogonalite.v" >
"orthogonalite.v.d" || ( RV=$?; rm -f "orthogonalite.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "orthogonalite_espace.v" >
"orthogonalite_espace.v.d" || ( RV=$?; rm -f "orthogonalite_espace.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "orthocentre.v" >
"orthocentre.v.d" || ( RV=$?; rm -f "orthocentre.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "operations_complexes.v" >
"operations_complexes.v.d" || ( RV=$?; rm -f "operations_complexes.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "milieu.v" > "milieu.v.d" || (
RV=$?; rm -f "milieu.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "metrique_triangle.v" >
"metrique_triangle.v.d" || ( RV=$?; rm -f "metrique_triangle.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "mesure_algebrique.v" >
"mesure_algebrique.v.d" || ( RV=$?; rm -f "mesure_algebrique.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "mediatrice.v" >
"mediatrice.v.d" || ( RV=$?; rm -f "mediatrice.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "isocele.v" > "isocele.v.d" ||
( RV=$?; rm -f "isocele.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "homoth_Euler.v" >
"homoth_Euler.v.d" || ( RV=$?; rm -f "homoth_Euler.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "homothetie_plane.v" >
"homothetie_plane.v.d" || ( RV=$?; rm -f "homothetie_plane.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "formes_complexes.v" >
"formes_complexes.v.d" || ( RV=$?; rm -f "formes_complexes.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Field_affine.v" >
"Field_affine.v.d" || ( RV=$?; rm -f "Field_affine.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "exercice_espace.v" >
"exercice_espace.v.d" || ( RV=$?; rm -f "exercice_espace.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "euclidien_classiques.v" >
"euclidien_classiques.v.d" || ( RV=$?; rm -f "euclidien_classiques.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "equations_droites.v" >
"equations_droites.v.d" || ( RV=$?; rm -f "equations_droites.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Droite_plan_espace.v" >
"Droite_plan_espace.v.d" || ( RV=$?; rm -f "Droite_plan_espace.v.d"; exit ${RV}
)
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "droite_Euler.v" >
"droite_Euler.v.d" || ( RV=$?; rm -f "droite_Euler.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "Droite_espace.v" >
"Droite_espace.v.d" || ( RV=$?; rm -f "Droite_espace.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "distance_euclidienne.v" >
"distance_euclidienne.v.d" || ( RV=$?; rm -f "distance_euclidienne.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "dilatations.v" >
"dilatations.v.d" || ( RV=$?; rm -f "dilatations.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "determinant.v" >
"determinant.v.d" || ( RV=$?; rm -f "determinant.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "coplanarite.v" >
"coplanarite.v.d" || ( RV=$?; rm -f "coplanarite.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry
"composee_translation_rotation.v" > "composee_translation_rotation.v.d" || (
RV=$?; rm -f "composee_translation_rotation.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "composee_transformations.v" >
"composee_transformations.v.d" || ( RV=$?; rm -f
"composee_transformations.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "composee_reflexions.v" >
"composee_reflexions.v.d" || ( RV=$?; rm -f "composee_reflexions.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "composee_dilatations.v" >
"composee_dilatations.v.d" || ( RV=$?; rm -f "composee_dilatations.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes.v" >
"complexes.v.d" || ( RV=$?; rm -f "complexes.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_transformations.v"
> "complexes_transformations.v.d" || ( RV=$?; rm -f
"complexes_transformations.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_similitudes.v" >
"complexes_similitudes.v.d" || ( RV=$?; rm -f "complexes_similitudes.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_exercice.v" >
"complexes_exercice.v.d" || ( RV=$?; rm -f "complexes_exercice.v.d"; exit ${RV}
)
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_dilatations.v" >
"complexes_dilatations.v.d" || ( RV=$?; rm -f "complexes_dilatations.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "complexes_conjugaison.v" >
"complexes_conjugaison.v.d" || ( RV=$?; rm -f "complexes_conjugaison.v.d"; exit
${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "cocyclicite.v" >
"cocyclicite.v.d" || ( RV=$?; rm -f "cocyclicite.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "cercle.v" > "cercle.v.d" || (
RV=$?; rm -f "cercle.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "barycentre.v" >
"barycentre.v.d" || ( RV=$?; rm -f "barycentre.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "applications_cocyclicite.v" >
"applications_cocyclicite.v.d" || ( RV=$?; rm -f
"applications_cocyclicite.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "angles_vecteurs.v" >
"angles_vecteurs.v.d" || ( RV=$?; rm -f "angles_vecteurs.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "angles_droites.v" >
"angles_droites.v.d" || ( RV=$?; rm -f "angles_droites.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "alignement.v" >
"alignement.v.d" || ( RV=$?; rm -f "alignement.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "aire_signee.v" >
"aire_signee.v.d" || ( RV=$?; rm -f "aire_signee.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqdep -c -glob -slash -R . HighSchoolGeometry "affine_classiques.v" >
"affine_classiques.v.d" || ( RV=$?; rm -f "affine_classiques.v.d"; exit ${RV} )
warning: option -slash has no effect and is deprecated.
coqc -dump-glob Rutile.glob -q -R . HighSchoolGeometry Rutile
coqc -dump-glob Field_affine.glob -q -R . HighSchoolGeometry Field_affine
File "./Field_affine.v", line 47, characters 0-85:
Warning: fcons is declared as a local axiom [local-declaration,scope]
coqc -dump-glob vecteur.glob -q -R . HighSchoolGeometry vecteur
coqc -dump-glob alignement.glob -q -R . HighSchoolGeometry alignement
File "./alignement.v", line 133, characters 19-20:
Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in
[vernac:tactic_command]).
Makefile:171: recipe for target 'alignement.vo' failed
make[1]: *** [alignement.vo] Error 1
make[1]: Leaving directory '«BUILDDIR»'
dh_auto_build: make -j1 returned exit code 2
debian/rules:4: recipe for target 'build' failed
make: *** [build] Error 2
dpkg-buildpackage: error: debian/rules build gave error exit status 2
[…]
The full build log is attached.
Regards,
--
,''`.
: :' : Chris Lamb
`. `'` [email protected] / chris-lamb.co.uk
`-
coq-highschoolgeometry.8.4+20150620-1.unstable.amd64.log.txt.gz
Description: Binary data
