MathemaTeX

Stream: general

[Eric Wieser]

Dean Young said:

Screen-Shot-2022-12-28-at-1.43.19-PM.png

Take a look at this screenshot from a PDF I made using MathemaTex! Would you care for this \lean{} environment in .TeX? Reach out to me here or at edeany@nyu.edu.

Could you explain what we're looking at here? From the screenshot,it looks like \lean{} just draws a box; perhaps you could write a longer description of what exactly it is you're announcing, since I assume it's more than that!

[Mario Carneiro]

...but not on #announce please!

[Mario Carneiro]

cc: @Dean Young

[Dean Young]

Eric Wieser said:

Dean Young said:

Screen-Shot-2022-12-28-at-1.43.19-PM.png

Take a look at this screenshot from a PDF I made using MathemaTex! Would you care for this \lean{} environment in .TeX? Reach out to me here or at edeany@nyu.edu.

Could you explain what we're looking at here? From the screenshot,it looks like \lean{} just draws a box; perhaps you could write a longer description of what exactly it is you're announcing, since I assume it's more than that!

[A] Where we're headed.

Mathematex is going to be a Latex library that compiles and runs lean and scores of other softwares. The basic concept is that the code is run at the server of linearlibrary.org (which is down right now for maintenance). I was thinking that the same compilation for the latex file could shoot the code over to the server and update the associated output.txt file. Ideally this would be done with as much as possible packed into a Latex library. I thought that the convenience of the Mathematex package could be enough to make more people try out Lean, Coq, Mizar, Isabelle, etc. And secondly I wanted a professional looking workflow for my work on the computer.

[B] Where we're at.

Right now it's not on my server, just my laptop. The "workflow" part is done and I want to see about making this concept work online through this linearlibrary website I've created. The picture shows lean code which compiled at the same command as the .tex file on my MacBook Pro. It's also pretty good looking except for not having return-lines in some places where it should.

[Dean Young]

P.S. One con is that latex doesn't read unicode. I thought that a good solution would be to have the associated lean file for any serious checks whereas the pdf can have any macros at all compiled using the .tex macro system. To get the associated lean file, the $ and the \ are all deleted. Meanwhile the \lean{} environment has a fixed width font, maybe with the possibility of adding in some code coloring? I liked the prospects of coloring definitions blue or something like that.

[Dean Young]

I'm interested in modifications and advice about [A] from anyone who is interested in the idea.

[Dean Young]

Screen-Shot-2022-12-28-at-1.43.19-PM.png Screen-Shot-2022-12-28-at-5.40.47-PM.png

[Dean Young]

Uploading Screen Shot 2022-12-28 at 5.42.10 PM.png…

[Yaël Dillies]

Do you know about the existing ways we write Lean code into LaTeX? There we have already solved the Unicode issue.

[Dean Young]

Yaël Dillies said:

Do you know about the existing ways we write Lean code into LaTeX? There we have already solved the Unicode issue.

Actually I hadn't heard of this. What is the way?

[Eric Wieser]

One such way is to use LuaTeX or XeTeX instead of pdfLaTeX, along with a font with wider support like DejavuSansMono

[Martin Dvořák]

For example, I write stuff like \texttt{g$_1$.nt $\oplus$ g$_2$.nt} for g₁.nt ⊕ g₂.nt which works but is a bit annoying.

[Eric Wieser]

You definitely don't need to do that Martin

[Kevin Buzzard]

Yeah I use minted and it just works

[Martin Dvořák]

Is it this package?
https://ctan.org/pkg/minted?lang=en

[Kevin Buzzard]

Yes

[Kevin Buzzard]

I include \usepackage(minted) and do

\begin{minted}{lean}
  code here
\end{minted}

to get lean in my LaTeX documents including beamer (you might have to tag the frames as fragile in beamer)

[Kevin Buzzard]

Here's an example which someone doing my course last year wrote (they wanted to change some default options and add some unicode):

