Nix: installation de ssreflect

Question

J'utilise Coq (versions 8.5-6), installé avec Nix. Je veux installer ssreflect, de préférence aussi w/Nix. La seule information que j'ai trouvé à ce sujet est here. Cependant, il ne s'agit pas d'installer ssreflect, mais simplement de l'essayer. Néanmoins, j'ai essayé de l'essayer, mais je me suis retrouvé avec des centaines d'avertissements (sur le contenu de divers fichiers .v et .ml4) et je ne pouvais pas attendre la fin du processus. Un avertissement assez typique ressemblait à ceci:

Fichier "./algebra/ssralg.v", ligne 856, caractères 0-39: Attention: Arguments implicites est dépréciées; utiliser des arguments à la place

La question: Comment diable puis-je installer ssreflect w/Nix?

EDIT: Après avoir lu les commentaires de ejgallego, il semble qu'il peut être impossible d'installer ssreflect w/Nix - esp. Si l'on veut installer, il suffit de refaire abstraction des autres modules (fingroup, algebra, etc.). Donc, j'ai aussi la question suivante:

L'installation standard Opam ou make install de ssreflect fonctionnerait-elle avec un Coq installé par Nix?

Answer 1

Il y a quelques choses que vous devez être au courant:

• Nix est un gestionnaire de paquets source avec un cache binaire. Beaucoup de paquets sont préconstruits et disponibles dans le cache binaire, ainsi leur installation ne prend pas longtemps; certains paquets (en particulier les bibliothèques de développement) ne sont pas pré-compilés et Nix, lors de leur installation, prendra le temps nécessaire pour les compiler. S'il vous plaît soyez patient: il vous suffira d'attendre la compilation complète la première fois (et oui, math-comp émet beaucoup d'avertissement lors de la compilation); Les prochaines fois, le package sera déjà disponible dans votre magasin Nix local.

• Puisque OPAM est également basé sur la source, l'utilisation d'OPAM au lieu de Nix ne vous fera pas gagner du temps. Vous ne pouvez pas mélanger le Coq installé par Nix avec le SSReflect installé par OPAM car ce dernier voudra que le premier soit une dépendance à l'OPAM. La façon Nix d'utiliser les bibliothèques n'est pas de les installer mais de les charger avec nix-shell à la place. nix-shell va "installer" les bibliothèques et définir certaines variables d'environnement pour vous (par exemple $COQPATH dans ce cas).

• Vous pouvez également compiler le paquet de la source même à l'aide d'un Coq Nix installé mais vous ne pouvez pas exécuter make install parce que cela tenterait d'installer ssreflect au même endroit où Coq est installé, mais le magasin Nix est non-mutables. Au lieu de cela, vous pouvez ignorer cette étape et configurer manuellement $COQPATH.

• En effet, la compilation de la maquette mathématique complète prend beaucoup de temps. Il existe un paquet Coq ssreflect plus léger. Vous pouvez l'obtenir à l'aide:

  nix-shell -p coqPackages_8_6.ssreflect