Empêcher Opam de créer et conserver certains fichiers.

Lu’!

Pour les besoins d’une soumission, j’ai préparé une machine virtuelle pour que les reviewers aient tous les outils dispo pour vérifier que mes résultats sont corrects. Et du coup, j’essaie de me débrouiller pour que tout ça soit le plus léger possible pour ne pas avoir un fichier de 2 tonnes à stocker en ligne.

Du coup, je me suis penché un peu sur ce qui occupe de la place dans la VM, et il s’avère que ce qui prend le plus de place si on retire le système que j’ai nettoyé au maximum, c’est le monstre Opam. Juste avec Coq, Why3 et Alt-ergo, cet enfoiré pèse bien son Giga, sachant que j’ai déjà viré quelques trucs dedans (notamment les sources dont je n’ai plus besoin).

Reste qu’après avoir jeté un oeil, il semble y avoir encore des trucs dont je n’ai pas besoin dans une VM pour laquelle je me contente d’exécuter les softs qui sont dans Opam.

Typiquement :

• les fichiers bytecode,
• des fichiers qui semblent être là pour lier des logiciels à la compilation (? les CMX, CMI ?).

Du coup, je me demandais s’il y avait moyen de dire à Opam de rester le plus light possible en ne conservant rien ou presque, ou est ce qu’il va falloir que j’aille gentiment supprimer tout ça à la main ?

Notes :

• je ne sais pas si c’est l’endroit le plus approprié pour ce post, mais il semblait que c’était plus une question système que programmation,
• peut être que j’aurai plutôt dû faire un docker, mais je ne sais pas si c’est encore répandu pour les reviewers d’utiliser ça.

La question est sans doute naïve, mais tu ne peux pas juste fournir un « Opamfile » ou un truc du genre, qui dirait à Opam quoi télécharger et builder, sans avoir besoin que ce soit dans ta VM a priori ?

Moi ça m’arrangerait mais je ne suis pas sûr que les reviewers vont être très heureux d’attendre la recompilation de Coq sur la VM, parce que ça prend véritablement des plombes. L’autre problème, c’est que j’ai un autre soft, qui est compilé à part et qui dépend d’une partie des choses qu’il y a dans Opam (et encore un autre qui n’est pas lié à Opam mais lui j’ai déjà nettoyé au max).

Est-ce que tu es seulement intéressé par le binaire ou bien les librairies t’intéressent aussi ?

Entre la version native et bytecode, tu peux supprimé manuellement les fichiers bytecode si tu ne t’en sers pas, non ?

(1) Je pensais que les binaires me suffiraient mais en fait non. Par exemple, pour l’utilisateur puisse ouvrir CoqIDE, il a besoin de certains CMXS. Galère. Du coup, j’ai retiré progressivement des choses en vérifiant que tout ce qui était prévu continue à marcher. Typiquement, les CMO, CMI, CMT, CMX, … et encore vachement d’autres fichiers dont on pourrait se demander pourquoi ils sont là par défaut . Le problème c’est que Coq a encore beaucoup de choses de son côté, les VOs et les GLOBs notamment et ça, je vois moyennement comment faire le tri sans tout péter. C’est énorme Coq en fait, genre, pire qu’Eclipse .

(2) Tout à fait, c’est ce que j’ai fait du coup. Mais je me demandais s’il existait quelque chose de plus standard dans Opam. Je trouve dommage qu’un utilisateur se retrouve avec ces éléments s’il n’en a pas besoin.

(1) Est-ce que tu es seulement intéressé par le binaire ou bien les librairies t’intéressent aussi ?

(2) Entre la version native et bytecode, tu peux supprimé manuellement les fichiers bytecode si tu ne t’en sers pas, non ?

(1) Je pensais que les binaires me suffiraient mais en fait non. Par exemple, pour l’utilisateur puisse ouvrir CoqIDE, il a besoin de certains CMXS. Galère. Du coup, j’ai retiré progressivement des choses en vérifiant que tout ce qui était prévu continue à marcher. Typiquement, les CMO, CMI, CMT, CMX, …

Quand tu développes en OCaml, c’est pratique car ça permet d’aller récupérer des informations de type sur les fonctions que tu utilises (c’est ce que fait ocaml-merlin). Les CMI, CMO et CMX sont en général utile si tu te sers du paquet comme librairie. Mais je suis d’accord pour dire que ce système hérité du C est un peu désuet.

et encore vachement d’autres fichiers dont on pourrait se demander pourquoi ils sont là par défaut .

