1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104

# LeanTeX - LaTeX presentations in Lean 4 

Want to make cool presentations in LaTeX? Want macros and
extensibility without having to learn TeX?

Presenting:
![Demo](https://raw.githubusercontent.com/kiranandcode/leantex/main/demo.jpg)

## Usage

LeanTeX is made as easy as possible to use!

Create a new Lean project requiring `LeanTeX` in your `lakefile.toml`:
```toml
# This is your presentation root
[[lean_lib]]
name = "MyPresentation"

# Require LeanTex!
[[require]]
name = "LeanTex"
git = "https://github.com/kiranandcode/leantex.git"
rev = "main"
```

If you are using a `lakefile.lean`:
```lean
-- lakefile.lean
package MyPresentation

-- This is your presentation root
lean_lib MyPresentation where

-- Require LeanTex!
require LeanTeX from git "https://github.com/kiranandcode/leantex.git" @ "main"
```

In your Lean project, you can import `LeanTeX` use its DSL to write LaTex directly from Lean:
```lean
-- MyPresentation.lean
import LeanTeX

#usepackage bera
#usepackage hyper

#latex_slide do
     latex![| \titlepage |]

```

Finally, to build the presentation, run `lake exe GenerateSlides`:
```bash
$ lake exe GenerateSlides
...

Output written on slides.pdf (5 pages, 33772 bytes).
Transcript written on slides.log.
```
The resulting presentation PDF will be placed in `build/slides.pdf`

## Features

- *Escape hatch* - `latex![| |]` acts as an escape hatch for inserting
  arbitrary text into the generated file. 
  ```lean
  latex![| \author{[|fontsize (size:=18) "Kiran (She/Her)" |]} |]
  ```
  
  The macro itself is an interpolated string, but unlike Lean's
  default string interpolation, we use `[| |]` to break out back into
  Lean. `@{}` also is allowed to escape back into Lean.

- *DSL for Slides* - LeanTex comes with a built in DSL for simplifying
  some LaTeX constructions within Lean:
  ```
  slide "Example Slide" do
     \begin{itemize}
        \item{"Writing LaTeX-like code within Lean"}
        \item{"Looks like LaTeX"}
        \item{"is actually Lean~"}
     \end{itemize}
  ```

- *Animations* - the `with steps` macro allows named steps for your
  animations, avoiding the issue with hard to grasp numeric animation indices

```lean
  with steps [step1, step2, step3, step4] do
     latex![|
       \begin{tikzpicture}
          \draw<@{step1}->  (0,0) rectangle ++(1,1);
          \draw<@{step2}->  (1,0) rectangle ++(1,1);
          \draw<@{step3}->  (2,0) rectangle ++(1,1);
          \draw<@{step4}->  (3,0) rectangle ++(1,1);
       \end{tikzpicture}
     |]
```

- *Static files* - If you create a directory `static` you can place
  files that should be copied into the build directory

See `example` for an example of a LeanTeX project.