saleGauss: putain mais c'est pas possible. Tu es en stage de license/master à polytechnique ou quoi ???

« Si je me retrouver à devoir compiler Coq à la main, ça va être drôle :D » mon cobureau fait ça. C'est pas insurmontable, mais ça implique de connaître des devs Coq.

Pour ne rien te cacher, j'ai trouvé une distribution avec Coq 8.3 … le problème c'est que c'est Arch et qu'ils ont tendance à faire du chiffre d'abord, et à réfléchir après. Selon moi, le profil type de l'utilisateur de arch c'est le geek qui adore passer son temps à réparer sa machine plutôt qu'à l'utiliser, donc je te le déconseille vivement.

Ce que je peux faire, c'est attendre la sortie de la future Debian stable (prévue autour du 6 février) et contacter directement un des développeurd du paquet coq pour Debian afin d'avoir des infos précises sur la situation.

ouais désolé effectivement j'avais pas tout lu...

mais je trouve en général l'environnement linux plus propice à la programmation.

1. saleGauss Voir le profil de saleGauss
2. Posté le 26 janvier 2011 à 11:04:42 Avertir un administrateur
3. Les amis (_skip et Infestor), il faut lire un peu avant de poster s'il vous plait.

Mes problèmes sont bien plus compliqués que ça : je me moque de la vitesse de compilation de code C++.
Je n'utilise pas C++.

Content pour toi...
Je pensais que C/C++ t'intéressaient puisque tu parlais de minGW sous windows. Fin de la parenthèses, amuse-toi bien.

mingw met plus longtemps à compiler, d'accord, mais à la sortie ca donne quoi au niveau de l'exécutable? la question m'intéresse (pardon pour l'intervention HS )

gcc (et donc mingw) est probablement le compilateur le plus minable (en terme de performance) disponible sur le marche. N'importe quel autre compilateur compilera plus rapidement et fournira un binaire de meilleur qualite.

Le seul interet de GCC (AMHA) est qu'il fonctionne sur toute les architectures du monde. C'est pourquoi il est massivement utilise par la communaute du logiciel libre. Il permet de compiler opur n'importe quel architecture bizarre.

Puis surtout qu'il est gratuit . Moi c'est son debugger que je supporte mal.

_skip : tcc, pcc, et clang sont tout aussi gratuits.

C'est quoi que tu entends par "son debugger" ?
gdb marche raisonnablement bien. Par contre, il est extrêmement mal intégré dans les divers IDE (mais c'est la faute des IDEs). La seule GUI décente pour gdb que je connaisse reste le bon vieux ddd.

Je trouve qu'il est super lent et qu'il a tendance à souvent crasher et je suis loin d'être le seul. C'est clair que ça a le mérite d'exister mais c'est largement en dessous de ce que fait par exemple un msvc.

J'ai ete utilisateur de msvc pendant longtemps, et personnellement je ne trouve pas le debugger si bien que ca. Enfin, il est bien, mais je ne fais pas la difference avec gdb dans mes cas d'utilisation. La plupart du temps mes structures de donnees sont bine trop complique pour etre visualisable directement avec l'interface. Et j'appelle des fonctions interne a mon code qui affiche les informations dont j'ai besoin.

_skip : l'as tu seulement utilisé directement pour dire ça ?
Là, je ne peux m'empêcher de penser que tu me décris parfaitement l'interface de (disons) Code::Blocks qui, elle, est effectivement lente, boguée, et qui crache en permanence.

godrik : même pour des choses compliquée, on peut réussir à visualiser un peu avec ddd.

all : et si on continuait ça sur le blabla parce que là c'est HS ?

la suite de la discussion debugger ici: https://www.jeuxvideo.com/forums/1-47-46404-17-0-1-0-printf-blabla.htm#message_52647

Et si vous avez une autre discussion pas en lein avec la question original, blabla c'est bien aussi

Bon, comme l'a majorité me l'a conseillé, et comme je n'arrivais à rien avec mon open suse (j'ai tenté une installation à la main, et il me manquait 160 choses qui n'étaient bien sur pas dans mon gestionnaire de paquets), j'ai telechargé Mandriva One 2010.2 (32 bits).

Et là, c'est encore pire qu'avant.
J'ai lancé l'interface graphique du gestionnaire de paquets.
J'ai au premier demarrage choisit "gerer les paquets pour les MAJs et pour les autres applications".

J'ai choisis un miroir.

J'ai une liste de depots qui est cochée par defaut (que les "stables").
Je cherche ocaml. Rien, aucun resultat.

Je coche tous les depots (testins, debug, ...), je recherche ocaml, toujours rien. Pas une reponse.

Mes questions :
1) Existe-t'il un soft de recherche de paquets sur le web sous mandriva comme c'est le cas sous open suse ?
(Un soft qui permet de trouver le repository d'un paquet particulier).

2) Savez vous comment puis-je trouver le depot pour ocaml pour Mandriva ?

Franchement, soit j'ai un soucis d'utilisation des systemes, soit c'est vraiment de la mouise.

