Static facets and Export.Parse not built

Currently, when building comparator with an already built/distributed lean4export, it tries to build Export.Parse leading to a permission denied issue when the artifacts of lean4export are distributed in a read-only state (as is the case with nix e.g.).

To fix this, lean4export should also build Export.Parse which can be fixed by adding globs = ["Export.*"] to lakefile.toml under the Export library configuration (otherwise, when building comparator for example, lake tries to build these in the immutable location /path/to/lean4export/.lake).

This would be sufficient to build comparator's oleans, but as it also contains an exe which import Export.Parse, it needs the static library facets (including the .c.o.export files that are found under .lake/build/ir/Export/) which again, when missing, lake tries to build in the immutable location. To build static facets as part of lean4export we should add defaultFacets = ["static"] to the Export library configuration.

I can submit a PR for this if it's okay?

Start in lakefile.toml at the Export library configuration and review how comparator builds against distributed lean4export artifacts. Verify the configuration for Export.Parse and static facets, then build comparator with read-only lean4export artifacts. Done means comparator's oleans and executable build without lake trying to write into the immutable lean4export location.