Skip to content

Commit

Permalink
Gitpod in readme
Browse files Browse the repository at this point in the history
  • Loading branch information
ianjauslin-rutgers committed May 7, 2024
1 parent e7e5a29 commit 2624f0a
Showing 1 changed file with 14 additions and 1 deletion.
15 changes: 14 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
# PrimeNumberTheoremAnd


## Blueprint

This project has a blueprint, which is available at <https://AlexKontorovich.github.io/PrimeNumberTheoremAnd/web/>.

To use the tool, first install local requirements using
Expand All @@ -13,9 +16,19 @@ cd blueprint
make pdf
```

# Use of LaTeX inside Lean
## Use of LaTeX inside Lean

For those using github's copilot (free for educators), it's very convenient to have the natural language statements
right next to the Lean to be formalized. So we write the blueprint TeX right in the *.lean document, separated by
delimiters `/-%% text here %%-/` for multi-line and `--%% text here` for single-line TeX. The code automatically
scrapes these and populates the blueprint accordingly.


## Quick contributions via gitpod
If you want to quickly contribute to the project without installing your own copy of lean, you can do so using gitpod.
Simply visit: <https://gitpod.io/new/#https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/>, or click the button below:

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/new/#https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/)

All the required dependencies will be loaded (this takes a few minutes), after which you will be brought to a web-based
vscode window, where you can edit the code, and submit PR's.

0 comments on commit 2624f0a

Please sign in to comment.