LaTeX advice

Stream: FLT

[Kevin Buzzard]

I have never written LaTeX in VS Code before FLT; all my papers are written in emacs. But it's convenient to write FLT LaTeX in VS Code because of the copilot boost. What can I use to make my LaTeX experience easier? In emacs I just have shortcuts to do stuff like "compile this LaTeX", "open the pdf" etc. I would also be interested in streamline the approach being used in the PNT project; they are writing LaTeX in .lean files and I would like to avoid this if possible whilst still getting copilot autocomplete.

[Josha Dekker]

Kevin Buzzard said:

I have never written LaTeX in VS Code before FLT; all my papers are written in emacs. But it's convenient to write FLT LaTeX in VS Code because of the copilot boost. What can I use to make my LaTeX experience easier? In emacs I just have shortcuts to do stuff like "compile this LaTeX", "open the pdf" etc. I would also be interested in streamline the approach being used in the PNT project; they are writing LaTeX in .lean files and I would like to avoid this if possible whilst still getting copilot autocomplete.

I’m assuming you know the LaTeX workshop extension? I find that very easy! You can also set up VS-code to automatically compile the latex once you save a file. If you can’t find it, I can look up how I did it tomorrow!

[Julian Berman]

Just to be sure Kevin, you I assume considered the reverse, enabling copilot in Emacs? https://github.com/copilot-emacs/copilot.el looks like a thing.

[Jireh Loreaux]

I think the LaTeX workshop extension here is the way to go. To be honest, I used to use Emacs, and I started primarily because of LaTeX, but at this point the main thing I use it for is magit!

[Kevin Buzzard]

I don't want to write Lean code in emacs, I'm sick of emacs, I'm too old to use it. I just want something which is simple to use for people who can't remember keyboard shortcuts and easy to extend, I don't have time for emacs any more :-( When I was a post-doc my emacs had a psychoanalyze-pinhead command but those halcyon days are gone.

[Terence Tao]

Kevin Buzzard said:

I have never written LaTeX in VS Code before FLT; all my papers are written in emacs. But it's convenient to write FLT LaTeX in VS Code because of the copilot boost. What can I use to make my LaTeX experience easier? In emacs I just have shortcuts to do stuff like "compile this LaTeX", "open the pdf" etc. I would also be interested in streamline the approach being used in the PNT project; they are writing LaTeX in .lean files and I would like to avoid this if possible whilst still getting copilot autocomplete.

Code snippets are a nice feature for VSCode's LaTeX plugin. For instance here is my snippet to create a theorem+proof from typing "thm" and then TAB:

"Theorem":{
    "prefix": "thm",
    "body": [
        "\\begin{theorem}[$1]\\label{$2}",
        "$3",
        "\\end{theorem}",
        "",
        "\\begin{proof}",
        "$4",
        "\\end{proof}"
    ],
    "description": "Theorem environment"
},

After one writes a single such snippet, Copilot is pretty good at making more; after entering in the theorem snippet manually, Copilot correctly gave me a lemma snippet, corollary snippet, remark snippet, etc. without difficulty.

[Mario Carneiro]

Is FLT set up for use with Latex Workshop? I had difficulties compiling the blueprint last time I tried

[Mario Carneiro]

The default build target seems not to work; there is a long list of alternative builds and by trial and error I found that "Recipe: latexmk (lualatex)" works but I'm not sure what needs to be done so that it remembers to keep doing that

[Eric Wieser]

latex-workshop.latex.recipe.default is probably the setting to change

[Patrick Massot]

This is a really sad thread. emacs or vi are clearly infinitely superior to VSCode for TeX writing. And code snippets support exists in every editor.

[Kevin Buzzard]

Is that really true? :-( I was hoping to migrate to VSCode and make everything better

[Kim Morrison]

Patrick has an opinion, but it is not universally shared. :-)

[Patrick Massot]

I never saw anyone using VSCode efficiently for that kind of editing. The closest I saw were people explaining the main trick is to use a plugin that tries to use vim from VSCode but only half works, and I couldn’t quite see the point.

