Sublime text build system for Lean

Viewed 31

I'm trying to write a build system for the Lean computer proof assistant in sublime text. I have an M1 Mac.

I've written this python file which opens a latex file EXAMPLE.tex and puts out a lean file EXAMPLE.lean.

Here's some code I've come up with to produce a lean file from a tex file. Basically, it takes the text which was internal to the environment \begin{lean} ... \end{lean}.

import re

latexfile = open("/Users/edeany/Documents/latex.tex", "r")
text = latexfile.read()
text = text.replace('\n', '')

x = re.findall("begin\{lean\}.*end\{lean\}", text)
y = ""
for i in range(len(x)):
    y = y + x[i][11 : -10]

leanfile = open("/Users/edeany/Documents/lean.lean", "w")

leanfile.write(y)

My goal is to make a build system for sublime text. I want the build system to build a latex file NAME.tex. By building I mean:

  1. It extracts the $file of the file we want to build
  2. It runs the above python code somehow using the $file string instead of the path that the above code uses, obtaining a file NAME.lean (where we started with NAME.tex).
  3. It runs latex on the original latex file, updating the pdf.
  4. Ideally, there would be a way to run the lean file, but maybe this is not a simple task.

I was hoping someone could show me how to do 1-3. And maybe 4 is possible too.

0 Answers
Related