Bug#850925: coq-highschoolgeometry: FTBFS: Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]).
Chris Lamb
lamby at debian.org
Wed Jan 11 10:07:40 UTC 2017
Source: coq-highschoolgeometry
Version: 8.4+20150620-1
Severity: serious
Justification: fails to build from source
User: reproducible-builds at lists.alioth.debian.org
Usertags: ftbfs
X-Debbugs-Cc: reproducible-bugs at lists.alioth.debian.org
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
`. `'` lamby at debian.org / chris-lamb.co.uk
`-
-------------- next part --------------
A non-text attachment was scrubbed...
Name: coq-highschoolgeometry.8.4+20150620-1.unstable.amd64.log.txt.gz
Type: application/octet-stream
Size: 9701 bytes
Desc: not available
URL: <http://lists.alioth.debian.org/pipermail/reproducible-bugs/attachments/20170111/b114c89e/attachment-0001.obj>
More information about the Reproducible-bugs
mailing list