1 files changed, 23 insertions, 1 deletions
diff --git a/modules/coq.nix b/modules/coq.nix
index 3a1dfef..995dc40 100644
--- a/modules/coq.nix
+++ b/modules/coq.nix
@@ -3,8 +3,11 @@
 with lib;
 let
   cfg = config.coq;
-  coqBuildInputs = (with cfg.coqPackages; [ coq ])
+  coqBuildInputs =
+    (with cfg.coqPackages; [ coq ])
     ++ (cfg.packages cfg.coqPackages);
+  coqrc = pkgs.writeText "coqrc" cfg.rc;
+  coqFlags = concatStringsSep " " ([ "-init-file ${coqrc}" ]);
 in {
   options.coq = {
     enable = mkEnableOption { name = "coq"; };
@@ -28,8 +31,27 @@ in {
         coqPackages: with coqPackages; [ autosubst ];
       '';
     };
+    rc = mkOption {
+      type = types.lines;
+      default = "";
+      description = ''
+        Commands to be prepended to any document read by Coq.
+      '';
+      example = ''
+        Add Rec LoadPath "../my-module/" as MyModule.
+      '';
+    };
+
+    # This option isn't available yet as disabling buildIde is actually heavier
+    # on the user (the version without IDE is not cached by Hydra).
+    # ide.enable = mkEnableOption "IDE";
   };
   config = mkIf cfg.enable {
     buildInputs = coqBuildInputs;
+    aliases = {
+      coqc = "${cfg.coqPackages.coq}/bin/coqc ${coqFlags} \\$@";
+      coqide = "${cfg.coqPackages.coq}/bin/coqide ${coqFlags} \\$@";
+      coqtop = "${cfg.coqPackages.coq}/bin/coqtop ${coqFlags} \\$@";
+    };
   };
 }