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

Parce que c'est gourmand en espace ces bêtes là.

L’auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

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.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

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 ?

Merida is so cool · “Now that I have built my very own hammer, nothing looks like a nail anymore. ”

+0 -0
Auteur du sujet

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).

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+1 -0

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 ?

+0 -0
Auteur du sujet

(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 ?

Saroupille

(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 O_o . 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 :lol: .

(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.

Édité par Ksass`Peuk

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

(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 ?

Saroupille

(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 O_o .

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.

C’est énorme Coq en fait, genre, pire qu’Eclipse :lol: .

Ksass`Peuk

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

Édité par Saroupille

+0 -0
Auteur du sujet

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.

Saroupille

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.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

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.

Édité par gasche

+0 -0

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.)

+0 -0
Auteur du sujet

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.

gasche

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.

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.

gasche

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).

Édité par Ksass`Peuk

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

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.

+0 -0
Auteur du sujet

Mais quand tu dis que ton truc pèse 1Gio, c’est avant ou après la compression par VirtualBox

gasche

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).

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0

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é ?

+0 -0
Auteur du sujet

Peut-être regarder une autre technologie pour la reproductibilité ?

gasche

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.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein [Tutoriel Frama-C WP]

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte