Speed up ref generation

.gitignore

@@ -10,4 +10,5 @@ build.ninja
 *.ilean
 *.olean
 ref/index.html
-ref/src/generated.lean
+ref/src/generated.lean
+mir

dodo.py

@@ -30,7 +30,8 @@ def task_electrolysis_ref():
     for p in list(ref.rglob('lib.rs')):
         yield {
             'name': str(p),
-            'actions': [['cargo', 'run', p]] +
+            'actions': [['cargo', 'run', p],
+                        'rustc --crate-type lib -Z unstable-options --unpretty mir "{}" > "{}"'.format(p, p.with_name('mir'))] +
             ([['mv', p.with_name('generated.lean'), p.with_name('broken.lean')]]
              if '!' in str(p) else []),
             'file_dep': [p, 'target/debug/electrolysis'],

ref/7 Statements and expressions/7.2 Expressions/7.2.15 Lambda expressions/1 Mutable closures./pre.md

@@ -0,0 +1 @@
+Mutable closures work out of the box as long as they don't close over mutable references - that would require [nested storing of `&mut`](#nested-storing-of-mut-refs.).

ref/make_ref.py

@@ -76,8 +76,7 @@ def rec(path, depth):
         yield markdown.markdown(open(os.path.join(path, 'pre.md')).read(), extensions=[CodeBlockExtension()])
     if 'lib.rs' in entries:
         rust = os.path.join(path, 'lib.rs')
-        mir = subprocess.run(['rustc', '--crate-type', 'lib', '-Z', 'unstable-options', '--unpretty', 'mir', rust],
-                             stdout=subprocess.PIPE, check=True).stdout.decode('utf8')
+        mir = open(os.path.join(path, 'mir')).read()
         generated = open(os.path.join(path, 'broken.lean' if '!' in path else 'generated.lean')).read()
         if '5 Crates' not in path:
             generated = re.search('(open [^\n]*\n)+\n(.*)', generated, flags=re.DOTALL).group(2)