Bonjour à tous
Ma demande concerne le package coq.
coq est un assistant de preuve développé par l'inria. http://coq.inria.fr/
La version actuelle est la 8.2.
Actuellement il est uniquement disponible dans AUR mais il me semble qu'il mériterait d'être dans un répertoire stable. C'est un des plus gros projets d'assistant de preuve et il est utilisé par beaucoup de monde -parmi les chercheurs -.
Pensez-vous qu'il serait possible de l'intégrer dans le dépôt archlinuxfr?
J'ai essayé de demander pour community ou autre mais on m'a répondu qu'il n'avait pas assez de votes (ce n'est pourtant pas sa faute s'il y a si peu de chercheurs ).
Merci!
j'ai essayé de le compiler (c'est effectivement très long), mais j'ai ces erreurs à la fin :
install: ne peut évaluer `bin/coqide.byte': Aucun fichier ou dossier de ce type
install: ne peut évaluer `bin/coqide.opt': Aucun fichier ou dossier de ce type
make[1]: *** [install-ide-opt] Erreur 1
make[1]: quittant le répertoire « /tmp/yaourt-tmp-eric/aur-coq/coq/src/coq-8.2-1 »
Si tu arrives à le builder correctement, tu pourras toujours le mettre sur le dépot [archlinuxfr] (il est pas mal utilisé), on te montrera comment ça marche (ou alors on le fera pour toi ).
Effectivement, dans community il y a seulement les paquets récoltants un certains nombre de voix (entre autres)
farvardin a écrit :j'ai essayé de le compiler (c'est effectivement très long), mais j'ai ces erreurs à la fin :
install: ne peut évaluer `bin/coqide.byte': Aucun fichier ou dossier de ce type
install: ne peut évaluer `bin/coqide.opt': Aucun fichier ou dossier de ce type
make[1]: *** [install-ide-opt] Erreur 1
make[1]: quittant le répertoire « /tmp/yaourt-tmp-eric/aur-coq/coq/src/coq-8.2-1 »
Salut, désolé pour le déterrage mais j'ai le même problème.
As-tu réussi à le résoudre depuis le temps ?
EDIT: Bon au final j'ai édité le PKGBUILD pour appeller le ./configure avec l'option « -coqide no ».
Si y'a une solution propre hésitez pas à le dire ! (même si j'aurais probablement la flemme de rebuild)
). 