Je ne sais vraiment pas comment tu as fais, mais tu t'y es pris comme un manche. .
Le paquet existe bel et bien (dans main en plus, donc pas de case à cocher en plus dans l'interface de gestion des dépôts) :
ftp://https://www.jeuxvideo.com//ftp.free.fr/mirrors/ftp.mandriva.com/MandrivaLinux/official/current/i586/media/main/release/ocaml-3.11.2-3mdv2010.1.i586.rpm

NdM du 38: ce que j'ai fais est très mal. On ne doit pas piocher comme un sauvage directement dans le dépôt.

Incomprehensible, avec l'interface graphique, il ne me trouvait rien.
Et pourtant, il était bien reglé sur afficher "tous" (pas que les installés).

Et puis j'ai découvert la commande "urpmi", pour lancer le télechargement et l'installation d'un paquet.

Et là, il trouvait ocaml, camlp5, et tout ce dont j'avais besoin.

Merci à toi Chris pour ta réponse.

Je reposte dans quelques minutes pour donner une marche à suivre un peu détaillée pour ceux qui rencontreraient les même problemes que moi.

Tu ferais mieux de me dire quelle interface graphique tu as utilisée (ça pue la logithèque gnome à plein nez en tout cas).

MARCHE A SUIVRE POUR L'INSTALLATION DE COQ EN DERNIERE VERSION, pour ceux qui doivent impérativement utiliser la dernière.

Donc, vous avez vérifié, et votre gestionnaire de paquets de vous propose pas la dernière version de Coq (la 8.3pl1 au moment où j'écris ces lignes).

Vous devez :

0) Installer Make
------------------------------------
$su
Puis entrez votre mot de passe.
Hop, vous voila admin.
Puis :

1. urpmi make

1) Installer ocaml
--------------------
Si vous êtes sur Mandriva (et ça m'a l'air d'être un bon choix, j'ai jamais réussi vite à faire quelque chose sur un linux), faites :

1. urpmi ocaml

Si il vous demande si i doit installer aussi les dépendances, répondez bien sur oui.

2) Installer camlp5
-------------------------
Sur le meme terminal, faites :

1. urpmi camlp5

3) Installer lablgtk-2.0.
--------------------------
Faites

1. urpmi lablgtk-2.0

Il va vous dire que ce paquet n'existe pas, mais qu'il ressemble à deux autres (plus un troisième de docs, que je n'ai pas pris).
Faites donc

1. urpmi <nom1> <nom2>

4) Compilation de Coq et CoqIDE à partir de la dernière version des sources.

- Récuperez les sources sur http://coq.inria.fr/download
- L'extraire
- Se placer dans le répertoire obtenu.
- Faire

1. make cleanarch

- Faire

1. ./config

Il va vous dire dans les première lignes si tout est OK (Ocaml trouvé ! camlp5 trouvé ! lalblgtk trouvé ! pthread trouvé !) et si il peut donc installer Coq et CoqIDE.
Si tout n'est pas OK, et que vous avez pourtant bien suivi les première étapes, bon courage...
Il va vous demander de choisir le nom des répertoires pour les binaires, les libs...
on peut lui donner /usr/bin pour les binaires, /usr/lib/coq pour les lib, /usr/man pour les pages du manuel, and so on...

A la fin, relisez bien ce qu'il a affiché, et que tout est bien OK.

- Faites

1. make world 2>&1 > log.makeworld.0

Cette étape est longue !
Prenez le temps d'allez boir un café, ou de relire une page du CoqArt, ou les deux.

Si il vous sort des erreurs, bon courage.
Pensez à checker le log obtenu pour vérifier que tout semble OK.

NB : On obtient un "shift reduce conflit" sans importance.

Si tout est OK ici, normalement vous êtes (presque) sorti d'affaire.

- Faites

1. make install 2>&1 > log.makeinstall.0

Si cette étape echoue, avec des erreurs très etranges, comme "fichier1 and fichier2 make inconsistent assumtions over <nomD'interface>, bon courage.
J'en étais arrivé là sur openSuse, et j'ai choisi de formater...

Cette étape est assez rapide.
Checkez à la fin le log obtenu.

Bravo, c'est fini pour l'installation !

1. exit (pour sortir du mode admin lancé au tout debut)

$exit (pour quitter la console)
5) Lancer Coq ou CoqIDE
----------------------
$coqtop&
ou
$coqide&

Roulez !

Notons qu'il est probablement plus propre d'installer coq dans le repertoire de l'utilisateur courant.

Vu que ça parle pas mal de OCaml et d'outil OCaml, un outils qui peut aider c'est GODI. C'est un système de paquet multiplateforme prévu spécifiquement pour OCaml, ses lib et les programmes écrit avec (entre autre, je suis certain que Coq est dedans). Avec compilation depuis les sources.

Usuellement il y a les dernière version des programme qui sont packagé pour ça donc ça pourrait faire ce que tu veux. Moi je déteste, c'est un outils horrible qui a plein de problèmes. Mais il y a aussi plein de gens qui s'en servent et qui sont très content avec.

Je te conseille au moins d'y jeter un coup d'œil.

godrik : j'ai longtemps pensé la même chose que toi sur gcc. Mais depuis quels version, les optimisations qu'il fait son pas mal du tout. J'ai déjà fait des tests où il a produit du code plus efficace que icc (probablement plus par chance qu'autre chose, mais quand même). Et ça fait longtemps que je n'ai plus utilisé msvcc donc je ne peux plus trop comparer, mais l'écart entre ces trois compilo a probablement du se resserrer (sauf pour la génération de code SSE et Cie. probablement)

j'avais fait des test entre gcc et pcc (portland group) pour compiler du fortran et gcc etait clairement plus lent que pcc. Mais c'etait principalement pour des questions de vectorisations.

redhat a un benchmark comparant gcc 4 et icc 8.1 ( http://people.redhat.com/bkoz/benchmarks/ ) et globalement icc semble bien meilleur. En emem temps gcc 4 c'est super vieux.

J'ai access a une version recente du compilo intel (11.1), si quelqu'un connait un bon benchmark, je peux le faire tourner.