title: Sublime text build system for Lean
body: <p>I'm trying to write a build system for the Lean computer proof assistant in sublime text. I have an M1 Mac.</p>
  <p>I've written this python file which opens a latex file EXAMPLE.tex and puts out a lean file EXAMPLE.lean.</p>
  <p>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 <code>\begin{lean} ... \end{lean}</code>.</p>
  <pre><code>import re
  
  latexfile = open(&quot;/Users/edeany/Documents/latex.tex&quot;, &quot;r&quot;)
  text = latexfile.read()
  text = text.replace('\n', '')
  
  x = re.findall(&quot;begin\{lean\}.*end\{lean\}&quot;, text)
  y = &quot;&quot;
  for i in range(len(x)):
      y = y + x[i][11 : -10]
  
  leanfile = open(&quot;/Users/edeany/Documents/lean.lean&quot;, &quot;w&quot;)
  
  leanfile.write(y)
  </code></pre>
  <p>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:</p>
  <ol>
  <li>It extracts the $file of the file we want to build</li>
  <li>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).</li>
  <li>It runs latex on the original latex file, updating the pdf.</li>
  <li>Ideally, there would be a way to run the lean file, but maybe this is not a simple task.</li>
  </ol>
  <p>I was hoping someone could show me how to do 1-3. And maybe 4 is possible too.</p>