search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

I nixified this: https://github.com/jorsn/infotheo/tree/nixify #57

Open jorsn opened 3 years ago

jorsn commented 3 years ago

Hi! I am excited to see a formal proof lib for information theory!

If I manage to find the time, I will try to apply it to some proofs about multi-user identification. Therefore I nixified this: https://github.com/jorsn/infotheo/tree/nixify. The most recent build from there is also cached in my cachix cache (run cachix use jorsn).

If you are interested in using nix, I can create a PR and perhaps write a usage note for the README. If not, feel free to close this issue. Whether I can maintain the nix stuff (and add it to nixpkgs) depends on whether I will expect to really use it for longer.

affeldt-aist commented 3 years ago

Thank you for your interest

We were planning to look into the automated nix support provided by the coq-community https://github.com/coq-community/coq-nix-toolbox