\usepackage{minted}
\usepackage{newunicodechar}
\newunicodechar{Ñ}{\ensuremath{\mathcal{N}}}
\newunicodechar{ᵐ}{\ensuremath{^m}}
\newunicodechar{ᶜ}{\ensuremath{^c}}
\newunicodechar{ᶠ}{\ensuremath{^f}}

and then

\begin{minted}[mathescape, numbersep=5pt, frame=lines, framesep=2mm, fontsize=\small]{Lean}
lemma eventually.mono {p q : α → Prop} {f : filter α}
  (hp : ∀ᶠ x in f, p x) (hq : ∀ x, p x → q x) :
  ∀ᶠ x in f, q x
\end{minted}

[Eric Wieser]

The newunicodechar stuff isn't needed so much if you use a different font like the DejaVuSansMono package with non-pdfLaTeX; but is an approach that I've used before too.

[Eric Wieser]

@Dean Young, addressing your original post rather than this tangent about formatting Lean in LaTeX; it's hard for me to believe that running Lean from LaTeX is a useful thing to do, for numerous reasons:

• Building Lean can be slow. If I edit some wording in my paper, I don't want to wait for it to rerun the embedding Lean every time (you can of course solve this with caching like minted does)
• A big part of lean is the fact that it is an interactive theorem prover. When used in an editor designed for writing Lean, you get told all the errors messages and goal states as you are writing, which are crucial for actually developing proofs. Running lean --make from the command line every time you do this is already a very ineffective way to work; having to wait for LaTeX to turn this output into a PDF only makes it more painful!
• Lean often requires a lot of boilerplate which is just noise for mathematical papers where you really only want to include abridged key results (and link to actual working code hosted in a way that is easy for the reader to run)

[Eric Wieser]

I think there is a useful tool hiding here somewhere; sometimes I'll edit Lean code in a paper to fix line-wrapping etc, and accidentally introduce an error that's not present in the supplemental code repository. A way of marking up Lean files such that I can write \includeleansnippet{some_file.lean}{some-marker-ids} to include certain lines of a file (by finding markers not line numbers) or something would ensure that these don't fall out of sync.

I wouldn't be surprised if there are LaTeX packages that provide such a mechanism already for other programming languages.

[Eric Wieser]

Dean Young said:

Mathematex is going to be a Latex library that compiles and runs lean and scores of other softwares. The basic concept is that the code is run at the server of linearlibrary.org (which is down right now for maintenance).

Running arbitrary user code on your own servers is probably not something you want to go anywhere near unless you really know what you're doing when it comes to sandboxing / rate limiting / authentication. See for instance how github stopped running CI for new users to prevent people asking their servers to mine cryptocurrency!

[Dean Young]

Hmm ok. Thanks for all of this information. I'll go with minted then, except I want to keep the visual style of what I had. It seems minted requires a download?

[Eric Wieser]

A download of what? LaTeX doesn't come preinstalled on most systems, so a download of some kind seems unavoidable.

[Dean Young]

Eric Wieser said:

A download of what? LaTeX doesn't come preinstalled on most systems, so a download of some kind seems unavoidable.

It was just some trouble with the package. Here was the error and solution for me:

https://tex.stackexchange.com/questions/99475/how-to-invoke-latex-with-the-shell-escape-flag-in-texstudio-former-texmakerx

I'm not sure if anyone else had the same problem.

[Dean Young]

Thanks all for your help in steering me towards the work that's been done. It seems there's not the space I thought there was for this idea. I decided to go with minted plus the tcolorbox I was using. If anyone wants the look it goes like this:

\begin{tcolorbox}[width=5.5in,colback={white},title={\begin{center}\texttt{Lean \thepythoncounter} \addtocounter{pythoncounter}{1}  \end{center}},colbacktitle=Red,coltitle=black]
\begin{minted}{lean}
def a := 1
\end{minted}
\end{tcolorbox}

with:

\usepackage{tcolorbox, minted}

[Dean Young]

Screen-Shot-2022-12-30-at-12.18.56-PM.png

[Eric Wieser]

I think minted has some built-in integration with tcolorbox available, although I've never used it