note-taking organisation in Github

Stream: general

[Josha Dekker]

Hi, although not a pure Lean question, I think this is a good place to ask this question because there might be more people who experienced this here.

I'm not happy with the way my notes are currently structured (read: scattered over my desk, overleaf and notes) and would like to have everything in one centralised place that is maximally integrated in my workflow. I've tried Notion but I'm not happy with the fact that it does not really support offline and does not integrate nicely with code on my device.

As a solution, I'm thinking of putting my notes in a private Github repo and using VS Code as my note-taking environment, so that I can easily link to/integrate snippets of math/Julia code/Lean code/text. (In terms of work-flow, I'm a PhD candidate in Financial Math, so I'm writing notes in LaTex and programming in Julia (in VS Code). I also do some Lean programming in my spare time, and would like to integrate this in my note-taking workflow as much as possible!

Does anyone have experience with this/have pointers to an approach that is suitable for LaTeX, Julia and Lean?

[Johan Commelin]

Do you know about foam-bubble, the vscode plugin?

[Josha Dekker]

No, but that looks very good!

[Anne Baanen]

I have also heard many people saying good things about Emacs org-mode, which is supposed to be able to do all these things too!

[Adam Topaz]

if you want something like roam/foam-bubble with org-mode, there's also org-roam

[Patrick Massot]

And if you want all that in a good editor there is https://github.com/nvim-neorg/neorg

[Adam Topaz]

is there a good org-mode replacement for neovim?

[Adam Topaz]

honestly that's the one thing that makes me want to stay with emacs.

[Adam Topaz]

rather I should ask, how good is neorg?

[Patrick Massot]

I don’t know, I never used any such tool.

[Patrick Massot]

But I’ve heard good things about it.

[Josha Dekker]

so many options... I'll clearly need to explore my options carefully before making a choice, although I'm slightly hesitant to switch to Emacs as I've heard the learning curve can be kind of steep... what is the preferred environment for Lean? VS Code or Emacs? (Or something else?)

[Julian Berman]

Adam Topaz said:

rather I should ask, how good is neorg?

Its OK.

[Julian Berman]

When I tried it, it wasn't ready for day-to-day use in my opinion. But that was around a year or so ago.

[Adam Topaz]

Josha Dekker said:

what is the preferred environment for Lean? VS Code or Emacs? (Or something else?)

VScode is the clear winner here (and neovim is a close second)

[Julian Berman]

(No actually looks like it was 2 years ago even -- https://github.com/Julian/dotfiles/commit/cccac6f54257a53477989d7f96296e27263842ee -- so maybe it's worth a shot again.)

[Adam Topaz]

I think I'll try it out.

[Josha Dekker]

Adam Topaz said:

Josha Dekker said:

what is the preferred environment for Lean? VS Code or Emacs? (Or something else?)

VScode is the clear winner here (and neovim is a close second)

Okay, thank you! That tilts the favour to sticking with VS Code for now for me I think!

[Julian Berman]

Adam Topaz said:

I think I'll try it out.

Lemme know how it goes, I use VimWiki still (thoguh besides neorg there's 2 other org-mode-alikes for nvim too...)

[Jannis Limperg]

Adam Topaz said:

VScode is the clear winner here (and neovim is a close second)

Wait, can neovim do anything (Lean-related) that Emacs can't?

[Adam Topaz]

I don't know... My measure for "preferred" is the number of people using a particular editor, and I think more people use nvim as opposed to emacs.

[Julian Berman]

Jannis Limperg said:

Adam Topaz said:

VScode is the clear winner here (and neovim is a close second)

Wait, can neovim do anything (Lean-related) that Emacs can't?

Widgets, notably, albeit we haven't progressed much over the past few months beyond what Rish initially got working.

There's a fuller demo (of all of lean.nvim's capabilities) in the README: https://github.com/Julian/lean.nvim?tab=readme-ov-file#leannvim

[Richard Copley]

Adam Topaz said:

I don't know... My measure for "preferred" is the number of people using a particular editor, and I think more people use nvim as opposed to emacs.

Does it have to be a popularity contest? The emacses and vims and vscodes and notepads++s and nanos and what have you have coexisted for a long time. Is it really desirable to tell everyone that this language is only for vscode-touchers?

[Patrick Massot]

How is that message related to what you are quoting?

[Richard Copley]

Directly.

[Patrick Massot]

Adam’s message is factual information about what current user prefer to use. How is that linked to “Is it really desirable to tell everyone that this language is only for vscode-touchers?”

[Richard Copley]

Patrick Massot said:

Adam’s message is factual information about what current user prefer to use.

No, it isn't, and doesn't claim to be.
Patrick Massot said:

How is that linked to “Is it really desirable to tell everyone that this language is only for vscode-touchers?”

Directly.

[Richard Copley]

I need to apologize to @Adam Topaz, and others reading, because my earlier message must have seemed like an accusation. I'm sorry.

I do think, in general, that better support for other editors than VS Code would be wonderful. On the other hand I do understand that targetting a web browser-style environment has many benefits.

[Patrick Massot]

I think this is mostly a historical accident. Core developers don’t have time to work on this so it all depends on contributors (I should say depended since the FRO now pay Marc partly for this job, but this is super recent compared to the prevalence of VSCode). There are some fancy widget demos that really use the web browser, but nothing that is used daily.

[Patrick Massot]

This was before I came here, but I think it all started because Jared Roesch decided he wanted to try to develop a VSCode extension during an internship.

[Marc Huisinga]

I think what Richard is also referring to is that the web browser compatibility of VS Code itself is also very good, which enables several use cases where people can work with Lean in VS Code without actually having to install it.

[Yaël Dillies]

eg using gitpod.io (highly rate it, especialy because you can get 250h/month free if you tell them you're an open source software developer)

[Julian Berman]

GitPod luckily works with any of the mentioned editors.

[Yury G. Kudryashov]

Hi, I'm very sorry for not reviewing Emacs lean4-mode PRs. I'll do my best to go over them today.

[Yury G. Kudryashov]

One of the issues is that my Emacs programming skills are pretty bad. I fixed some linter errors and @Sebastian Ullrich made me a co-maintainer.

[Yury G. Kudryashov]

So, I'll ask stupid questions while reviewing...

[Yury G. Kudryashov]

I merged some, will look at some others tomorrow.

[Richard Copley]

Great! Thank you.

[Samuel Levi Schmidt]

Just a +1 for emacs with org-mode. I actively use it to combine lean with LaTeX and other things :smile:

[Junyan Xu]

Andrej Karpathy recommending Obsidian today. And apparently it can be use with Git.

[Josha Dekker]

In the end, I settled on using VS Code + Foam-Bubble + Lean4 + LaTeX Workshop all in the same folder, which makes for a very nice work-flow with Copilot enabled!