Vadim Zaliva (Nov 09 2023 at 01:14): Vadim Zaliva (Nov 09 2023 at 01:14):In order to format code in vscode it needs a plugin for coq. Searching for "category:formatters coq" finds nothing. Did anyone solved this? Perhaps piping it via some external formatter?
Huỳnh Trần Khanh (Nov 09 2023 at 01:18):if you made a formatter you would become famous
Vadim Zaliva (Nov 09 2023 at 01:19):I can run emacs in batch mode :)
Vadim Zaliva (Nov 09 2023 at 01:31):there is also coqc -beautify which I never tried myself. but it is still needs to be hooked up to vscode somehow
Huỳnh Trần Khanh (Nov 09 2023 at 01:33):coqc -beautify is absolutely broken
Huỳnh Trần Khanh (Nov 09 2023 at 01:33):idk about emacs batch mode but ig it just does autoindent
Huỳnh Trần Khanh (Nov 09 2023 at 01:34):I could also do gg=G in Vim lol
Huỳnh Trần Khanh (Nov 09 2023 at 01:35):would you like a chance to be famous?
Vadim Zaliva (Nov 09 2023 at 01:36):also there is this: http://www.eelis.net/coqindent/
Vadim Zaliva (Nov 09 2023 at 01:38):I wonder if there is some simple pluging or shortcut in vscode to run source buffer via external command and update with the output. then I would try to find some suitable formatter to try.
Huỳnh Trần Khanh (Nov 09 2023 at 01:38):Code Runner
Huỳnh Trần Khanh (Nov 09 2023 at 01:39):but anyway feel free to try out "formatters" you find online. you'll find them severely lacking
Huỳnh Trần Khanh (Nov 09 2023 at 01:39):isn't it sad
Vadim Zaliva (Nov 09 2023 at 01:40):Code runner does not seems to be able to replace the current buffer with the output
Vadim Zaliva (Nov 09 2023 at 01:41):it will show it in "output" buffer instead
Huỳnh Trần Khanh (Nov 09 2023 at 01:41):close enough. you can pass the current file as argument. and when the file is rewritten the buffer is automatically updated
Vadim Zaliva (Nov 09 2023 at 01:42):ok, thanks. I will experiment with it
Vadim Zaliva (Nov 09 2023 at 01:42):I am reasonable happy with emacs proof general Coq identation. I was not kidding about running emacs in batch mode :)
Bas Spitters (Nov 09 2023 at 10:41):http://www.eelis.net/coqindent/
Huỳnh Trần Khanh (Nov 09 2023 at 11:47):https://github.com/toku-sa-n/coqfmt (AGPL)
Huỳnh Trần Khanh (Nov 09 2023 at 11:51):looks like this person will become famous
Karl Palmskog (Nov 09 2023 at 12:44):AGPL is unfortunately a minefield, in particular for something that spits out code (some background here)
Théo Zimmermann (Nov 09 2023 at 13:18):For libraries, we can argue that strong copyleft discourages adoption, but for tools I disagree. A formatter cannot be claimed to spit out any code besides the one that you entered (so absolutely no licensing issue here). The fact that some big companies like Google are shy with AGPL is a fact that people might consider disqualifies this license if they want the widest use, but I would argue that the problem is on those companies (and I wouldn't expect smaller companies like, e.g., Bedrock Systems, to be afraid to use a code formatter that is licensed under AGPL).
Karl Palmskog (Nov 09 2023 at 13:20):AGPL is so strong that you basically need a lawyer to look at the program in question and determine whether its output is under the tool's license
Karl Palmskog (Nov 09 2023 at 13:22):see discussion about source code tools here.
Karl Palmskog (Nov 09 2023 at 13:24):I would be surprised if Bedrock allow any kind of external AGPL tools anywhere, but maybe Paolo or Janno could could comment...
Karl Palmskog (Nov 09 2023 at 13:39):I guess one question is if the formatter only ever outputs white spaces, newlines and the like. If it can sometimes add hardcoded code fragments, I'd say that may turn your code into AGPL. The question is how to even be sure it doesn't output hardcoded text
Emilio Jesús Gallego Arias (Nov 09 2023 at 14:09):I think we should be careful about stating strong legal opinions here; there is little in the intent of the AGPL (with intent being often the most relevant legal term) that would indicate that a source code formatter would be allowed to alter the license of its input and more strikingly to claim copyright over it!
This would be AKIN to having Photoshop claim copyright of images it processed (which is now a problem due to their AI fill, but that's a different story), or Word's auto-format being able to have your text licensed by Microsoft.
Quoting the AGPL "Why section"
The purpose of the GNU Affero GPL is to prevent a problem that affects developers of free programs that are often used on servers.
So indeed, Hiroki-san formatter being AGPL means that if someone is going to run that formatter as a service, the actual source code should be available to the service's users under the AGPL; which in the context of the formatter, it seems fine.
AGPL is so strong that you basically need a lawyer to look at the program in question and determine whether its output is under the tool's license
That seems like quite a strong claim, in the sense that AGPL doesn't differ from GPL in this scenario. Can you point out an event where this happened?
As Théo correctly points out, it makes total sense for Google to be very wary of the AGPL as the AGPL is indeed precisely designed to target Google and other operators of cloud service as not to allow them to use free software in their servers without releasing its source code, something that for sure Google would like to prevent at all costs.
Making the jump from the needs of a large, service-oriented company to a code formatting tool is maybe too much of a jump.
Karl Palmskog (Nov 09 2023 at 14:49):what I mean with "strong" is that if the tool indeed embeds its own source code into its output, and you apply the output on a single file in a large project, the project as a whole may have to turn AGPL, and any clients of the project as well
Huỳnh Trần Khanh (Nov 09 2023 at 14:52):actually even if the output doesn't fall under AGPL there might be other implications. CI workflows that automatically format code might be affected
Emilio Jesús Gallego Arias (Nov 09 2023 at 14:52):How would such workflows be affected @Huỳnh Trần Khanh ?
Emilio Jesús Gallego Arias (Nov 09 2023 at 14:53):Other than having to point out where the source code for the exact version of the tool used in the workflow is?
Emilio Jesús Gallego Arias (Nov 09 2023 at 14:54):Which is the case for all CI workflows using open source linters that I know of. You are correct that AGPL would prevent using a private version of the formatter in CI that I can access, unless you share the modified version with me. But is this a real issue?
Emilio Jesús Gallego Arias (Nov 09 2023 at 14:56):Karl Palmskog said:
what I mean with "strong" is that if the tool indeed embeds its own source code into its output, and you apply the output on a single file in a large project, the project as a whole may have to turn AGPL, and any clients of the project as well
I guess that indeed there are many strange things tools that process source code can do, but I fail to see how this applies here. Also, in that hypothetical case you describe, a tool doing that would hardly force a whole existing codebase not licensed under the AGPL to become AGPL, this is not how copyright works, in particular if the tool misrepresented what it is doing with your code.
Karl Palmskog (Nov 09 2023 at 15:01):one case in point. The lexer generator JFlex was previously under GPL. However, it had an additional clause stating that all the tool's output is owned by the user. Here is a tool under an even stronger copyleft license that makes no claim like this. Since I don't have time to do (A)GPL license analysis for specific tools, I'd just prefer to not use any (A)GPL licensed tool that outputs source code.
Karl Palmskog (Nov 09 2023 at 15:03):I give several more examples of GPL'd tools outputting source code and issues flagged up by FSF themselves here, as linked above
Emilio Jesús Gallego Arias (Nov 09 2023 at 15:11):I'd just prefer to not use any (A)GPL licensed tool that outputs source code.
I can understand this is your preference, however that doesn't mean there is a problem with the tool, which you seem to imply. IMHO this creates unnecessary uncertainty and distracts from the primary purpose of the tool by a problem that is, IMVHO, not even hypothetical in the context of the tool.
AGPL is not more of a minefield for a tool that outputs "original" code than any of the GPL licenses. GPL / AGPL are widely considered to be non-issues for tools that transform inputs such as GIMP or Code Formatters (tho the legal framework is still far from settled)
Note that in the CoqFFI discussion the author indeed did not share your position, even if in the end he went for a relicensing. The issues you point out about bison or GCC are issues well understood (the output needs an essential library to work, which needs a different copyright), and have little to do with AGPL but with the GPL. But again, I'm not sure why pointing out problems in other contexts is relevant for the discussion of the formatting tool here.
Karl Palmskog (Nov 09 2023 at 15:15):are you saying you know exactly what a claimed formatter tool does? If a formatter tool author was interested in assuring their users, why wouldn't they add a "you own all output" clause?
Karl Palmskog (Nov 09 2023 at 15:19):the difference from GIMP is that GIMP doesn't embed its source code in edited images...
Karl Palmskog (Nov 09 2023 at 15:22):GPL and AGPL are the same in that they can both embed source code in their output and get code that uses it relicensed, but AGPL is much more large in scope of what code gets relicensed. I don't have time to figure out what "network interaction" means in my jurisdiction
Emilio Jesús Gallego Arias (Nov 09 2023 at 15:44):Again I do understand what you may have your own reasons (whether founded on legal experience or not) to use or not to use a tool.
However I still do think we should be more careful about turning our own reasons into general advice or comment on a tool or a license, in particular when your own perceived "danger" of the license of the tool doesn't seem to the case here AFAICT. This does create unnecessary and unfounded uncertainty around the tool, whose license is fine unless you want to do a closed-source formatting service.
Emilio Jesús Gallego Arias (Nov 09 2023 at 15:44):Karl Palmskog said:
the difference from GIMP is that GIMP doesn't embed its source code in edited images...
Neither does the formatter we are discussing, so how is this relevant?
Emilio Jesús Gallego Arias (Nov 09 2023 at 15:45):Even if it did, any claim on this action affecting the copyright of the input would be legally void, trivially, in any court.
Emilio Jesús Gallego Arias (Nov 09 2023 at 15:46):The relevant legal notion here is whether the output can be considered a "derived work" of the tool, that in itself is a very complex not fully developed notion.
Enrico Tassi (Nov 09 2023 at 20:44):Can someone with enough rights move this thread to Misc > AGPL for a formatting library?
I don't see any link with vscoq starting from the message questioning the choice of license.
Paolo Giarrusso (Nov 09 2023 at 21:39):Can you configure Emacs to defer indentation to this tool?
Vadim Zaliva (Nov 09 2023 at 21:43):not sure you can do it for "live" indentation as you type. but you can probably configure indent-region to call an external tool.
Paolo Giarrusso (Nov 09 2023 at 21:44):Can you disable live indentation?
Vadim Zaliva (Nov 09 2023 at 21:44):yes
Paolo Giarrusso (Nov 09 2023 at 21:44):Interesting
Vadim Zaliva (Nov 09 2023 at 21:44):(defvar indent-line-function 'indent-relative
"Function to indent the current line.
This function will be called with no arguments.
If it is called somewhere where it cannot auto-indent, the function
should return `noindent' to signal that it didn't.
Setting this function is all you need to make TAB indent appropriately.
Don't rebind TAB unless you really need to.")
i guess re-defining this variable to noindent should do the trick. Maybe there is even more global way disabling indentation in emacs.
Paolo Giarrusso (Nov 09 2023 at 21:48):If this tool can be used with no additional burden for Emacs users, it'd be great.
Paolo Giarrusso (Nov 09 2023 at 21:49):That sounds promising, thanks.
Paolo Giarrusso (Nov 09 2023 at 21:50):@Karl Palmskog I haven't applied for using any AGPL tools yet, so I don't have statistics, I guess we'd have to look when that happens.
Vadim Zaliva (Nov 09 2023 at 21:51):As I mentioned, I am pretty happy with coq indentation in emacs. The original question was about indentation in VsCoq. I miss a functionality where I can quickly re-ident whole buffer (file? window?)
Paolo Giarrusso (Nov 09 2023 at 21:52):I know of no such feature today, especially not in vscoq
Vadim Zaliva (Nov 09 2023 at 21:53):this is how I do this in emacs:
(defun tidy-buffer ()
"Tidy up current buffer by re-identing and cleaning up whitespace"
(interactive)
(indent-region (point-min) (point-max))
(whitespace-cleanup-region (point-min) (point-max)))
This topic was moved here from #VsCoq devs & users > coq identation by Emilio Jesús Gallego Arias.
Emilio Jesús Gallego Arias (Nov 10 2023 at 14:18):Moved as requested, I've used User Interfaces better than Misc, but happy to head to misc if you folks feel that's better.
Emilio Jesús Gallego Arias (Nov 10 2023 at 14:19):Regarding use in VSCode or Emacs, it is easy to hook Hiroki-san formatter or any other formatter to for example coq-lsp, and use standard LSP-based facilities; happy to help with that project if someone is interested.
The hooks in coq-lsp are already there, so all you need is to write a function Ast.t -> string, YMMV
Emilio Jesús Gallego Arias (Nov 10 2023 at 14:20):The main pain point (as discussed with @Hiroki Tokunaga ) is that Coq doesn't offer facilities for formatters to access the AST.
Emilio Jesús Gallego Arias (Nov 10 2023 at 14:20):That's a real problem; coq-lsp and serlib provide their own system, but it is often not enough.
Pierre Courtieu (Nov 11 2023 at 00:28):@Vadim Zaliva this must be quite slow on big buffers, focusing on the current region may may be useful sometimes I suppose.
(defun tidy-region (min max)
"Tidy up current region by re-identing and cleaning up whitespace"
(interactive "r")
(indent-region min max)
(whitespace-cleanup-region min max))
Last updated: Oct 13 2024 at 01:02 UTC