Supprimer des CMI/CMX/CMO peut casser des choses, faut faire gaffe.

Le problème c’est que Coq a encore beaucoup de choses de son côté, les VOs et les GLOBs notamment et ça, je vois moyennement comment faire le tri sans tout péter.

Les VO sont les fichiers de preuves compilés. Si tu n’as pas besoin de toute la librairie standard, tu peux supprimer ceux qui ne t’intéressent pas. Coq fonctionne avec 0 fichier VO ou GLOB, mais alors il ne vient avec aucun théorème.

Je ne suis pas sûr que la comparaison soit adaptée.

C’est surtout que c’est la procédure recommandée pour installer ces softs, alors que tout le monde ne veut pas développer avec et juste les utiliser. Et dans ce cas, on se retrouve à charger les outils pour les dévs alors qu’on veut juste les outils d’utilisateur lambda.

Mais du coup, dans l’ensemble, ça répond à la question : Opam ne le permet pas directement.

C’est une question intéressante et je ne crois pas que les développeurs Coq se la soient posée.

(Évidemment je pense que ce serait moins chiant avec un fichier Docker; tu peux construire et distribuer l’image, mais même juste distribuer la recette qui est du pur texte et dont le contenu liste des paquets précisément versionnés.)

J’ai l’impression que les fichiers produits par Coq se compressent très bien, en particulier les .glob qui sont du texte, et les .cmxs produits par le compilateur OCaml. Par exemple si on prend theories/Reals, il pèse 26Mio sur ma machine, mais seulement 7Mio compressé avec zip. Voici donc une piste : si tu stockais seulement une version compressée du .opam dans ton image, et que tu le décompressais au vol quand l’utilisateur lance la machine virtuelle ?

Edit: en fait c’est un peu idiot comme suggestion, j’imagine que les images de machine virtuelles stockent déjà toutes leurs données de façon compressée, non ? Dans ce cas ça ne devrait rien changer.

Bon, 7z a 4.07.0.7z 4.07.0 passe mon .opam/4.07.0 de 1.8Gio à 258Mio, donc tu devrais essayer ça.

C’est quoi la répartition en taille entre Coq et Why3 ? Chez moi …lib/coq pèse seulement 270Mio, ça n’explique pas ton Gibioctet.

(Dans le dépôt Coq, le tiers du poids vient des .coq-native, on peut les supprimer si on est sûr de ne pas utiliser native_compute dans son travail.)

Apparemment, l’algo de compression utilisé par VirtualBox est suffisamment brutal pour que ça n’y change rien. Du coup, ça veut dire que ça se compresse bien quand même, donc que de toute façon, je ne pourrais pas y gagner beaucoup.

1Go, c’est pour .opam complet.

En gros les 4 trucs les plus lourds dans libs (donc il faut aussi compter les binaires en plus) sont Coq (270 Mo), Why3 (180 Mo), Ocaml (130 Mo), et Alt-Ergo (30 Mo). Après, j’ai aussi des dépendances pour Frama-C mais elles pèsent peanuts.

(Après, pour le docker, je ne sais pas si j’aurai pu en fait, j’ai une version non publique d’un outil que j’ai compilé sur-mesure pour avoir certains bugfixes qui en sont pas encore publics).

Mais quand tu dis que ton truc pèse 1Gio, c’est avant ou après la compression par VirtualBox ? Quelle est la taille de ton image compressée ? Parce que chez moi lib/coq pèse 270Mio avant la compression, et seulement 49Mio ensuite.

Avant. J’ai une image compressée finale qui fait à peu près 1.6Go au total. Il faut que je regarde de plus près quelle distrib utiliser. Après m’être tapé la tête contre les murs avec des debian testing qui n’acceptaient de lancer le bureau que si je forçais la suppression de certains fichiers (tout gestionnaire confondu), j’ai fini par jeter mon dévolu sur une Lubuntu que j’ai dépouillée au maximum mais on peut faire mieux je pense (il faudrait que je crâme les fonts par exemple).

Si l’ensemble prend 1.6Gio compressé alors que Coq pèse 260Mio (compressé), j’ai l’impression que le coût est ailleurs et que ça ne sert pas à grand chose de jouer à l’apprenti-sorcier sur les fichiers de Coq ou Why3. Peut-être regarder une autre technologie pour la reproductibilité ?

Le problème étant d’avoir un truc aisément acceptable pour les reviewers. Et suffisamment flexible pour y mettre du soft pas encore ouvert sans se prendre la tête.