[Kim Morrison]

I've never really been bothered by the efficiency of the communication channel between my brain and the tex file. My brain is clearly slower than the channel already. :-)

[Patrick Massot]

I feel that lack of efficiency here translates to loosing focus.

[Patrick Massot]

But of course if Kevin’s goal is to get Copilot to write everything then focus and brains are kind of irrelevant.

[Kevin Buzzard]

Did you see that I tried experimenting with a hand-rolled definition of Z-hat and some basic adelic calculations in disguise, in the new "example" chapter of the project? Copilot was really good at writing the Lean API from the LaTeX, which I was manually pasting into the lean file as comments and then deleting after the Lean code was compiling. Right now I don't know a better system.

[Patrick Massot]

I was pointed out that you could use Copilot in emacs

[Kevin Buzzard]

Sure but I am too stupid for emacs now, I want a simple interface.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

I have never written LaTeX in VS Code before FLT; all my papers are written in emacs. But it's convenient to write FLT LaTeX in VS Code because of the copilot boost. What can I use to make my LaTeX experience easier? In emacs I just have shortcuts to do stuff like "compile this LaTeX", "open the pdf" etc. I would also be interested in streamline the approach being used in the PNT project; they are writing LaTeX in .lean files and I would like to avoid this if possible whilst still getting copilot autocomplete.

FWIW, I very often use VSCode for LaTeX with this extension and I have configured all the shortcuts as in TeXstudio, so I basically forget whether I have opened a tex with VSCode or with TeXstudio. You can do this from the VSCode Keyboard Shortcuts button. But I have never tried Copilot for LaTeX.

[Mario Carneiro]

Patrick Massot said:

This is a really sad thread. emacs or vi are clearly infinitely superior to VSCode for TeX writing. And code snippets support exists in every editor.

FWIW, I've written many hundreds of pages in LaTeX using vscode. My fingers refuse to learn vi/emacs, and it's approximately tied with overleaf regarding my personal productivity in producing latex documents. (I will usually use overleaf for smaller articles and vscode for books or thesis-sized projects)

[Mario Carneiro]

I honestly fail to see what makes vscode so horrible or vi so infinitely superior, assuming we set aside the general editor stuff

[Patrick Massot]

What makes vi infinitely superior to VSCode is modal editing.

[Mario Carneiro]

ah. Okay... (slowly walks to the exit)

[llllvvuu]

As a lifelong vi/vim/nvim user, I think it's a habits thing. Back then we didn't have much of a choice to invest in that ecosystem. Nowadays I generally don't recommend people invest in it if they haven't already.

As for modal editing, I consider it orthogonal to buying into the plugin/config ecosystem. I actually find vscode-neovim works well, and I have <100 lines of config active in it (versus >1000 lines of config active for nvim TUI frontend). But I'm not even sure I'd force the issue on modal editing for people who haven't already sunk into the habits. I see people be productive enough with VSCode controls.

[Julian Berman]

Yes I too subscribe to "modal editing is very large amounts better" as well as even more arguably "the nvim + emacs plugin ecosystems are way way better", but tapered by "I don't think it's worth it if you don't want to fuss with your editor and/or pay the learning cost, if you're too cranky for that already at some point in your life just move on :)." But that's indeed why I mentioned the copilot plugin.

[Eric Wieser]

But VSCode is modal too; sometimes my right hand is in "operate mouse mode", and other times it's on the keyboard!

[Patrick Massot]

Operate what?! Is your house infested?

[Kevin Buzzard]

How do I set up LaTeX workshop to work with FLT (or more generally a blueprint project)? I probably need to explicitly give the build command. But I couldn't get cd blueprint/src; lualatex print.tex; cd ../.. or leanblueprint pdf to work.

[Alex Kontorovich]

@Ian Jauslin, is this something you might be able to help Kevin with?

[Kevin Buzzard]

Oh it's OK, it works out of the box :-)