search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Remove emacs header from files? #2100

Closed jdchristensen closed 2 weeks ago

jdchristensen commented 2 weeks ago

Our STYLE.md document currently suggests adding an emacs header to all files, but I'd be inclined to remove it, since many people working on the library don't use emacs, and in emacs, you can make this setting yourself (which I do, so the headers aren't useful for me). If we decide to remove these headers, we should also update STYLE.md at the same time.

_Based on a comment by @jdchristensen in https://github.com/HoTT/Coq-HoTT/pull/2099#discussion_r1773731771_

SkySkimmer commented 2 weeks ago

It should also be possible to put the setting in dir-locals instead of copying it in every file.

jdchristensen commented 2 weeks ago

It should also be possible to put the setting in dir-locals instead of copying it in every file.

Oh, right, that's a great idea!

jdchristensen commented 2 weeks ago

The line we use turns on coq-mode and visual-line-mode. But it doesn't make sense to globally enable coq-mode for every file in the repository, since there are .md files, bash files, python files, etc. Moreover, anyone using proof-general presumably has it set up to open .v files in coq-mode (or maybe that even happens by default if proof-general is installed). So I think I'll just put visual-line-mode in the .dir-locals.el file.