Motivation for this change

I'm writing my undergraduate thesis on Homotopy Type Theory 😄 But honestly, users of HoTT are becoming a larger and larger share of Coq users in general.

There's an issue with this package: because HoTT replaces the Coq standard library, it's difficult to use with vanilla coqc, coqtop, and related binaries. It provides its own (hoqc, hoqtop, etc.), but they expect to be in the same directory as the compiled *.vo files or for said files to be at /usr/share/hott. I've simply dropped the *.vo files into bin. I'm also open to symlinking them from a more standard directory.

Another issue is that the current version might not work with older versions of Coq. Is there a way to prevent it from building with e.g. coq_8_4?

You can test the build by running

nix-build -A coqPackages_8_6.HoTT

and then

./result/bin/hoqtop

and typing

Require Import HoTT.Categories.Category

You should get no error message, as opposed to when typing foo and getting

Coq < Require Import foo.
Toplevel input, characters 15-18:
> Require Import foo.
>                ^^^
Error: Unable to locate library foo.

Things done

• Tested using sandboxing (nix.useSandbox on NixOS, or option build-use-sandbox in nix.conf on non-NixOS)
• Built on platform(s)
  • NixOS
  • macOS
  • Linux
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• Fits CONTRIBUTING.md.