created basic site structure and added support for katex and lagda

This commit is contained in:
Rachel Lambda Samuelsson 2022-01-26 21:35:10 +01:00
commit 94da16f45e
7 changed files with 78 additions and 0 deletions

4
.gitignore vendored Normal file
View File

@ -0,0 +1,4 @@
.jekyll-cache
.agda-html
_site
*.agdai

15
_config.yml Normal file
View File

@ -0,0 +1,15 @@
url: "https://depsterr.com" # the base hostname & protocol for your site, e.g. http://example.com
baseurl: "" # the subpath of your site, e.g. /blog
title: "depsterr.com" # the name of your site, e.g. ACME Corp.
plugins:
- jekyll-feed
- jekyll-katex
- jekyll/agda
exclude:
- "*.agdai"
katex:
rendering_options:
throw_error: true

14
_layouts/default.html Normal file
View File

@ -0,0 +1,14 @@
<!DOCTYPE html>
<html lang="en-US">
<head>
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta charset="utf-8">
<title>{{ page.title }} - {{ site.title }}</title>
<link rel="stylesheet" href="{{ "/assets/css/main.css" | relative_url }}">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.15.2/dist/katex.min.css" integrity="sha384-MlJdn/WNKDGXveldHDdyRP1R4CTHr3FeuDNfhsLPYrq2t0UBkUdK2jyTnXPEK1NQ" crossorigin="anonymous">
<link rel="stylesheet" href="{{ '/lagda/Agda.css' | relative_url }}" />
</head>
<body>
{{ content }}
</body>
</html>

View File

@ -0,0 +1,20 @@
---
layout: default
title: "test"
---
{% katexmm %}
Hi :)
$\sqrt{x + \frac{1}{2}}$
{% endkatexmm %}
```agda
data : Set where
zero :
suc :
```
Is `Set` clickable? Yes it is.
And the other keywords too!

9
_sass/main.scss Normal file
View File

@ -0,0 +1,9 @@
$backgroundColor: #ffffff;
$bodyColor: #000000;
$bodyFont: -apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";
body {
background: $backgroundColor;
color: $bodyColor;
font-family: $bodyFont;
}

4
assets/css/main.scss Normal file
View File

@ -0,0 +1,4 @@
---
---
@import "main";

12
index.html Normal file
View File

@ -0,0 +1,12 @@
---
layout: default
title: "home"
---
<ul>
{% for post in site.posts %}
<li>
<h2><a href="{{ post.url }}">{{ post.title }}</a></h2>
{{ post.excerpt }}
</li>
{% endfor %}
</ul>