Stream: VsCoq devs & users

Topic: Ignoring binary files

Karl Palmskog (Oct 16 2020 at 23:26):

In VSCoq, is the best practice to ignore .vo, .glob, etc., really to have the following in .vscode/settings.json:

{
    "files.exclude": {
        "**/.*.aux": true,
        "**/*.glob": true,
        "**/*.vo": true,
        "**/*.vok": true,
        "**/*.vos": true
    }
}

Isn't this something that can be configured by default for all projects somehow?

Paolo Giarrusso (Oct 16 2020 at 23:49):

that’s a great vscode mystery

Paolo Giarrusso (Oct 16 2020 at 23:49):

my files.exclude lists **/.git and **/.DS_Store, and I just confirmed neither is implied.

Paolo Giarrusso (Oct 16 2020 at 23:50):

uh sorry, that’s not true.

Paolo Giarrusso (Oct 16 2020 at 23:52):

hm. I have the Hide gitignored extension, and I have a global .gitignore configuration with those files.

Karl Palmskog (Oct 16 2020 at 23:53):

OK, so basically one should get that extension and not bother with the above (settings.json)?

Paolo Giarrusso (Oct 16 2020 at 23:53):

but I remember that wasn’t satisfactory, so I still have those files in files.exclude...

Paolo Giarrusso (Oct 16 2020 at 23:53):

sorry — my TLDR is “I also failed to find something better”

Karl Palmskog (Oct 16 2020 at 23:55):

that's depressing, I guess this is state of the art (everyone goes in and configures on their own, or we all duplicate a settings.json everywhere): https://stackoverflow.com/questions/30140112/how-do-i-hide-certain-files-from-the-sidebar-in-visual-studio-code

Karl Palmskog (Oct 16 2020 at 23:56):

I'm still all in on emacs, but since everyone and their brother is seemingly using vscode these days, I have to keep up..

Paolo Giarrusso (Oct 17 2020 at 00:08):

At least you'll see all the possible bugs from async proofs and/or VsCoq... (Async proofs work better in coqide)

Théo Winterhalter (Oct 17 2020 at 07:10):

I think if, instead of using the bar on the left with the list of files, you use Ctrl/Cmd + P to access files, it is smarter and recommends the interesting files first.

Paolo Giarrusso (Oct 17 2020 at 10:09):

But does that work for the workspace search? IIRC not

Théo Winterhalter (Oct 17 2020 at 11:02):

Oh I see sorry.

Last updated: Jun 04 2023 at 22:30 UTC