Nix doesn't like filenames with '!'

Stream: lean4

[Mario Carneiro]

Reposting mathlib4#1212 here in case someone knows whether this is a Nix issue or an issue in the lean Nix derivation (@Sebastian Ullrich ?):

I've tried to follow the lean4 manual to get a working flake.nix under NixOS because I haven't figured out how to get elan run correctly.

{
  description = "My Lean package";

  inputs.lean.url = github:leanprover/lean4;
  inputs.std4-src.url = github:leanprover/std4;
  inputs.std4-src.flake = false;
  inputs.qq-src.url = github:gebner/quote4;
  inputs.qq-src.flake = false;
  inputs.aesop-src.url = github:JLimperg/aesop;
  inputs.aesop-src.flake = false;
  inputs.flake-utils.url = github:numtide/flake-utils;

  outputs = { self, lean, std4-src, qq-src, aesop-src, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
    let
      leanPkgs = lean.packages.${system};
      std = leanPkgs.buildLeanPackage {
        name = "Std";
    src = "${std4-src}/";
      };
      qq = leanPkgs.buildLeanPackage {
        name = "Qq";
    src = "${qq-src}/";
      };
      aesop = leanPkgs.buildLeanPackage {
        deps = [ std ];
        name = "Aesop";
    src = "${aesop-src}/";
      };
      pkg = leanPkgs.buildLeanPackage {
        deps = [ std  qq aesop ];
        name = "Mathlib";  # must match the name of the top-level .lean file
        src = ./.;
      };
    in rec {
      packages = pkg // {
        inherit std;
    inherit aesop;
    inherit qq;
        inherit (leanPkgs) lean;
      };

      defaultPackage = packages.modRoot;
    });
}

[Mario Carneiro]

when running nix shell I get

error: store path '0v269bm9c066cm2xrgj4ic37cy7j1y2n-Clear!.lean' contains illegal character '!'
(use '--show-trace' to show detailed location information)

[Sebastian Ullrich]

I guess I didn't anticipate that. I'll add escaping.